GitLab

Now advise to just install the Coq platform

The tutorial document, based on RST, is too complex for the simple CI
spell check. Please use your editor's spell checker when editing the
tutorial.

Sergey Bozhko authored Feb 09, 2022 and Björn Brandenburg committed Feb 16, 2022

From changelog of Coq version 8.15:
Changed: [apply with] does not rename arguments unless using
compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan
Gilbert).

So, this commit replaces all occurrences of [apply L with (NAME0 := V)]
to [apply L with (NAME := V)]

The default works just fine (nowadays), so let's use that.

Martin Constantino–Bodin authored Feb 22, 2021 and Björn Brandenburg committed Feb 16, 2022

... instead of `service_in`, to mirror the way
the primitive `scheduled_on` is used to realize
`scheduled_in`.

Sergey Bozhko authored Feb 16, 2022 and Björn Brandenburg committed Feb 16, 2022

There are quite a few places where hypotheses about the task of a job are simply stated as equality (even though a proper predicate exists). This patch replaces the equalities with the predicate.

As Pierre pointed out in [MR187](!187),
we don't want updates in any of our dependencies to accidentally
shadow Prosa symbols. Hence, always import Prosa modules last to make
sure Prosa symbols "win" any name clashes.

This way, an addition in external libraries
cannot shadow a definition in Prosa.

Kimaya Bedarkar authored Feb 09, 2022 and Björn Brandenburg committed Feb 09, 2022

Provide an RTA for FIFO scheduling on ideal uniprocessors based on an
instantiation of abstract RTA. The provided RTA is works for tasks
described by arbitrary arrival curves and is independent of the
workload's preemption model (since FIFO schedules are necessarily
non-preemptive). 

Kimaya Bedarkar authored Jan 31, 2022 and Björn Brandenburg committed Jan 31, 2022

* Added a lemma for proving `rbf` at `\varepsilon` is more than 0. This is a general fact which can be used in the FIFO RTA to simplify a proof. 
* Changed `1` to `\varepsilon` in one of the existing RBF lemmas for uniformity.

Sergey Bozhko authored Jan 13, 2022 and Björn Brandenburg committed Jan 13, 2022

Add an implementation of arrival curves via fast
extrapolation of a finite arrival-curve prefix.