Commit 9d811c88 authored by Ralf Jung's avatar Ralf Jung
Browse files

downgrade Iris to 3.2.0 to depend on something stable

parent fcd3be22
Pipeline #20830 passed with stage
in 16 minutes and 47 seconds
...@@ -31,17 +31,3 @@ build-coq.8.9.0: ...@@ -31,17 +31,3 @@ build-coq.8.9.0:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.9.0" OPAM_PINS: "coq version 8.9.0"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-iris.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
except:
only:
- triggers
- schedules
- api
# Iris + Fair Refinements COQ DEVELOPMENT # Iris + Fair Refinements COQ DEVELOPMENT
** This project is no longer maintained.
It will not be adjusted to work with current versions of Iris. **
This is the Coq development for an extension of Iris to support This is the Coq development for an extension of Iris to support
termination-preserving fair refinement. It is an updated version of work termination-preserving fair refinement. It is an updated version of work
described in the paper: described in the paper:
...@@ -15,14 +18,13 @@ support general BI logics. ...@@ -15,14 +18,13 @@ support general BI logics.
This version is known to compile with: This version is known to compile with:
- Coq 8.8.2 / 8.9.0 - Coq 8.9.0
- A development version of Iris - Iris 3.2.0
The easiest way to install the correct versions of the dependencies is through The easiest way to install the correct versions of the dependencies is through
opam. You will need the Coq and Iris opam repositories: opam. You will need the Coq opam repository:
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Once you got opam set up, run `make build-dep` to install the right versions Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies. of the dependencies.
......
...@@ -5,6 +5,6 @@ build: [make "-j%{jobs}%"] ...@@ -5,6 +5,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"] remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [ depends: [
"coq" { (>= "8.7.2") | (= "dev") } "coq" { ((>= "8.7.2") & (< "8.10")) | (= "dev") }
"coq-iris" { (= "dev.2019-10-25.0.bbd38120") | (= "dev") } "coq-iris" { (= "3.2.0") | (= "dev") }
] ]
...@@ -184,7 +184,7 @@ Implicit Types m : gmap K A. ...@@ -184,7 +184,7 @@ Implicit Types m : gmap K A.
Implicit Types i : K. Implicit Types i : K.
Implicit Types x y : A. Implicit Types x y : A.
Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i (mm2 = (.!! i)). Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i (mm2 = (!! i)).
Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed. Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
Lemma lookup_validN_Some n m i x : {n} m m !! i {n} Some x {n} x. Lemma lookup_validN_Some n m i x : {n} m m !! i {n} Some x {n} x.
...@@ -341,7 +341,7 @@ Section freshness. ...@@ -341,7 +341,7 @@ Section freshness.
End freshness. End freshness.
Lemma insert_local_update m i x y mf : Lemma insert_local_update m i x y mf :
x ~l~> y @ mf = (.!! i) <[i:=x]>m ~l~> <[i:=y]>m @ mf. x ~l~> y @ mf = (!! i) <[i:=x]>m ~l~> <[i:=y]>m @ mf.
Proof. Proof.
intros [Hxy Hxy']; split. intros [Hxy Hxy']; split.
- intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
...@@ -354,7 +354,7 @@ Proof. ...@@ -354,7 +354,7 @@ Proof.
Qed. Qed.
Lemma singleton_local_update i x y mf : Lemma singleton_local_update i x y mf :
x ~l~> y @ mf = (.!! i) {[ i := x ]} ~l~> {[ i := y ]} @ mf. x ~l~> y @ mf = (!! i) {[ i := x ]} ~l~> {[ i := y ]} @ mf.
Proof. apply insert_local_update. Qed. Proof. apply insert_local_update. Qed.
Lemma alloc_singleton_local_update m i x mf : Lemma alloc_singleton_local_update m i x mf :
...@@ -369,7 +369,7 @@ Proof. ...@@ -369,7 +369,7 @@ Proof.
Qed. Qed.
Lemma alloc_unit_singleton_local_update i x mf : Lemma alloc_unit_singleton_local_update i x mf :
mf = (.!! i) = None x ~l~> {[ i := x ]} @ mf. mf = (!! i) = None x ~l~> {[ i := x ]} @ mf.
Proof. Proof.
intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi. intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
Qed. Qed.
......
...@@ -235,7 +235,7 @@ Section properties. ...@@ -235,7 +235,7 @@ Section properties.
Local Arguments op _ _ !_ !_ / : simpl nomatch. Local Arguments op _ _ !_ !_ / : simpl nomatch.
Local Arguments cmra_op _ !_ !_ / : simpl nomatch. Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i (mk = (.!! i)). Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i (mk = (!! i)).
Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed. Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
Lemma list_op_app l1 l2 l3 : Lemma list_op_app l1 l2 l3 :
...@@ -332,7 +332,7 @@ Section properties. ...@@ -332,7 +332,7 @@ Section properties.
Qed. Qed.
Lemma list_middle_local_update l1 l2 x y ml : Lemma list_middle_local_update l1 l2 x y ml :
x ~l~> y @ ml = (.!! length l1) x ~l~> y @ ml = (!! length l1)
l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml. l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
Proof. Proof.
intros [Hxy Hxy']; split. intros [Hxy Hxy']; split.
...@@ -353,7 +353,7 @@ Section properties. ...@@ -353,7 +353,7 @@ Section properties.
Qed. Qed.
Lemma list_singleton_local_update i x y ml : Lemma list_singleton_local_update i x y ml :
x ~l~> y @ ml = (.!! i) {[ i := x ]} ~l~> {[ i := y ]} @ ml. x ~l~> y @ ml = (!! i) {[ i := x ]} ~l~> {[ i := y ]} @ ml.
Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed. Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
End properties. End properties.
......
...@@ -42,7 +42,7 @@ Proof. ...@@ -42,7 +42,7 @@ Proof.
rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto. rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
Qed. Qed.
Lemma cmra_update_updateP x y : x ~~> y x ~~>: (y =.). Lemma cmra_update_updateP x y : x ~~> y x ~~>: (y =).
Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed. Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
Lemma cmra_updateP_id (P : A Prop) x : P x x ~~>: P. Lemma cmra_updateP_id (P : A Prop) x : P x x ~~>: P.
Proof. intros ? n mz ?; eauto. Qed. Proof. intros ? n mz ?; eauto. Qed.
...@@ -52,7 +52,7 @@ Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed. ...@@ -52,7 +52,7 @@ Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
Lemma cmra_updateP_compose_l (Q : A Prop) x y : x ~~> y y ~~>: Q x ~~>: Q. Lemma cmra_updateP_compose_l (Q : A Prop) x y : x ~~> y y ~~>: Q x ~~>: Q.
Proof. Proof.
rewrite cmra_update_updateP. rewrite cmra_update_updateP.
intros; apply cmra_updateP_compose with (y =.); naive_solver. intros; apply cmra_updateP_compose with (y =); naive_solver.
Qed. Qed.
Lemma cmra_updateP_weaken (P Q : A Prop) x : Lemma cmra_updateP_weaken (P Q : A Prop) x :
x ~~>: P ( y, P y Q y) x ~~>: Q. x ~~>: P ( y, P y Q y) x ~~>: Q.
......
...@@ -133,7 +133,7 @@ Qed. ...@@ -133,7 +133,7 @@ Qed.
Lemma own_update γ a a' E : a ~~> a' own γ a ={E}=> own γ a'. Lemma own_update γ a a' E : a ~~> a' own γ a ={E}=> own γ a'.
Proof. Proof.
intros; rewrite (own_updateP (a' =.)); last by apply cmra_update_updateP. intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->. by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed. Qed.
End global. End global.
...@@ -224,7 +224,7 @@ Qed. ...@@ -224,7 +224,7 @@ Qed.
Lemma owne_update a a' E : a ~~> a' owne a (|={E}=> owne a'). Lemma owne_update a a' E : a ~~> a' owne a (|={E}=> owne a').
Proof. Proof.
intros; rewrite (owne_updateP (a' =.)); last by apply cmra_update_updateP. intros; rewrite (owne_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->. by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed. Qed.
......
...@@ -258,7 +258,7 @@ Proof. auto using pvs_mask_frame'. Qed. ...@@ -258,7 +258,7 @@ Proof. auto using pvs_mask_frame'. Qed.
Lemma pvs_ownG_update E m m' : m ~~> m' ownG m ={E}=> ownG m'. Lemma pvs_ownG_update E m m' : m ~~> m' ownG m ={E}=> ownG m'.
Proof. Proof.
intros; rewrite (pvs_ownG_updateP E _ (m' =.)); last by apply cmra_update_updateP. intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim=> m''; apply pure_elim_l=> ->. by apply pvs_mono, uPred.exist_elim=> m''; apply pure_elim_l=> ->.
Qed. Qed.
......
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