Polish one file

14 jobs for aSBF in 22 minutes and 2 seconds (queued for 5 seconds)
latest
Status Job ID Name Coverage
  Build
passed #93590
1.10.0-coq-8.11

00:06:51

passed #93591
1.11.0-coq-8.11

00:06:16

passed #93592
1.11.0-coq-8.12

00:06:04

passed #93593
build-for-process

00:03:25

passed #93594
build-for-process-classic

00:20:48

passed #93597
coq-8.12

00:06:36

passed #93598
coq-dev

00:05:31

failed #93595
proof-length

00:00:08

failed #93596
spell-check

00:16:32

 
  Process
passed #93601
doc

00:01:20

passed #93602
doc-classic

00:00:35

failed #93603
proof-state

00:02:49

passed #93599
validate

00:00:54

passed #93600
validate-classic

00:01:13

 
Name Stage Failure
failed
spell-check Build
./analysis/abstract/i_and_w_auxillary.v: potentially misspelled word 'auxillary'
./analysis/abstract/i_and_w_auxillary.v: potentially misspelled word 'eqP'
./analysis/abstract/i_and_w_auxillary.v: potentially misspelled word 'eqn'
./analysis/abstract/restricted_supply_rta.v: potentially misspelled word 'del'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'jhp'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'ohep'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'sched'
./analysis/abstract/ideal_jlfp_rta.v: potentially misspelled word 'todo'
ERROR: Job failed: exit code 1
failed
proof-state Process
Collecting proof state for ./results/fixed_priority/rta/fully_nonpreemptive.v...
Collecting proof state for ./results/fixed_priority/rta/limited_preemptive.v...
Collecting proof state for ./implementation/definitions/ideal_uni_scheduler.v...
Collecting proof state for ./results/fixed_priority/rta/floating_nonpreemptive.v...
Collecting proof state for ./implementation/definitions/generic_scheduler.v...
Collecting proof state for ./implementation/facts/ideal_uni/prio_aware.v...
Collecting proof state for ./implementation/facts/ideal_uni/preemption_aware.v...
Collecting proof state for ./implementation/facts/generic_schedule.v...
ERROR: Job failed: exit code 1
failed
proof-length Build
Executing "step_script" stage of the job script
$ scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
Checked 2076 proofs in 359 files, while skipping 149 known long proofs.
Warning: new long proof of no_idle_time_within_non_quiet_time_interval in ./analysis/facts/busy_interval/busy_interval.v:338!
Warning: new long proof of busy_interval_has_uninterrupted_service in ./analysis/facts/busy_interval/busy_interval.v:527!
Warning: new long proof of todo2 in ./analysis/abstract/restricted_supply_rta.v:531!
Warning: new long proof of interference_plus_sched_le_serv_of_task_plus_task_interference_job in ./analysis/abstract/abstract_seq_rta.v:418!
Warning: new long proof of todo6 in ./analysis/abstract/ideal_abstract_rta.v:122!
ERROR: Job failed: exit code 1