Split proof [aRTA+ -> aRTA]

17 jobs for da3 in 19 minutes and 5 seconds (queued for 1 second)
Status Job ID Name Coverage
  Build
passed #63132
1.10.0-coq-8.10

00:08:28

passed #63133
1.10.0-coq-8.11

00:08:03

failed #63131
1.10.0-coq-8.9

00:01:29

passed #63129
1.9.0-coq-8.10

00:10:54

passed #63130
1.9.0-coq-8.11

00:10:55

failed #63128
1.9.0-coq-8.9

00:01:45

passed #63134
build-for-process

00:04:22

passed #63135
build-for-process-classic

00:04:04

failed #63138
allowed to fail
coq-8.10

00:05:42

failed #63139
allowed to fail
coq-dev

00:05:52

failed #63136
proof-length

00:00:44

failed #63137
spell-check

00:00:50

 
  Process
passed #63142
doc

00:02:22

passed #63143
doc-classic

00:01:26

passed #63144
proof-state

00:04:41

passed #63140
validate

00:01:48

passed #63141
validate-classic

00:02:36

 
Name Stage Failure
failed
coq-dev Build
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
'opam install -y -v -j 2 coq-prosa' failed.
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
failed
coq-8.10 Build
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
'opam install -y -v -j 2 coq-prosa' failed.
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
failed
spell-check Build
./analysis/abstract/abstract_rta.v: potentially misspelled word 'rbf'
./analysis/abstract/abstract_rta.v: potentially misspelled word 'reponse'
./analysis/abstract/abstract_rta.v: potentially misspelled word 'sched'
./analysis/abstract/abstract_rta.v: potentially misspelled word 'subcases'
./analysis/abstract/abstract_rta.v: potentially misspelled word 'tightess'
./analysis/abstract/abstract_rta.v: potentially misspelled word 'tsk'
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
failed
proof-length Build
Restoring cache
Downloading artifacts
Running before_script and script
$ scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
Warning: new long proof of uniprocessor_response_time_bound_SBF in ./analysis/abstract/abstract_rta.v:1207!
Checked 1857 proofs in 320 files, while skipping 149 known long proofs.
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
failed
1.10.0-coq-8.9 Build
# COQC classic/util/notation.v
# make[1]: *** [Makefile:677: util/setoid.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:327: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
failed
1.9.0-coq-8.9 Build

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1