Polished wc_trans

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

00:01:34

passed #54091
1.9.0-coq-8.10-classic

00:02:39

passed #54094
1.9.0-coq-8.9

00:01:34

failed #54095
allowed to fail
1.9.0-coq-dev

00:00:01

passed #54096
allowed to fail
latest-coq-8.10

00:01:34

passed #54092
proof-length

00:00:22

failed #54093
spell-check

00:00:32

 
  Process
passed #54099
doc

00:00:22

passed #54100
doc-classic

00:00:28

failed #54101
proof-state

00:01:10

passed #54097
validate

00:00:49

passed #54098
validate-classic

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
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
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)