Skip to content
Snippets Groups Projects
Select Git revision
  • classic-prosa protected
  • embed_arr_seq_uniq
  • fset
  • master default protected
  • prepare_MC_PR
  • tutorial
  • wip-hunspell
  • v0.5 protected
  • v0.4 protected
  • v0.3 protected
  • v0.2 protected
  • v0.1 protected
12 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.09Sep28Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713104328Oct27222016151413126130Sep2925221716151110987643128Aug26252418171211654331Jul302928272524222117Proved optimality of work-conserving EDF schedulesAdd Request Bound FunctionsTwo small lemmasCoq 8.10 no longer supported since #104add notion of offset, job index and proof of periodic arrival timesimprove the EDF optimality proof by reasoning about prefixesnote that basic readiness is non-clairvoyantnote some trivial facts about schedules with a shared prefixstill allow compilation with mathcomp 1.10.0 & Coq 8.11still allow compilation with mathcomp 1.10.0fix deprecation warning in classic global schedulefix name clash in classicFixed error in classicReplaced `omega` with `lia`Fixed compilation errors (without classic)update opam spec fileCI: remove older versions no longer supportedCI: add new jobs for mathcomp 1.11 and Coq 8.12CI: don't hardcode version multiple timesadd ideal uniprocessor reference schedulerreplace_at does not need decidable equalityadd readiness properties and facts on backloggedadd notion of a shared identical schedule prefixadditional minor lemmas on job arrivalsadd trivial replace_at definition rewriting lemmageneralize notion of jobs_backlogged_atadd function to generate uniprocessor schedulesupdate ack configmake --only-classic skip prosa.implementation moduleguidelines: add a section about backward vs forward reasoningfix injection warnings in single-cost sustainability reductionprosa classic: move import out of section to fix warningfix some warnings in prosa.classic.util.tacticssuppress warnings in prosa.util.seqsetfix warnings in prosa.util.search_argresolve warnings related to eq_big_permAdded spell command to MakefileRemoved verbatim text from spell-checkerImproved guidelineAdded guideline