Pipeline · Sergey Bozhko / rt-proofs

Polish one file

14 jobs for aSBF in 22 minutes and 2 seconds (queued for 5 seconds)

Status	Job ID	Name
Build
passed	#93590	1.10.0-coq-8.11	00:06:51 Sep 24, 2020
passed	#93591	1.11.0-coq-8.11	00:06:16 Sep 24, 2020
passed	#93592	1.11.0-coq-8.12	00:06:04 Sep 24, 2020
passed	#93593	build-for-process	00:03:25 Sep 24, 2020
passed	#93594	build-for-process-classic	00:20:48 Sep 24, 2020
passed	#93597	coq-8.12	00:06:36 Sep 24, 2020
passed	#93598	coq-dev	00:05:31 Sep 24, 2020
failed	#93595	proof-length	00:00:08 Sep 24, 2020
failed	#93596	spell-check	00:16:32 Sep 24, 2020

Process
passed	#93601	doc	00:01:20 Sep 24, 2020
passed	#93602	doc-classic	00:00:35 Sep 24, 2020
failed	#93603	proof-state	00:02:49 Sep 24, 2020
passed	#93599	validate	00:00:54 Sep 24, 2020
passed	#93600	validate-classic	00:01:13 Sep 24, 2020

	Name	Stage
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