From b14d30533a604f9debc25507893f7b8108bdf77e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 22 May 2020 15:28:49 +0200
Subject: [PATCH] Test with merge SBI.
---
.gitlab-ci.yml | 19 ++-----------------
theories/base_logic/vprop.v | 3 +--
theories/base_logic/weakestpre.v | 2 +-
theories/examples/na_stack.v | 2 +-
theories/examples/treiber_stack.v | 4 ++--
theories/gps/model_defs.v | 3 +--
6 files changed, 8 insertions(+), 25 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 78407980..3bf479c5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -27,25 +27,10 @@ variables:
## Build jobs
-build-coq.8.11.0:
+build-iris.dev:
<<: *template
variables:
- OPAM_PINS: "coq version 8.11.0"
- OPAM_PKG: "coq-gpfsl"
+ OPAM_PINS: "coq version 8.11.0 coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#ci/robbert/merge_sbi_new"
tags:
- fp-timing
-build-coq.8.10.2:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.10.2"
-
-build-iris.dev:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.11.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 coq-orc11.dev git git+https://gitlab.mpi-sws.org/iris/orc11.git#$ORC11_REV"
- except:
- only:
- - triggers
- - schedules
- - api
diff --git a/theories/base_logic/vprop.v b/theories/base_logic/vprop.v
index a66f5885..f2a014a3 100644
--- a/theories/base_logic/vprop.v
+++ b/theories/base_logic/vprop.v
@@ -17,7 +17,6 @@ Canonical Structure view_bi_index :=
Definition vProp Σ := monPred view_bi_index (uPredI (iResUR Σ)).
Definition vPropO Σ := monPredO view_bi_index (uPredI (iResUR Σ)).
Definition vPropI Σ := monPredI view_bi_index (uPredI (iResUR Σ)).
-Definition vPropSI Σ := monPredSI view_bi_index (uPredSI (iResUR Σ)).
Hint Extern 10 (IsBiIndexRel _ _) => unfold IsBiIndexRel; solve_lat
: typeclass_instances.
@@ -25,7 +24,7 @@ Hint Extern 10 (IsBiIndexRel _ _) => unfold IsBiIndexRel; solve_lat
(* SOME big_op lemmas *)
From iris.bi Require Import big_op.
-Lemma big_sepM_dup {PROP: sbi} `{Countable K} {A: Type} (φ: K → A → PROP) (m: gmap K A) k a q
+Lemma big_sepM_dup {PROP: bi} `{Countable K} {A: Type} (φ: K → A → PROP) (m: gmap K A) k a q
(In: m !! k = Some a)
: ▷?q (φ k a -∗ φ k a ∗ φ k a) ∗ ▷?q ([∗ map] k' ↦ v' ∈ m, φ k' v')
⊢ ▷?q φ k a ∗ ▷?q ([∗ map] k' ↦ v' ∈ m, φ k' v').
diff --git a/theories/base_logic/weakestpre.v b/theories/base_logic/weakestpre.v
index 6fced496..27755f38 100644
--- a/theories/base_logic/weakestpre.v
+++ b/theories/base_logic/weakestpre.v
@@ -129,7 +129,7 @@ Proof.
by iApply ("IH" with "Hs' WP").
Qed.
-Program Definition wp_def tid E e Φ : vPropSI Σ :=
+Program Definition wp_def tid E e Φ : vPropI Σ :=
MonPred (λ V,
∀ 𝓥, ⌜V ⊑ 𝓥.(cur)⌝ -∗ own tid (● to_latT 𝓥) -∗ seen 𝓥 -∗
WP e at 𝓥 @ E {{ λ v𝓥', let '(v at 𝓥') := v𝓥' return _ in
diff --git a/theories/examples/na_stack.v b/theories/examples/na_stack.v
index a06d57ca..e440607b 100644
--- a/theories/examples/na_stack.v
+++ b/theories/examples/na_stack.v
@@ -58,7 +58,7 @@ Proof.
destruct A as [|v A]; [done|].
apply bi.exist_ne => ?.
repeat (apply bi.sep_ne; [done|]).
- apply bi.later_contractive. destruct n => //. by apply H.
+ f_contractive. by apply H.
Qed.
Definition NAStack_def := fixpoint NAStack'.
diff --git a/theories/examples/treiber_stack.v b/theories/examples/treiber_stack.v
index e1553347..1ca3cf28 100644
--- a/theories/examples/treiber_stack.v
+++ b/theories/examples/treiber_stack.v
@@ -68,7 +68,7 @@ Proof.
repeat (apply bi.sep_ne; [done|]).
do 2 (apply bi.exist_ne => ?).
repeat (apply bi.sep_ne; [done|]).
- apply bi.later_contractive. destruct n => //. by apply H.
+ f_contractive. by apply H.
Qed.
Definition Reachable := fixpoint Reachable'.
@@ -91,7 +91,7 @@ Proof.
apply bi.sep_ne; [done|].
apply bi.exist_ne => ?.
apply bi.sep_ne; [done|].
- apply bi.later_contractive. destruct n => //. by apply H.
+ f_contractive. by apply H.
Qed.
Definition ReachableD := fixpoint ReachableD'.
diff --git a/theories/gps/model_defs.v b/theories/gps/model_defs.v
index 831bb92d..0d9aaf8f 100644
--- a/theories/gps/model_defs.v
+++ b/theories/gps/model_defs.v
@@ -639,8 +639,7 @@ Program Example intExample Σ : interpO Σ unitProtocol :=
(λ (F : interpO Σ unitProtocol) b l γ t s v, ∃ c, ⌜c = #1⌝ ∗ ▷ F b l γ t s v)%I _.
Next Obligation.
repeat intro.
- apply bi.exist_ne => ? . apply bi.sep_ne; [done|]. apply bi.later_contractive.
- destruct n; [done|]. apply H.
+ apply bi.exist_ne => ? . apply bi.sep_ne; [done|]. f_contractive. apply H.
Qed.
Lemma alloc_local_singleton_seen_local l t m V:
--
GitLab