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.022Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9512Oct19Sep417Jul5Jan14Dec710Jan25Nov26Oct191866Sep5Aug317Jul151413128Jun65May431Mar223Feb16141273120Jan1915141312109876529Dec181716151410987432130Nov242320181713Update the Installing Coq sectionAdd Contributing sectio (TODO)Add Coq installation instructions to tutorialCI: exclude doc/ from comments spell-checkaddress some spelling issuesfilter backticks in commentsCI: compile the tutorial with alectryonMakefile: add a `make tutorial` targetInitiate a Prosa TutorialRemove unused sectionDeprecate ltn_leq_transRestore compatibility with Coq 8.13examples of how to avoid `apply with`Rename arguments of [apply _ with (NAME0 := _)]update Alectryon imagecoqdoc: remove unnecessary --coqlib flagbump supported Coq and mathcomp versions and update CIdefine `service_on` in the class `ProcessorState`change [job_task j = tsk] to [job_of_task tsk j]update coding guidlines (require external deps first)Fix some AdmittedfsetfsetRequire external libraries first[WIP] Replace seq with finite setsEmbeds arrival_uniq into arrival sequencesembed_arr_seq_u…embed_arr_seq_uniqadd an RTA for FIFO scheduling based on aRTAadd new helper lemma about RBFIntroduce extrapolated arrival curve Add bounded tardiness definitionFix a comment in job.vnew lemma about rbfremoved assumption job_of_task and restructured proofstwo new utility lemmas on FIFO and job completionComment fixes in filesnote equivalence of two ways of constraining `workload_of_jobs`add two new utility lemmas about sums over set partitionsadd rewriting lemma on the workload of "all other jobs"clean up in util/unit_growth.vadd basic facts about the FIFO scheduling policyadd a stronger notion of priority policy complianceintroduce the job-level predicate `preempted_at`