Add periodic task model

12 jobs for v0.4 in 13 minutes and 8 seconds (queued for 2 seconds)
latest
Status Job ID Name Coverage
  Build
passed #81697
1.9.0-coq-8.10

00:01:53

passed #81698
1.9.0-coq-8.10-classic

00:05:51

passed #81701
1.9.0-coq-8.9

00:02:26

failed #81702
allowed to fail
1.9.0-coq-dev

00:00:03

failed #81703
allowed to fail
latest-coq-8.10

00:01:45

passed #81699
proof-length

00:00:08

passed #81700
spell-check

00:00:14

 
  Process
passed #81706
doc

00:00:18

failed #81707
doc-classic

00:07:13

passed #81708
proof-state

00:03:24

passed #81704
validate

00:04:44

passed #81705
validate-classic

00:07:15

 
Name Stage Failure
failed
doc-classic Process
COQDOC -d html 
$ mv html with-proofs
$ make gallinahtml -j ${NJOBS}
"coqc" -q -w -notation-overriden,-parsing -R . prosa classic/implementation/uni/basic/fp_rta_example.v
COQDOC -d html -g
$ mv html without-proofs
$ make htmlpretty -j ${NJOBS}
make: *** No rule to make target 'htmlpretty'. Stop.
ERROR: Job failed: exit code 1
failed
latest-coq-8.10 Build
File "./results/edf/rta/bounded_pi.v", line 548, characters 12-57:
Error: The LHS of MIN
(minn (A + ε + D tsk - D tsko) Δ)
does not match any subterm of the goal

make[1]: *** [Makefile:673: results/edf/rta/bounded_pi.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:321: all] Error 2
ERROR: Job failed: exit code 1
failed
1.9.0-coq-dev Build
Running with gitlab-runner 13.1.1 (6fbc7474)
on MPI-SWS shared runner docker 4 VmNnd6_F
Preparing the "docker" executor
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: manifest unknown: manifest unknown (docker.go:119:1s)