More polish to comments

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

00:02:00

passed #53984
1.9.0-coq-8.10-classic

00:03:02

passed #53987
1.9.0-coq-8.9

00:01:58

failed #53988
allowed to fail
1.9.0-coq-dev

00:00:02

passed #53989
allowed to fail
latest-coq-8.10

00:01:58

passed #53985
proof-length

00:00:26

failed #53986
spell-check

00:00:33

 
  Process
passed #53992
doc

00:00:25

passed #53993
doc-classic

00:00:29

failed #53994
proof-state

00:01:08

passed #53990
validate

00:00:51

passed #53991
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 b027b6b5
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)