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.028Jan2011Nov109828Sep207129Aug25181084128Jul2521191514116130Jun27May26161296519Apr1413725Mar24181716114325Feb232218171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct1918More qualified import of mathcomp.zidfy.ssrZ mastermastergeneralize abstract RTAadd lemmas about job relationsreplace [intros] with [move]add reflection for negated priority inversionoptimize importsimprove tabulation and commentsimprove tacticspreserve 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 functions