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.010Aug84128Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jandon'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 costadd utility lemmas on `\max_( r <- xs)` (bigmax)add fact about non-pathological arrival curvesaRTA clean-upfix various deprecation warningsremove unnecessary `unfold prefix`classic: fix deprecated mathcomp symbolsrename `prefix` -> `prefix_of`CI: bump mathcomp versionadd concrete job constructorupdate license, silence opam warningCI: account for proof irrelevance when checking validation output