Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa protected
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.010Nov9828Sep207129Aug25181084128Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb1614add .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 definitionexclude the blocking bound from the EDF search spaceadjust FP NPS PI-blocking bound proof to narrowed definitionnarrow priority-inversion bound to jobs with non-zero cost