all important proof sketches done

17 jobs for oio in 10 minutes and 38 seconds (queued for 5 seconds)
Status Job ID Name Coverage
  Build
passed #84058
1.10.0-coq-8.10

00:05:29

passed #84059
1.10.0-coq-8.11

00:10:36

passed #84057
1.10.0-coq-8.9

00:10:38

passed #84055
1.9.0-coq-8.10

00:10:37

passed #84056
1.9.0-coq-8.11

00:10:35

passed #84054
1.9.0-coq-8.9

00:10:22

passed #84060
build-for-process

00:03:44

passed #84061
build-for-process-classic

00:03:35

failed #84064
allowed to fail
coq-8.10

00:07:04

failed #84065
allowed to fail
coq-dev

00:05:51

failed #84062
proof-length

00:01:11

failed #84063
spell-check

00:01:26

 
  Process
passed #84068
doc

00:00:22

passed #84069
doc-classic

00:00:34

failed #84070
proof-state

00:02:14

passed #84066
validate

00:02:04

passed #84067
validate-classic

00:01:10

 
Name Stage Failure
failed
proof-state Process
Collecting proof state for ./results/edf/rta/bounded_pi.v...
Collecting proof state for ./results/edf/rta/floating_nonpreemptive.v...
Collecting proof state for ./results/fixed_priority/rta/bounded_nps.v...
Collecting proof state for ./results/fixed_priority/rta/fully_preemptive.v...
Collecting proof state for ./results/fixed_priority/rta/fully_nonpreemptive.v...
Collecting proof state for ./results/fixed_priority/rta/bounded_pi.v...
Collecting proof state for ./results/fixed_priority/rta/limited_preemptive.v...
Collecting proof state for ./results/fixed_priority/rta/floating_nonpreemptive.v...
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.
ERROR: Job failed: exit code 1
failed
coq-dev Build
'opam install -y -v -j 2 coq-prosa' failed.


<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
ERROR: Job failed: exit code 1
failed
spell-check Build
./analysis/facts/sporadic.v: potentially misspelled word 'lt'
./analysis/facts/sporadic.v: potentially misspelled word 'ltnP'
./analysis/facts/sporadic.v: potentially misspelled word 'mem'
./analysis/facts/sporadic.v: potentially misspelled word 'nat'
./analysis/facts/sporadic.v: potentially misspelled word 'orP'
./analysis/facts/sporadic.v: potentially misspelled word 'ssromega'
./analysis/facts/sporadic.v: potentially misspelled word 'tsk'
./analysis/facts/sporadic.v: potentially misspelled word 'uniq'
ERROR: Job failed: exit code 1
failed
proof-length Build
Executing "step_script" stage of the job script
$ scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
Warning: new long proof of eq_size_of_arrivals_at in ./analysis/facts/oi.v:689!
Warning: new long proof of corresponding_job_arrives in ./analysis/facts/oi.v:850!
Warning: new long proof of nat_4 in ./analysis/facts/oi.v:452!
Warning: new long proof of job_arr_index in ./analysis/facts/oi.v:625!
Warning: new long proof of job_sep_periodic_induction in ./analysis/facts/periodic/index.v:55!
Checked 1903 proofs in 331 files, while skipping 149 known long proofs.
ERROR: Job failed: exit code 1