Skip to content

GitLab

some initial fixes

15 jobs for !116 with generalize_aRTA in 4 minutes and 30 seconds (queued for 3 seconds)
latest merge request
d91e7019
1 related merge request: !116 Draft: Generalize ideal aRTA
Name Stage Failure
failed
coq-8.13 Build 
# Error: Last block to end has name CumulativePriorityInversion.
# 
# make[1]: *** [Makefile:738: analysis/definitions/priority_inversion.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:343: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
coq-dev Build 

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+- 
- No changes have been performed
'opam install -y -v -j 2 coq-prosa' failed.
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
proof-state Build 
to use this functionality in finished proof scripts.
[require-in-section,fragile]
File "./analysis/definitions/priority_inversion.v", line 107, characters 0-22:
Error: Last block to end has name CumulativePriorityInversion.

make: *** [Makefile:781: analysis/definitions/priority_inversion.vo] Error 1
make: *** Waiting for unfinished jobs....
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
1.11.0-coq-8.12 Build 
# Error: Last block to end has name CumulativePriorityInversion.
# 
# make[1]: *** [Makefile:734: analysis/definitions/priority_inversion.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:339: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
failed
1.12.0-coq-8.13 Build 
# 
# COQC classic/model/schedule/global/response_time.v
# make[1]: *** [Makefile:738: analysis/definitions/priority_inversion.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:343: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
failed
1.11.0-coq-8.11 Build 
# Error: Last block to end has name CumulativePriorityInversion.
# 
# make[1]: *** [Makefile:696: analysis/definitions/priority_inversion.vo] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:327: all] Error 2

'opam install -y -v -j 2 coq-prosa' failed.
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
spell-check Build 
./analysis/facts/busy_interval/busy_interval.v: potentially misspelled word 'Qed'
./analysis/facts/busy_interval/busy_interval.v: potentially misspelled word 'ResponseTimeBoundFromBusyInterval'
./analysis/facts/busy_interval/busy_interval.v: potentially misspelled word 'forall'
./analysis/facts/busy_interval/busy_interval.v: potentially misspelled word 'leq'
./analysis/facts/busy_interval/busy_interval.v: potentially misspelled word 'posnP'
./analysis/facts/busy_interval/busy_interval.v: potentially misspelled word 'sched'
./model/processor/restricted_supply.v: potentially misspelled word 'complemental'
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
compile Build 
[require-in-section,fragile]
File "./analysis/definitions/priority_inversion.v", line 107, characters 0-22:
Error: Last block to end has name CumulativePriorityInversion.

make[1]: *** [Makefile:738: analysis/definitions/priority_inversion.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:343: all] Error 2
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
1.10.0-coq-8.11 Build 

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+- 
- No changes have been performed
'opam install -y -v -j 2 coq-prosa' failed.
Cleaning up file based variables
ERROR: Job failed: exit code 1
failed
proof-length Build 
$ scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
Warning: new long proof of no_idle_time_within_non_quiet_time_interval in ./analysis/facts/busy_interval/busy_interval.v:332!
Warning: new long proof of fk in ./analysis/abstract/ideal_jlfp_rta.v:656!
Warning: new long proof of busy_interval_has_uninterrupted_service in ./analysis/facts/busy_interval/busy_interval.v:520!
Warning: new long proof of todo2 in ./analysis/abstract/restricted_supply_rta.v:531!
Warning: new long proof of todo6 in ./analysis/abstract/ideal_abstract_rta.v:122!
Checked 2106 proofs in 363 files, while skipping 149 known long proofs.
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1