Polished wc_trans

12 jobs for work-conserving-edf in 3 minutes and 35 seconds (queued for 3 seconds)
latest
Status Name Job ID Coverage
  Build
passed 1.9.0-coq-8.10 #54090

00:01:34

passed 1.9.0-coq-8.10-classic #54091

00:02:39

passed 1.9.0-coq-8.9 #54094

00:01:34

failed 1.9.0-coq-dev #54095
allowed to fail

00:00:01

passed latest-coq-8.10 #54096

00:01:34

passed proof-length #54092

00:00:22

failed spell-check #54093

00:00:32

 
  Process
passed doc #54099

00:00:22

passed doc-classic #54100

00:00:28

failed proof-state #54101

00:01:10

passed validate #54097

00:00:49

passed validate-classic #54098

00:00:53

 
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
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)
failed
spell-check Build
Removing util/supremum.vo
Removing util/tactics.glob
Removing util/tactics.vo

Skipping Git submodules setup
$ scripts/flag-typos-in-comments.sh `find . -iname '*.v' ! -path './classic/*'`
./analysis/transform/facts/wc_correctness.v: potentially misspelled word 'istant'
./analysis/transform/wc_trans.v: potentially misspelled word 'wc'
ERROR: Job failed: exit code 1