Skip to content
Snippets Groups Projects

Move lemma [early_hep_job_is_scheduled] to separate file

Merged Move lemma [early_hep_job_is_scheduled] to separate file
sbozhko/rt-proofs:move_lemma into master
All threads resolved!
Merged Sergey Bozhko requested to merge sbozhko/rt-proofs:move_lemma into master
All threads resolved!

Partially solves #78 (closed)

  • Move file facts/edf.v to facts/priority/edf.v
  • Move lemma early_hep_job_is_scheduled to a separate file so it no longer depends on EDF schedule
  • Dependence on ideal schedule is still present, because early_hep_job_is_scheduled uses lemma scheduling_of_any_segment_starts_with_preemption_time which assumes an ideal scheduler

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Sergey Bozhko added 1 commit

    added 1 commit

    • d7f0cc94 - move lemma [early_hep_job_is_scheduled] to separate file

    Compare with previous version

  • Sergey Bozhko resolved all threads

    resolved all threads

  • Björn Brandenburg resolved all threads

    resolved all threads

  • Björn Brandenburg added 2 commits

    added 2 commits

    • 3ab704f7 - 1 commit from branch RT-PROOFS:master
    • 9cc286c2 - move lemma [early_hep_job_is_scheduled] to separate file

    Compare with previous version

  • Björn Brandenburg enabled an automatic merge when the pipeline for 9cc286c2 succeeds

    enabled an automatic merge when the pipeline for 9cc286c2 succeeds

  • Björn Brandenburg merged

    merged

  • Kimaya Bedarkar mentioned in issue #78 (closed)

    mentioned in issue #78 (closed)

    • Please register or sign in to reply