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.027May26161296519Apr1413725Mar24181716114325Feb232218171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915improve 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_seqSimplify proof of leq_sum_sub_uniqSimplify proof of sum_pred_diffSimplify proof of sum_majorant_constantSimplify proof of sum_notin_rem_eqnSimplify sum_nat_gt0Generalize and simplify proof of sum_nat_eq0_natRewrite 2 proofs in more ssreflect styleRemove add_mul_diffRemove exists_or_not_add_mul_casesPrepare leq_subRL_impl for MathComp PRPrepare subdnD for MathComp PRRemove leq_addkRemove subn_abbaadd lemmas about [service_of_jobs]introduce the notion of "total service of jobs"rename `np_uni_schedule` to `pmc_uni_schedule`add alternate interpretation of numeric prioritiesmake naming consistent and fix commentsPut a "How to read this tutorial" section upfronttutorialtutorialfix the `job_preemption_points` name clashCI: fix opam-triggered recompilationdemonstrate arrival-model conversion with an exampleenable periodic->RBF auto conversionenable automatic arrival-model conversion