Closed all the proofs

17 jobs for aSBF in 11 minutes and 12 seconds (queued for 1 second)
Status Job ID Name Coverage
  Build
passed #70640
1.10.0-coq-8.10

00:11:11

passed #70641
1.10.0-coq-8.11

00:11:09

failed #70639
1.10.0-coq-8.9

00:01:56

passed #70637
1.9.0-coq-8.10

00:11:04

passed #70638
1.9.0-coq-8.11

00:11:10

failed #70636
1.9.0-coq-8.9

00:01:57

passed #70642
build-for-process

00:03:58

passed #70643
build-for-process-classic

00:07:38

failed #70646
allowed to fail
coq-8.10

00:06:40

failed #70647
allowed to fail
coq-dev

00:07:08

failed #70644
proof-length

00:01:31

failed #70645
spell-check

00:01:40

 
  Process
failed #70650
doc

00:02:08

passed #70651
doc-classic

00:01:12

failed #70652
proof-state

00:05:33

passed #70648
validate

00:05:41

passed #70649
validate-classic

00:02:24

 
Name Stage Failure
failed
proof-state Process
Collecting proof state for ./analysis/abstract/i_and_w_auxillary.v...
Collecting proof state for ./analysis/abstract/rs_jlfp_rta.v...
Collecting proof state for ./analysis/abstract/abstract_seq_rta.v...
Collecting proof state for ./analysis/abstract/ideal_jlfp_rta.v...
Collecting proof state for ./analysis/abstract/ideal_abstract_rta.v...
Collecting proof state for ./analysis/abstract/restricted_supply_rta.v...
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
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
doc Process
Anomaly
"Uncaught exception Library.Faulty("/builds/sbozhko/rt-proofs/analysis/facts/preemption/job/preemptive.vo")."
Please report at http://coq.inria.fr/bugs/.

make: *** [Makefile:696: analysis/facts/preemption/task/preemptive.glob] Error 129
make: *** Waiting for unfinished jobs....
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
failed
1.9.0-coq-8.9 Build
# 
# 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.10.0-coq-8.9 Build
# 
# 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
spell-check Build
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'pred'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'proc'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'sched'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'simpl'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'tsk'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'upp'
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1
failed
proof-length Build
Warning: new long proof of exists_busy_interval_from_total_workload_bound in ./analysis/facts/busy_interval/carry_in.v:248!
Warning: new long proof of instantiated_interference_and_workload_consistent_with_sequential_tasks in ./results/edf/rta/bounded_pi.v:232!
Warning: new long proof of instantiated_interference_and_workload_consistent_with_sequential_tasks in ./results/fixed_priority/rta/bounded_pi.v:194!
Warning: new long proof of todo2 in ./analysis/abstract/restricted_supply_rta.v:530!
Warning: new long proof of interference_plus_sched_le_serv_of_task_plus_task_interference_job in ./analysis/abstract/abstract_seq_rta.v:396!
Checked 1901 proofs in 330 files, while skipping 149 known long proofs.
Running after_script
Uploading artifacts for failed job
ERROR: Job failed: exit code 1