Commit 09703078 authored by Björn Brandenburg's avatar Björn Brandenburg

port existing proofs to ssreflect 1.9.0

From the mathcomp 1.9.0 release notes:

> removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to
> improve robustness of by ...; scripts may need to invoke addn0,
> addnS, muln0 or mulnS explicitly where these hints were used
> accidentally.

=> This patch makes these required fixes in Prosa.

While at it, turn on CI for coq:dev and Coq 8.9 with two versions of ssreflect.
parent 8045a633
......@@ -5,14 +5,11 @@ stages:
.build:
stage: build
image: coqorg/${CI_JOB_NAME}
image: coqorg/${COQ_DOCKER_IMAGE}
before_script:
- if [ -n "${COMPILER_EDGE}" ]; then opam switch ${COMPILER_EDGE} && eval $(opam env); fi
- opam update -y
# NOTE: we currently fix the mathcomp version to 1.8.0 here because
# version 1.9.0 causes a build failure that still needs to be
# investigated.
- opam install -y -j ${NJOBS} coq-mathcomp-ssreflect.1.8.0
- opam install -y -j ${NJOBS} ${SSREFLECT_PACKAGE}
- opam config list
- opam repo list
- opam list
......@@ -22,9 +19,25 @@ stages:
- make -j ${NJOBS}
- make validate
coq:8.9:
.ssreflect_latest:
extends: .build
variables:
SSREFLECT_PACKAGE: "coq-mathcomp-ssreflect"
COQ_DOCKER_IMAGE: ${CI_JOB_NAME}
coq:8.9+ssreflect:1.8.0:
extends: .build
variables:
COQ_DOCKER_IMAGE: "coq:8.9"
# NOTE: we currently fix the mathcomp version to 1.8.0 here because
# version 1.9.0 causes a build failure that still needs to be
# investigated.
SSREFLECT_PACKAGE: "coq-mathcomp-ssreflect.1.8.0"
coq:8.9:
extends: .ssreflect_latest
# Currently does not work with fixed ssreflect version
#coq:dev:
# extends: .build
coq:dev:
extends: .ssreflect_latest
# it's ok to fail with an unreleased version of Coq
allow_failure: true
......@@ -386,7 +386,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
rewrite case2 Hcases. repeat rewrite addSn case1 -subn1 subKn //.
repeat rewrite subn0.
case Hc_slot:(c < time_slot); rewrite /duration_to_finish_from_start_of_slot_with.
* by rewrite ceil_eq1.
* by rewrite ceil_eq1 //; ssromega.
* rewrite ceil_suba //; try ssromega.
rewrite subn1 mulnBl mul1n addnA -addSn addn1.
apply/eqP. rewrite eqn_add2l subnBA // addnA. repeat rewrite addnBA; try ssromega.
......@@ -834,4 +834,4 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
End WCRT_analysis.
End WCRT_OneJobTDMA.
\ No newline at end of file
End WCRT_OneJobTDMA.
......@@ -391,7 +391,7 @@ Module SustainabilityAllCostsProperties.
have SAME: service sched_new j0 t.+1 = service sched_new j0 t.
{
apply negbTE in NOTSCHEDn.
by rewrite /service /service_during big_nat_recr //= /service_at NOTSCHEDn.
by rewrite /service /service_during big_nat_recr //= /service_at NOTSCHEDn addn0.
}
rewrite SAME {SAME} in NOTLATE'.
have INV := sched_new_service_invariant t (ltnW LTr) j0.
......@@ -520,7 +520,7 @@ Module SustainabilityAllCostsProperties.
apply leq_trans with (n := suspension_start sched_susp j0 t); [|by apply IHt].
apply eq_leq, same_service_implies_same_last_execution.
rewrite /service /service_during big_nat_recr //= /service_at.
case (boolP (scheduled_at sched_susp j0 t)); last by done.
case (boolP (scheduled_at sched_susp j0 t)); last by rewrite addn0.
intros SCHEDs; apply H_respects_self_suspensions in SCHEDs.
by move: SUSPn => /andP [/andP [_ SUSPs] _].
}
......@@ -946,4 +946,4 @@ Module SustainabilityAllCostsProperties.
End ReductionProperties.
End SustainabilityAllCostsProperties.
\ No newline at end of file
End SustainabilityAllCostsProperties.
Require Import rt.util.all.
Require Import rt.model.suspension.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.schedule.uni.schedule.
......@@ -510,7 +511,7 @@ Module SuspensionIntervals.
last by apply last_execution_bounded_by_identity.
apply eq_leq, same_service_implies_same_last_execution.
rewrite /service /service_during big_nat_recr //= /service_at.
by apply negbTE in NOTSCHED; rewrite NOTSCHED.
by apply negbTE in NOTSCHED; rewrite NOTSCHED addn0.
Qed.
End ExecutionBeforeSuspension.
......@@ -519,4 +520,4 @@ Module SuspensionIntervals.
End DefiningSuspensionIntervals.
End SuspensionIntervals.
\ No newline at end of file
End SuspensionIntervals.
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