Make Prosa compatible with Coq 8.7.0 and Mathcomp 1.6.4

- Remove Require declarations from Modules.
- Small fixes due to changes in the type checker.
- Generate _CoqProject with Makefile and remove spurious warnings from ssreflect.

.gitignore

@@ -4,3 +4,4 @@
 *.html
 *.aux
 Makefile*
+_CoqProject

_CoqProject

--R . rt
\ No newline at end of file

analysis/apa/bertogna_edf_theory.v

@@ -919,7 +919,7 @@ Module ResponseTimeAnalysisEDF.
           rewrite -[_ < _]negbK in SUM.
           move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
           unfold I, total_interference_bound_edf.
-          rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+          rewrite big_seq_cond [X in _ <= X]big_seq_cond.
           apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
           specialize (ALL (tsk_k, R_k) INBOUNDSk).
           unfold interference_bound_edf; simpl in *.

analysis/global/basic/bertogna_edf_theory.v

@@ -719,7 +719,7 @@ Module ResponseTimeAnalysisEDF.
           rewrite -[_ < _]negbK in SUM.
           move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
           unfold I, total_interference_bound_edf.
-          rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+          rewrite big_seq_cond [X in _ <= X]big_seq_cond.
           apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
           specialize (ALL (tsk_k, R_k) INBOUNDSk).
           unfold interference_bound_edf; simpl in *.

analysis/global/jitter/bertogna_edf_theory.v

@@ -761,7 +761,7 @@ Module ResponseTimeAnalysisEDFJitter.
             rewrite -[_ < _]negbK in SUM.
             move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
             unfold I, total_interference_bound_edf.
-            rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+            rewrite big_seq_cond [X in _ <= X]big_seq_cond.
             apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
             specialize (ALL (tsk_k, R_k) INBOUNDSk).
             unfold interference_bound_edf; simpl in *.

analysis/global/parallel/bertogna_edf_theory.v

@@ -415,7 +415,7 @@ Module ResponseTimeAnalysisEDF.
           rewrite -[_ < _]negbK in SUM.
           move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
           unfold I, total_interference_bound_edf.
-          rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+          rewrite big_seq_cond [X in _ <= X]big_seq_cond.
           apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
           specialize (ALL (tsk_k, R_k) INBOUNDSk).
           unfold interference_bound_edf; simpl in *.

create_makefile.sh

+#!/bin/bash 
+
+# Include rt-proofs library in _CoqProject. (For Coq versions >= 8.6, remove spurious warnings.)
+version=$(echo $(coqc -v 1) | grep -o "version .\.." | tail -c 4)
+if ([ "$version" == "8.4" ] || [ "$version" == "8.5" ]) then
+  echo "-R . rt" > _CoqProject
+else
+  echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
+fi
+
 # Compile all *.v files (except the ones that define the decidable equality). Those
 # are directly included in other files.
 coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile

model/schedule/global/jitter/interference.v

@@ -3,6 +3,8 @@ Require Import rt.model.arrival.basic.task rt.model.priority rt.model.schedule.g
 Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
+Require rt.model.schedule.global.basic.interference.
+
 Module Interference.
 
   Import ScheduleOfSporadicTaskWithJitter Priority Workload.
@@ -10,7 +12,7 @@ Module Interference.
   (* We import some of the basic definitions, but we need to re-define almost everything
      since the definition of backlogged (and thus the definition of interference)
      changes with jitter. *)
-  Require Import rt.model.schedule.global.basic.interference.
+  Import rt.model.schedule.global.basic.interference.
   Export Interference.
   
   Section InterferenceDefs.

model/schedule/global/jitter/schedule.v

@@ -3,11 +3,13 @@ Require Import rt.model.arrival.basic.task.
 Require Import rt.model.schedule.global.jitter.job rt.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
+Require rt.model.schedule.global.basic.schedule.
+
 (* Definition, properties and lemmas about schedules. *)
 Module ScheduleWithJitter.
 
   (* We import the original schedule module and redefine whatever is required. *)
-  Require Export rt.model.schedule.global.basic.schedule.
+  Export rt.model.schedule.global.basic.schedule.
   Export ArrivalSequence Schedule.
   
   (* We need to redefine the properties of a job that depend on the arrival time. *)

model/schedule/partitioned/schedulability.v

@@ -5,9 +5,10 @@ Require Import rt.model.schedule.global.basic.schedule.
 Require Import rt.model.schedule.partitioned.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
-Module PartitionSchedulability.
+Require rt.model.schedule.uni.schedule.
 
-  Require rt.model.schedule.uni.schedule.
+Module PartitionSchedulability.
+  
   Module uni_sched := rt.model.schedule.uni.schedulability.Schedulability.
   Import ArrivalSequence Partitioned Schedule Schedulability.
 

util/tactics.v

@@ -412,7 +412,7 @@ Ltac feed H :=
     assert foo as FOO; [|specialize (H FOO); clear FOO]
   end.
 
-Ltac feed_n n H := match constr:n with
+Ltac feed_n n H := match constr:(n) with
   | O => idtac
   | (S ?m) => feed H ; [| feed_n m H]
                    end.