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.010Nov9828Sep207129Aug25181084128Jul2521191514116130Jun27May26161296519Apr1413725Mar24181716114325Feb232218171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct19186preserve Classic Prosa upon retirementclassic-prosaclassic-prosaretire classic Prosaupdate the OPAM fileadd .mailmap use custom alectryon driver to comply with DSGVO (Germany privacy law)Adapt to https://github.com/coq/coq/pull/16004Update POET's support code to match the newer aRTA blocking boundv0.5v0.5CI: bump preferred Coq versiongeneralize one proof related to FPadd remaining POET support filesdocument some recently discussed guidelinesuse `valid_arrival_sequence` predicate more consistently revise the FIFO RTA documentationsimplify FIFO cumulative priority inversion bounddon't duplicate [odflt] from [ssrfun]fix spelling and markup issues uncovered by `hunspell`wip-hunspellwip-hunspellCI: update custom dictionaryCI: detect & remove multiline verbatim blocksCI: switch spellchecking to `hunspell`add GEL RTAadd task-related refinements and helper lemmasstreamline proof of EDF `total_workload_shorten_range` lemmaadd `workload_of_jobs` filtering lemmasadd `arrivals_between` filtering lemmasgeneralize some parts of the EDF aRTA instantiationgeneralize priority inversion definitionadd lemma about [service_of_jobs_at]add auxiliary lemmas about ideal scheduleadd computed fixpoints for FP-FP RTAadd utilities for finding fixpoints of functionsadd lemmas on misc. properties of total RBF variantsadd a lemma on the monotonicity of sums of monotonic functionsfix comments for hypothesisclean up proofsremove sequential tasks assumption from EDF RTAmake assumption weakergeneralize lemma for bound on busy windowadd more lemmas to [basic_rt_facts]add lemmas about [workload_of_jobs]simplify GEL definition