Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5
  • v0.4
  • v0.3
  • v0.2
  • v0.1
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.07Oct65430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep29252217161511move lemma [early_hep_job_is_scheduled] to separate fileadd lemmas to util/div_modadd lemmas to util/listdrop support of older versions of Coq and ssreflectCI: explicitly trigger recompilation in axiom checkCI: automatically check validation output for unexpected axiomsimprove tactic [convert_two_instants_into_instant_and_duration]relax assumption in aRTAautomatically use implications of `valid_schedule`FP: switch from basic readiness to sequential readinessEDF: switch RTA to `valid_schedule` hypothesisEDF ensures the `sequential_tasks` propertyadjust lemmas to work-bearing readinessremove ideal uniproc. assumption from some lemmas on `service_of_jobs`note basic `task_schedule` propertiesadd two helper lemmas on processor serviceadd notion `receives_service_at`move [Context] declaration out of the global contextfix description in behavior/job.vclean up in util/bigcat.vsmall clean up in util/step_function.vsmall clean up in util/seqset.vclean up in util/nondecreasing.vadd lemmas to util/div_mod.vclean up in util/lcmseq.vclean up in util/rel.vclean up util/minmax.vclean up util/list.vadd comments to file [util/div_mod.v]remove [util.counting.v]clean up `nat.v`misc. code and comments polishcleanup: coqdoc fixes and unnecessary ideal uniprocessor assumptionMakefile: allow alectryon to work in parallelCI: remove old proof-state scriptsCI: use custom Docker image for proof-state collectionCI: don't run expensive jobs in wip- branchesCI: use alectryon for proof-state displayadd alectryon wrapper script and `make alectryon` targetadd sequential and work-bearing readiness models