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.05May19Apr1413725Mar24181716114325Feb232218171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan19151413add 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 conversionreorganize arrival model conversionsadd sporadic task -> arrival curve interpretationestablish an arrival bound for sporadic tasksadd auxiliary lemmas on `{task_}arrivals_between`establish that `arrivals_between` is sortedadd lemma on `div_ceil` on integer multiplesclean up facts.sporadic.arrival_times