Polished lemmas

Status Job ID Name Coverage
  Build
passed #53666
1.9.0-coq-8.10

00:01:35

passed #53667
1.9.0-coq-8.10-classic

00:02:39

passed #53670
1.9.0-coq-8.9

00:01:33

failed #53671
allowed to fail
1.9.0-coq-dev

00:00:01

passed #53672
allowed to fail
latest-coq-8.10

00:01:34

failed #53668
proof-length

00:00:19

failed #53669
spell-check

00:00:28

 
  Process
passed #53675
doc

00:00:24

passed #53676
doc-classic

00:00:28

failed #53677
proof-state

00:01:10

passed #53673
validate

00:00:49

passed #53674
validate-classic

00:00:54

 
Name Stage Failure
failed
proof-state Process
Collecting proof state for ./analysis/facts/readiness/basic.v...
Collecting proof state for ./analysis/facts/tdma.v...
Collecting proof state for ./analysis/abstract/run_to_completion.v...
Collecting proof state for ./analysis/abstract/definitions.v...
Collecting proof state for ./analysis/abstract/search_space.v...
Collecting proof state for ./analysis/abstract/abstract_seq_rta.v...
Collecting proof state for ./analysis/abstract/abstract_rta.v...
Collecting proof state for ./analysis/abstract/ideal_jlfp_rta.v...
ERROR: Job failed: exit code 1
failed
spell-check Build
$ scripts/flag-typos-in-comments.sh `find . -iname '*.v' ! -path './classic/*'`
./model/schedule/weakly_work_conserving.v: potentially misspelled word 'NWC'
./model/schedule/weakly_work_conserving.v: potentially misspelled word 'cpu'
./model/schedule/weakly_work_conserving.v: potentially misspelled word 'forall'
./analysis/transform/facts/wc_correctness.v: potentially misspelled word 'TODO'
./analysis/transform/facts/wc_correctness.v: potentially misspelled word 'ication'
./analysis/transform/wc_trans.v: potentially misspelled word 'ification'
./analysis/transform/wc_trans.v: potentially misspelled word 'wc'
ERROR: Job failed: exit code 1
failed
proof-length Build
 * [new ref]         refs/pipelines/23112 -> refs/pipelines/23112
602cc6a..bf2fbe9 work-conserving-edf -> origin/work-conserving-edf
Checking out bf2fbe91 as work-conserving-edf...

Skipping Git submodules setup
$ scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
Warning: new long proof of mwa_finds_ready_jobs in ./analysis/transform/facts/wc_correctness.v:177!
Checked 1825 proofs in 320 files, while skipping 149 known long proofs.
ERROR: Job failed: exit code 1
failed
1.9.0-coq-dev Build
Running with gitlab-runner 12.5.0 (577f813d)
on MPI-SWS shared runner docker executor 2 686bfd3b
Using Docker executor with image mathcomp/mathcomp:1.9.0-coq-dev ...
Pulling docker image mathcomp/mathcomp:1.9.0-coq-dev ...
ERROR: Job failed: Error response from daemon: manifest for mathcomp/mathcomp:1.9.0-coq-dev not found (executor_docker.go:188:1s)