Commit 56406056 authored by Pierre Roux's avatar Pierre Roux Committed by Björn Brandenburg

Update CI configuration for Coq 8.10

We no longer support Coq 8.8.
parent c99edd11
...@@ -9,15 +9,10 @@ stages: ...@@ -9,15 +9,10 @@ stages:
- ./create_makefile.sh - ./create_makefile.sh
- make -j ${NJOBS} - make -j ${NJOBS}
1.8.0-coq-8.8: 1.9.0-coq-8.9:
extends: .build
1.9.0-coq-dev:
extends: .build extends: .build
# it's ok to fail with an unreleased version of Coq
allow_failure: true
1.9.0-coq-8.9: 1.9.0-coq-8.10:
extends: .build extends: .build
# Keep track of all compiled output and the build infrastructure # Keep track of all compiled output and the build infrastructure
artifacts: artifacts:
...@@ -46,19 +41,24 @@ stages: ...@@ -46,19 +41,24 @@ stages:
- "*/*/*/*/*/*/*/*/*.glob" - "*/*/*/*/*/*/*/*/*.glob"
- "*/*/*/*/*/*/*/*/*/*.glob" - "*/*/*/*/*/*/*/*/*/*.glob"
expire_in: 1 week expire_in: 1 week
1.9.0-coq-dev:
extends: .build
# it's ok to fail with an unreleased version of Coq
allow_failure: true
validate: validate:
stage: process stage: process
image: mathcomp/mathcomp:1.9.0-coq-8.9 image: mathcomp/mathcomp:1.9.0-coq-8.10
dependencies: dependencies:
- 1.9.0-coq-8.9 - 1.9.0-coq-8.10
script: make validate script: make validate
doc: doc:
stage: process stage: process
image: mathcomp/mathcomp:1.9.0-coq-8.9 image: mathcomp/mathcomp:1.9.0-coq-8.10
dependencies: dependencies:
- 1.9.0-coq-8.9 - 1.9.0-coq-8.10
script: script:
- make html -j ${NJOBS} - make html -j ${NJOBS}
- mv html with-proofs - mv html with-proofs
......
...@@ -539,7 +539,7 @@ Module ResponseTimeIterationEDF. ...@@ -539,7 +539,7 @@ Module ResponseTimeIterationEDF.
(exists k, k <= max_steps ts /\ f k = f k.+1) -> (exists k, k <= max_steps ts /\ f k = f k.+1) ->
f (max_steps ts) = f (max_steps ts).+1. f (max_steps ts) = f (max_steps ts).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply (@fixedpoint.iter_fix _ _ _ k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -999,4 +999,4 @@ Module ResponseTimeIterationEDF. ...@@ -999,4 +999,4 @@ Module ResponseTimeIterationEDF.
End Analysis. End Analysis.
End ResponseTimeIterationEDF. End ResponseTimeIterationEDF.
\ No newline at end of file
...@@ -379,7 +379,7 @@ Module ResponseTimeIterationFP. ...@@ -379,7 +379,7 @@ Module ResponseTimeIterationFP.
(exists k, k <= max_steps tsk /\ f k = f k.+1) -> (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
f (max_steps tsk) = f (max_steps tsk).+1. f (max_steps tsk) = f (max_steps tsk).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -723,4 +723,4 @@ Module ResponseTimeIterationFP. ...@@ -723,4 +723,4 @@ Module ResponseTimeIterationFP.
End Analysis. End Analysis.
End ResponseTimeIterationFP. End ResponseTimeIterationFP.
\ No newline at end of file
...@@ -532,7 +532,7 @@ Module ResponseTimeIterationEDF. ...@@ -532,7 +532,7 @@ Module ResponseTimeIterationEDF.
(exists k, k <= max_steps ts /\ f k = f k.+1) -> (exists k, k <= max_steps ts /\ f k = f k.+1) ->
f (max_steps ts) = f (max_steps ts).+1. f (max_steps ts) = f (max_steps ts).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -987,4 +987,4 @@ Module ResponseTimeIterationEDF. ...@@ -987,4 +987,4 @@ Module ResponseTimeIterationEDF.
End Analysis. End Analysis.
End ResponseTimeIterationEDF. End ResponseTimeIterationEDF.
\ No newline at end of file
...@@ -372,7 +372,7 @@ Module ResponseTimeIterationFP. ...@@ -372,7 +372,7 @@ Module ResponseTimeIterationFP.
(exists k, k <= max_steps tsk /\ f k = f k.+1) -> (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
f (max_steps tsk) = f (max_steps tsk).+1. f (max_steps tsk) = f (max_steps tsk).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -703,4 +703,4 @@ Module ResponseTimeIterationFP. ...@@ -703,4 +703,4 @@ Module ResponseTimeIterationFP.
End Analysis. End Analysis.
End ResponseTimeIterationFP. End ResponseTimeIterationFP.
\ No newline at end of file
...@@ -586,7 +586,7 @@ Module ResponseTimeIterationEDF. ...@@ -586,7 +586,7 @@ Module ResponseTimeIterationEDF.
(exists k, k <= max_steps ts /\ f k = f k.+1) -> (exists k, k <= max_steps ts /\ f k = f k.+1) ->
f (max_steps ts) = f (max_steps ts).+1. f (max_steps ts) = f (max_steps ts).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -1081,4 +1081,4 @@ Module ResponseTimeIterationEDF. ...@@ -1081,4 +1081,4 @@ Module ResponseTimeIterationEDF.
End Analysis. End Analysis.
End ResponseTimeIterationEDF. End ResponseTimeIterationEDF.
\ No newline at end of file
...@@ -372,7 +372,7 @@ Module ResponseTimeIterationFP. ...@@ -372,7 +372,7 @@ Module ResponseTimeIterationFP.
(exists k, k <= max_steps tsk /\ f k = f k.+1) -> (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
f (max_steps tsk) = f (max_steps tsk).+1. f (max_steps tsk) = f (max_steps tsk).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -723,4 +723,4 @@ Module ResponseTimeIterationFP. ...@@ -723,4 +723,4 @@ Module ResponseTimeIterationFP.
End Analysis. End Analysis.
End ResponseTimeIterationFP. End ResponseTimeIterationFP.
\ No newline at end of file
...@@ -531,7 +531,7 @@ Module ResponseTimeIterationEDF. ...@@ -531,7 +531,7 @@ Module ResponseTimeIterationEDF.
(exists k, k <= max_steps ts /\ f k = f k.+1) -> (exists k, k <= max_steps ts /\ f k = f k.+1) ->
f (max_steps ts) = f (max_steps ts).+1. f (max_steps ts) = f (max_steps ts).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -982,4 +982,4 @@ Module ResponseTimeIterationEDF. ...@@ -982,4 +982,4 @@ Module ResponseTimeIterationEDF.
End Analysis. End Analysis.
End ResponseTimeIterationEDF. End ResponseTimeIterationEDF.
\ No newline at end of file
...@@ -362,7 +362,7 @@ Module ResponseTimeIterationFP. ...@@ -362,7 +362,7 @@ Module ResponseTimeIterationFP.
(exists k, k <= max_steps tsk /\ f k = f k.+1) -> (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
f (max_steps tsk) = f (max_steps tsk).+1. f (max_steps tsk) = f (max_steps tsk).+1.
Proof. Proof.
by intros EX; des; apply iter_fix with (k := k). by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed. Qed.
(* Else, we derive a contradiction. *) (* Else, we derive a contradiction. *)
...@@ -686,4 +686,4 @@ Module ResponseTimeIterationFP. ...@@ -686,4 +686,4 @@ Module ResponseTimeIterationFP.
End Analysis. End Analysis.
End ResponseTimeIterationFP. End ResponseTimeIterationFP.
\ No newline at end of file
...@@ -429,7 +429,7 @@ Section Sequential_Abstract_RTA. ...@@ -429,7 +429,7 @@ Section Sequential_Abstract_RTA.
{ by move: H_not_job_of_tsk => /eqP TSK; rewrite TSK. } { by move: H_not_job_of_tsk => /eqP TSK; rewrite TSK. }
{ by move: H_sched => /eqP SCHEDt; apply scheduled_implies_pending; { by move: H_sched => /eqP SCHEDt; apply scheduled_implies_pending;
auto using ideal_proc_model_ensures_ideal_progress. } auto using ideal_proc_model_ensures_ideal_progress. }
case ARRNEQ: (job_arrival j' <= job_arrival j). case_eq (job_arrival j' <= job_arrival j) => ARRNEQ.
{ move: ARR => /andP [РР _]. { move: ARR => /andP [РР _].
eapply arrived_between_implies_in_arrivals; eauto 2. eapply arrived_between_implies_in_arrivals; eauto 2.
by apply/andP; split; last rewrite /A subnKC // addn1 ltnS. by apply/andP; split; last rewrite /A subnKC // addn1 ltnS.
...@@ -498,7 +498,7 @@ Section Sequential_Abstract_RTA. ...@@ -498,7 +498,7 @@ Section Sequential_Abstract_RTA.
2: by apply interference_plus_sched_le_serv_of_task_plus_task_interference_idle. 2: by apply interference_plus_sched_le_serv_of_task_plus_task_interference_idle.
have ARRs: arrives_in arr_seq j1; have ARRs: arrives_in arr_seq j1;
first by apply H_jobs_come_from_arrival_sequence with t; apply/eqP. first by apply H_jobs_come_from_arrival_sequence with t; apply/eqP.
case TSK: (job_task j1 == tsk). case_eq (job_task j1 == tsk) => TSK.
2: by eapply interference_plus_sched_le_serv_of_task_plus_task_interference_task; [edone| apply/negbT]. 2: by eapply interference_plus_sched_le_serv_of_task_plus_task_interference_task; [edone| apply/negbT].
case EQ: (j == j1); [move: EQ => /eqP EQ; subst j1 | ]. case EQ: (j == j1); [move: EQ => /eqP EQ; subst j1 | ].
1: by apply interference_plus_sched_le_serv_of_task_plus_task_interference_j. 1: by apply interference_plus_sched_le_serv_of_task_plus_task_interference_j.
...@@ -709,4 +709,4 @@ Section Sequential_Abstract_RTA. ...@@ -709,4 +709,4 @@ Section Sequential_Abstract_RTA.
End ResponseTimeBound. End ResponseTimeBound.
End Sequential_Abstract_RTA. End Sequential_Abstract_RTA.
\ No newline at end of file
...@@ -9,12 +9,12 @@ Section State. ...@@ -9,12 +9,12 @@ Section State.
Definition processor_state := option Job. Definition processor_state := option Job.
Global Instance pstate_instance : ProcessorState Job (option Job) := Global Program Instance pstate_instance : ProcessorState Job (option Job) :=
{ {
scheduled_in j s := s == Some j; scheduled_in j s := s == Some j;
service_in j s := s == Some j service_in j s := s == Some j;
}. }.
Proof. Next Obligation.
by move=> j [j'->|]. by rewrite H.
Defined. Defined.
End State. End State.
...@@ -13,12 +13,13 @@ Section Schedule. ...@@ -13,12 +13,13 @@ Section Schedule.
Definition identical_state := processor num_cpus -> processor_state. Definition identical_state := processor num_cpus -> processor_state.
Global Instance multiproc_state : ProcessorState Job (identical_state) := Global Program Instance multiproc_state : ProcessorState Job (identical_state) :=
{ {
scheduled_in j s := [exists cpu, scheduled_in j (s cpu)]; scheduled_in j s := [exists cpu, scheduled_in j (s cpu)];
service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu) service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
}. }.
Proof. Next Obligation.
move: j s H0.
move=> j s /existsP Hsched. move=> j s /existsP Hsched.
apply/eqP. apply/eqP.
rewrite sum_nat_eq0. rewrite sum_nat_eq0.
......
...@@ -31,12 +31,12 @@ Section State. ...@@ -31,12 +31,12 @@ Section State.
End Service. End Service.
Global Instance pstate_instance : ProcessorState Job (processor_state) := Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
{ {
scheduled_in := scheduled_in; scheduled_in := scheduled_in;
service_in := service_in service_in := service_in
}. }.
Proof. Next Obligation.
by move=> j [|j'|j']//=->. by move: H; case s => //= j' ->.
Defined. Defined.
End State. End State.
...@@ -27,12 +27,13 @@ Section State. ...@@ -27,12 +27,13 @@ Section State.
End Service. End Service.
Global Instance pstate_instance : ProcessorState Job processor_state := Global Program Instance pstate_instance : ProcessorState Job processor_state :=
{ {
scheduled_in := scheduled_in; scheduled_in := scheduled_in;
service_in := service_in service_in := service_in
}. }.
Proof. Next Obligation.
move: j s H.
by move=> j []//= j' s->. by move=> j []//= j' s->.
Defined. Defined.
......
...@@ -17,11 +17,10 @@ Section LiuAndLaylandReadiness. ...@@ -17,11 +17,10 @@ Section LiuAndLaylandReadiness.
Context `{JobArrival Job} `{JobCost Job}. Context `{JobArrival Job} `{JobCost Job}.
(* In the basic Liu & Layland model, a job is ready iff it is pending. *) (* In the basic Liu & Layland model, a job is ready iff it is pending. *)
Global Instance basic_ready_instance : JobReady Job PState := Global Program Instance basic_ready_instance : JobReady Job PState :=
{ {
job_ready sched j t := pending sched j t job_ready sched j t := pending sched j t
}. }.
Proof. trivial. Defined.
(* Under this definition, a schedule satisfies that only ready jobs execute (* Under this definition, a schedule satisfies that only ready jobs execute
......
...@@ -23,12 +23,12 @@ Section ReadinessOfJitteryJobs. ...@@ -23,12 +23,12 @@ Section ReadinessOfJitteryJobs.
(* A job that experiences jitter is ready only when the jitter-induced delay (* A job that experiences jitter is ready only when the jitter-induced delay
has passed after its arrival and if it is not yet complete. *) has passed after its arrival and if it is not yet complete. *)
Global Instance jitter_ready_instance : JobReady Job PState := Global Program Instance jitter_ready_instance : JobReady Job PState :=
{ {
job_ready sched j t := is_released j t && ~~ completed_by sched j t job_ready sched j t := is_released j t && ~~ completed_by sched j t
}. }.
Proof. Next Obligation.
move=> sched j t /andP [REL UNFINISHED]. move: H3 => /andP [REL UNFINISHED].
rewrite /pending. apply /andP. split => //. rewrite /pending. apply /andP. split => //.
move: REL. rewrite /is_released /has_arrived. move: REL. rewrite /is_released /has_arrived.
by apply leq_addk. by apply leq_addk.
......
...@@ -16,7 +16,7 @@ Section SeqSet. ...@@ -16,7 +16,7 @@ Section SeqSet.
Canonical Structure setSubType := [subType for _set_seq]. Canonical Structure setSubType := [subType for _set_seq].
Definition set_eqMixin := [eqMixin of set by <:]. Definition set_eqMixin := [eqMixin of set by <:].
Canonical Structure set_eqType := EqType set set_eqMixin. Canonical Structure set_eqType := EqType set set_eqMixin.
Canonical Structure mem_set_predType := mkPredType (fun (l : set) => mem_seq (_set_seq l)). Canonical Structure mem_set_predType := PredType (fun (l : set) => mem_seq (_set_seq l)).
Definition set_of of phant T := set. Definition set_of of phant T := set.
End SeqSet. End SeqSet.
...@@ -51,4 +51,4 @@ Section LemmasFinType. ...@@ -51,4 +51,4 @@ Section LemmasFinType.
by move: UNIQ => /card_uniqP ->. by move: UNIQ => /card_uniqP ->.
Qed. Qed.
End LemmasFinType. End LemmasFinType.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment