Martin Constantino–Bodin authored 3 years ago and Björn Brandenburg committed 3 years ago

`esy` is an `npm`-like package manager and build tool designed for
reproducibility, by preventing the use of unlisted dependencies and
pinning the exact version of each of these (a bit like `opam`, but
with more guarantees).

A nice feature of `esy` is ease of installation:

1. Install `esy` through `npm`. (However, note that `esy` is not a
   JavaScript program; the `esy` project just uses `npm` as a code
   hoster.

2. Run `esy` in the Prosa repository. 

This will download and compile all dependencies and compile the
repository. (On the flip side, this also means that Coq will be
compiled, so the first time, compilation will be slow.)

See the README.md file for usage instructions. 

See also the discussion: #80

For more information about `esy`, see: https://esy.sh/

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

`Task` should obviously be of type `TaskType`.

Mariam Vardishvili authored 3 years ago and Björn Brandenburg committed 3 years ago

...to match the description in the aRTA paper.

Mariam Vardishvili authored 3 years ago and Björn Brandenburg committed 3 years ago

The lemma [instantiated_busy_interval_equivalent_edf_busy_interval] actually does not depend on EDF.

mathcomp has deprecated `iota_add` in favor of `iotaD`.

However, `iotaD` wasn't added until mathcomp 1.12, so this patch breaks
compatibility with earlier versions.

Added a few lemmas to util/div_mod that are needed for POET

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

Coq 8.11, Coq 8.12, ssreflect 1.10, and ssreflect 1.11
are no longer supported

Due to whatever the CI environment does to cache and restore
intermediate result files, somehow `make validate` triggers some
spurious recompilation. To avoid confusing the checking script,
trigger any possible re-compilation steps before capturing the output
of `make validate`.

Closes #79

* use more concise name
* add cases with [is_true _] in addition to cases with [_ = true]

Currently, aRTA required [F] to be solution of equation
[A + F = task_rtct + IBF A (A + F)], this commit relaxes
this assumption to [A + F >= task_rtct + IBF A (A + F)]

Marco Maida authored 3 years ago and Björn Brandenburg committed 3 years ago

Added helper lemmas relating `valid_schedule` to job execution hps with hint.
Removed useless hps in aRTA.

Sergey Bozhko authored 4 years ago and Björn Brandenburg committed 3 years ago

With some misc. cleanups and reorganization thrown in.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

Add a few lemmas that will be useful later.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

also, removed one assumption in [eq_ind_in_seq]