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.021Jul191514116130Jun27May26161296519Apr1413725Mar24181716114325Feb232218171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar2remove 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 outputadd --without-refinements option to ./create_makefile.shopam: constrain min. supported versionadd refinements needed for POETCI: add CoqEAL dependencyCI: factor out common codeCI: simplify the setup to use a single stageremove redundant clause from `busy_intervals_are_bounded_by`improve readability of analysis.abstract.definitions