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.028Jul2521191514116130Jun27May26161296519Apr1413725Mar24181716114325Feb232218171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65Mayadd 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 definitionprotect TODO comments from spell checkerprepare_MC_PRprepare_MC_PRAdd MathComp to wordlistMathComp PR TODO for sum_majorant_eqnMathComp PR TODO for sumnB_natMathComp PR TODO for leq_sum_seq_predMathComp PR TODO for {l,}eq_sum_seqMathComp PR TODO for leq_sum_sub_uniqMathComp PR TODO for sum_nat_eq0_natMathComp PR TODO for leq_subRL_implMathComp PR TODO for subdnDMathComp PR TODO for sum_nat_gt0Revert "reorganize `util.sum` and add some comments"exclude 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