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.015Jul14116130Jun27May26161296519Apr1413725Mar24181716114325Feb232218171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120JanMathComp 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.definitionsimprove the bound on arrival blocking under EDFRename [ideal_schedule] into [ideal.schedule]add documentation for rt_[e]auto tacticsadd lemma relating task cost and task rbfAdd proper sequence of bullets to style guidelinesintroduce "greedy" concrete arrival sequencemodify definitions of priority policy complianceadd definitions of concrete tasks and jobs reorganize `util.sum` and add some commentsSimplify proof of sum_of_onesRemove sum0Simplify proof of sum_majorant_eqnRemove sum_seq_cond_gt0PSimplify proof of sumnB_natSimplify proof of leq_sum_seq_predSimplify proof of {l,}eq_sum_seq