Skip to content

GitLab

[WIP] close one more lemma

16 jobs for !171 with priority_inversion in 21 minutes and 25 seconds (queued for 23 seconds)
merge request
6dd29bd5
1 related merge request: !171 Generalize priority inversion
Name Stage Failure
failed
validate Process 
-    prosa.results.fixed_priority.rta.bounded_pi.instantiated_i_and_w_are_consistent_with_schedule
-    prosa.results.fixed_priority.rta.bounded_pi.instantiated_task_interference_is_bounded
-    prosa.results.fixed_priority.rta.bounded_nps.priority_inversion_is_bounded
-    prosa.results.fixed_priority.rta.bounded_pi.instantiated_busy_intervals_are_bounded
   
 * Constants/Inductives relying on type-in-type: <none>
   
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
failed
spell-check Build 
./results/fixed_priority/rta/bounded_pi.v: potentially misspelled word 'ohep'
./results/fixed_priority/rta/bounded_pi.v: potentially misspelled word 'orP'
./results/fixed_priority/rta/bounded_pi.v: potentially misspelled word 'proc'
./results/fixed_priority/rta/bounded_pi.v: potentially misspelled word 'rbf'
./results/fixed_priority/rta/bounded_pi.v: potentially misspelled word 'rta'
./results/fixed_priority/rta/bounded_pi.v: potentially misspelled word 'sched'
./results/fixed_priority/rta/bounded_pi.v: potentially misspelled word 'subst'
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
failed
proof-length Build 
Using docker image sha256:82926ff1b66881196388acfc72b3c8781ee5733d72534271853802d8d6e2e60e for python:3-alpine with digest python@sha256:397ebe8c3d80a076dad10287f69b143c93e5606acfa4709b0736f5a3b4c9bcf4 ...
$ scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
Warning: new long proof of A_is_in_concrete_search_space in ./results/fifo/rta.v:226!
Warning: new long proof of A_is_in_concrete_search_space in ./results/fixed_priority/rta/bounded_pi.v:189!
Warning: new long proof of uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments in ./results/fixed_priority/rta/bounded_nps.v:165!
Warning: new long proof of A_is_in_concrete_search_space in ./results/edf/rta/bounded_pi.v:575!
Checked 2113 proofs in 363 files, while skipping 158 known long proofs.
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1