From cf08f2ed2028f3d7d63b79eb985acaca6c17db60 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Thu, 9 Nov 2023 10:06:50 +0000
Subject: [PATCH] silence some warnings and change global behavior of
obligation tactic
Drops support for mathcomp 1.16.
---
.gitlab-ci.yml | 5 -----
README.md | 23 ++++++++++++-----------
behavior/ready.v | 2 --
behavior/schedule.v | 2 --
model/processor/multiprocessor.v | 6 +++---
model/processor/spin.v | 4 ++--
model/processor/varspeed.v | 2 +-
model/readiness/basic.v | 1 +
results/elf/rta/bounded_pi.v | 4 ++--
util/tactics.v | 7 +++++++
10 files changed, 28 insertions(+), 28 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4e296ed41..85f803ed2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -66,11 +66,6 @@ stages:
###################### The Jobs ######################
-1.16.0-coq-8.16:
- extends:
- - .build
- - .not_in_wip_branches
-
1.17.0-coq-8.17:
extends:
- .build
diff --git a/README.md b/README.md
index e1c750a57..3cb8e8450 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,12 @@
# Prosa: Formally Proven Schedulability Analysis
-This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016.
+This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016.
-From 2018–201, Prosa was further developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
+From 2018–201, Prosa was further developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
<center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
-Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome!
+Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome!
## Documentation
@@ -16,21 +16,21 @@ Up-to-date documentation for all branches of the main Prosa repository is availa
## Publications
-Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage.
+Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage.
### Classic Prosa
-All results published prior to 2020 used the "classic" version of Prosa as first presented at ECRTS'16. Classic Prosa has been superseded by this development and is no longer being maintained. Refer to [the `classic-prosa` branch](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/classic-prosa) to find this original version of Prosa.
+All results published prior to 2020 used the "classic" version of Prosa as first presented at ECRTS'16. Classic Prosa has been superseded by this development and is no longer being maintained. Refer to [the `classic-prosa` branch](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/classic-prosa) to find this original version of Prosa.
## Directory and Module Structure
The directory and module structure is organized as follows. First, the main parts, of which there are currently six.
-- [`behavior`](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
+- [`behavior`](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
- [`model`](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate. These models are *axiomatic* in the sense that they are collections of hypotheses and not necessarily backed by concrete implementations (but see below).
- [`analysis`](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
-- [`results`](results/): The `results` namespace contains all **high-level analysis results**.
+- [`results`](results/): The `results` namespace contains all **high-level analysis results**.
- [`implementation`](implementation/): This module collects concrete implementations of some of the axiomatic models and scheduling policies to which the results apply. These are used to instantiate (i.e., apply) high-level results in an assumption-free environment for concrete job and task types, which establishes the absence of contradictions in the axiomatic models refined by the implementations.
- [`implementation.refinements`](implementation/refinements/): The refinements needed by [POET](https://drops.dagstuhl.de/opus/volltexte/2022/16336/) to compute with large numbers, based on [CoqEAL](https://github.com/coq-community/CoqEAL).
@@ -48,6 +48,7 @@ Importing Prosa changes the behavior of ssreflect's `done` tactic by adding basi
```
Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
```
+Prosa overwrites the default obligation tactic of Coq with `idtac`. Refer [`util.tactics`](util/tactics.v) for details.
## Installation
@@ -104,7 +105,7 @@ Alternatively, `esy shell` opens a shell within its environment.
#### Dependencies
-Besides on Coq itself, Prosa depends on
+Besides on Coq itself, Prosa depends on
1. the `ssreflect` library of the [Mathematical Components project](https://math-comp.github.io),
2. the [Micromega support for the Mathematical Components library](https://github.com/math-comp/mczify) provided by `mczify`, and
@@ -165,13 +166,13 @@ To make things as smooth as possible, here are a couple of rules and guidelines
1. Always follow the project [coding and writing guidelines](doc/guidelines.md).
-2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times.
+2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times.
3. It's okay (and even recommended) to develop in a (private) dirty branch, but please clean up and re-base your branch (i.e., `git-rebase -i`) on top of the current master branch before opening a merge request.
4. Create merge requests liberally. No improvement is too small or too insignificant for a merge request. This applies to documentation fixes (e.g., typo fixes, grammar fixes, clarifications, etc.) as well.
-5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:" or "Draft:".
+5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:" or "Draft:".
6. We strive to have only "fast-forward merges" without merge commits, so always re-base your branch to linearize the history before merging. (WIP branches do not need to be linear.)
@@ -179,4 +180,4 @@ To make things as smooth as possible, here are a couple of rules and guidelines
8. If something seems confusing, please help with improving the documentation. :-)
-9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discussion, please file a ticket.
+9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discussion, please file a ticket.
diff --git a/behavior/ready.v b/behavior/ready.v
index bc759ae88..e4dc9e5b2 100644
--- a/behavior/ready.v
+++ b/behavior/ready.v
@@ -79,5 +79,3 @@ Section ValidSchedule.
properties are implied by jobs_must_be_ready_to_execute. *)
End ValidSchedule.
-
-Obligation Tactic := try done.
diff --git a/behavior/schedule.v b/behavior/schedule.v
index 9cb5b819e..4f1663845 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -104,5 +104,3 @@ Definition schedule {Job : JobType} (PState : ProcessorState Job) :=
[scheduled_on] and [service_on] are defined. Instead,
proofs must rely on basic lemmas about processor state classes. *)
Global Opaque scheduled_on service_on.
-
-Obligation Tactic := try done.
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index a0faaa1cc..995e7c6a5 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -52,7 +52,7 @@ Section Schedule.
[mps] on a given core [cpu] is exactly the supply provided by the
core-local state [(mps cpu)]. *)
Definition multiproc_supply_on
- (mps : multiprocessor_state) (cpu : processor num_cpus)
+ (mps : multiprocessor_state) (cpu : processor num_cpus)
:= supply_in (mps cpu).
(** Next, the service received by a given job [j] in a given
@@ -60,7 +60,7 @@ Section Schedule.
exactly the service given by [j] in the processor-local state
[(mps cpu)]. *)
Definition multiproc_service_on
- (j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
+ (j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= service_in j (mps cpu).
(** Finally, we connect the above definitions with the generic Prosa
@@ -82,7 +82,7 @@ Section Schedule.
[mps] is given by the sum of the service received across all individual
processors of the multiprocessor. *)
Lemma multiproc_service_in_eq : forall (j : Job) (mps : multiprocessor_state),
- service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu).
+ service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu).
Proof. reflexivity. Qed.
End Schedule.
diff --git a/model/processor/spin.v b/model/processor/spin.v
index 9cce1357f..083351ba7 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -57,7 +57,7 @@ Section State.
end.
End Service.
-
+
(** Finally, we connect the above definitions with the generic Prosa
interface for abstract processor states. *)
Program Definition pstate_instance : ProcessorState Job :=
@@ -68,6 +68,6 @@ Section State.
service_on := spin_service_on
|}.
Next Obligation. by move => j [] // s [] /=; case: eqP. Qed.
- Next Obligation. by move=> j [] //= j' _ /negbTE ->. Qed.
+ Next Obligation. by move => j [] // s [] /=; case: eqP. Qed.
End State.
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index 87393a987..098e7f4ca 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -64,7 +64,7 @@ Section State.
supply_on := varspeed_supply_on;
service_on := varspeed_service_on
|}.
- Next Obligation. by move=> j [] //= s n; case: eqP. Qed.
+ Next Obligation. by move=> j [] //= s ; case: eqP. Qed.
Next Obligation. by move=> j [] //= j' v _; case: ifP. Qed.
End State.
diff --git a/model/readiness/basic.v b/model/readiness/basic.v
index 7595ca7b8..032bb14f9 100644
--- a/model/readiness/basic.v
+++ b/model/readiness/basic.v
@@ -21,5 +21,6 @@ Section LiuAndLaylandReadiness.
{
job_ready sched j t := pending sched j t
}.
+ Next Obligation. by done. Qed.
End LiuAndLaylandReadiness.
diff --git a/results/elf/rta/bounded_pi.v b/results/elf/rta/bounded_pi.v
index c72931a47..c510de711 100644
--- a/results/elf/rta/bounded_pi.v
+++ b/results/elf/rta/bounded_pi.v
@@ -286,8 +286,8 @@ Section AbstractRTAforELFwithArrivalCurves.
move=> /andP[HEPj EP]; rewrite -TSK'; apply/andP; split =>//.
move: HEPj.
have -> : hep_job j0 j = (@hep_job _ (GEL Job Task) j0 j) by apply: hep_job_elf_gel.
- rewrite /is_ep_causing_intf ler_subr_addl addrAC ler_subr_addl addr0 -TSK'.
- apply: le_trans; rewrite ler_add2r ler_nat.
+ rewrite /is_ep_causing_intf lerBrDl addrAC lerBrDl addr0 -TSK'.
+ apply: le_trans; rewrite lerD2r ler_nat.
apply: job_arrival_between_ge=>//. }}
{ exists t1, t2; split=> [//|]; split=> [//|].
eapply instantiated_busy_interval_equivalent_busy_interval => //. }
diff --git a/util/tactics.v b/util/tactics.v
index 17afea968..92f48f02e 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -104,6 +104,13 @@ Ltac rt_eauto := eauto 4 with basic_rt_facts.
Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
#[export] Hint Resolve I : basic_rt_facts. (* ensure the database exists *)
+(** Note: [idtac] is a no-op. However, it suppresses the default obligation tactic,
+ which uses [intros] to introduce unnamed variables. This is a Coq technicality
+ that a casual reader may safely ignore. It is necessary to avoid triggering one
+ of Prosa's continuous integration checks that validates that no proof scripts
+ depend on automatically generated names. *)
+#[global] Obligation Tactic := idtac.
+
(* ************************************************************************** *)
(** * Handier movement of inequalities. *)
(* ************************************************************************** *)
--
GitLab