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.01Apr30Mar29272423171615131042128Feb272221201428Jan2011Nov109828Sep207129Aug25181084128Jul25211914116130Jun27May26161296519Apr1413725Mar24181716114325Feb18171615141311931Jan1315Dec729Nov252423543214Oct1211765430Sep29272217161511830Jul27261918Mar118129Jan211Dec25Sep2322928Aug271065430Jul9830Jun19May113Apr131Mar271027Feb2619111023Jan2121Dec2019181210420Nov19181511531Oct29242316151124Sep231730Aug2321201324Jul19227Jun26251312526May191613127329Apr9CI: check that POET certificates keep workingmove misplaced code out of `prosa.analysis.facts.busy_window`factor out ideal uniproc from carry-in lemmasgeneralize `low_service_implies_existence_of_idle_time`introduce a generic notion of `is_idle`rename `is_idle` -> `ideal_is_idle`cleanup: remove some stale references to ideal uniprocessorremove ideal uniprocessor assumption from TDMAfix outdated commentsadd workload-by-task partitioning lemmaweaken assumption of `sum_over_partitions_eq`generalize FP ⊂ GEL proof to any self-suspension modelintroduce the class of sequential readiness modelsgeneralize a number of core definitions and factsrelate ideal uniprocessor to `scheduled_job_at`introduce a generic notion of scheduled job(s)Makefile: add 'make proof-length'remove unused context declarationfix CoqdocJS handling of apostrophes embedded in identifiersprove that GEL conditionally generalizes FPadd lemma on sequential_tasksnote that GEL trivially generalizes both EDF and FIFOfix `make vacuum` if no `_CoqProject` is presentRevert "Restore compatibility with Coq 8.13"Bump lower bound for Coq to >= 8.16Bump lower bound on MathComp to >= 1.16.0Put mangle-names in a separate CI targetUse mathcomp's int instead of stdlib's ZAdd missing lemma not_hep_hp_taskProve a splitting fact about interferenceUse _dec definitions directlyMoving interference definitions out of iw_instantiationDefinition of ELFDefinitions of hp_task and its propertiesintroduce predicates on task- and job-level priority policiesupdate dot filesfix spell-checking issues in *.md filesalso spell-check *.md filesWarning about autogenerated namesWarning about implicit arguments