Merge branch 'jonathan' of gitlab.mpi-sws.org:mlesourd/rt-proofs into jonathan

6 jobs for jonathan in 6 minutes and 18 seconds (queued for 1 second)
latest
Status Job ID Name Coverage
  Build
passed #40404
1.8.0-coq-8.8

00:02:04

passed #40406
1.9.0-coq-8.9

00:02:05

failed #40405
allowed to fail
1.9.0-coq-dev

00:00:14

 
  Process
passed #40408
doc

00:03:06

failed #40409
proof-length

00:00:13

passed #40407
validate

00:04:12

 
Name Stage Failure
failed
proof-length Process There is an unknown failure, please try again
Downloading artifacts for 1.9.0-coq-8.9 (40406)...
Downloading artifacts from coordinator... ok id=40406 responseStatus=200 OK token=Ep-4vR-X
$ scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
Warning: new long proof of correction_lemma_UTT in ./restructuring/analysis/analysis_up_to_t/periodic_jitter_propagation_up_to_t.v:457!
Warning: new long proof of induction_lemma_UTT in ./restructuring/analysis/analysis_up_to_t/periodic_jitter_propagation_up_to_t.v:524!
Warning: new long proof of periodic_jitter_infinite in ./restructuring/model/arrival/periodic_jitter_up_to_t.v:129!
Warning: new long proof of dependency_arrival_bound_WCRT in ./restructuring/analysis/analysis_up_to_t/periodic_jitter_propagation_up_to_t.v:183!
Checked 1473 proofs in 230 files, while skipping 159 known long proofs.
ERROR: Job failed: exit code 1
failed
1.9.0-coq-dev Build There is an unknown failure, please try again
COQC util/powerset.v
COQC util/seqset.v
File "./util/seqset.v", line 19, characters 42-52:
Error: The reference mkPredType was not found in the current environment.

make[1]: *** [Makefile:659: util/seqset.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:321: all] Error 2
ERROR: Job failed: exit code 1