From 977b763b58c1a9dd6f44deece943f483fa30d7a6 Mon Sep 17 00:00:00 2001
From: Joshua Yanovski
Date: Mon, 31 Jul 2017 16:08:36 +0200
Subject: [PATCH] Bump Iris version to match LambdaRust-Coq.
---
opam.pins | 2 +-
theories/atomic.v | 1 -
theories/atomic_incr.v | 1 -
theories/flat.v | 14 +++++++-------
theories/misc.v | 8 ++++----
theories/peritem.v | 2 +-
theories/simple_sync.v | 2 +-
theories/treiber.v | 10 +++++-----
8 files changed, 19 insertions(+), 21 deletions(-)
diff --git a/opam.pins b/opam.pins
index ac0de21..9087d1e 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 01d12014855abe6adaea20bbb35b1e9beadff14e
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33
diff --git a/theories/atomic.v b/theories/atomic.v
index 84ddd9a..e3343ef 100644
--- a/theories/atomic.v
+++ b/theories/atomic.v
@@ -2,7 +2,6 @@
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
-From iris.prelude Require Export coPset.
Import uPred.
Section atomic.
diff --git a/theories/atomic_incr.v b/theories/atomic_incr.v
index e7fa0c9..a7ac870 100644
--- a/theories/atomic_incr.v
+++ b/theories/atomic_incr.v
@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris_atomic Require Import atomic.
From iris.proofmode Require Import tactics.
-From iris.prelude Require Import coPset.
From iris.heap_lang.lib Require Import par.
Section incr.
diff --git a/theories/flat.v b/theories/flat.v
index 07b98eb..35ec113 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -166,7 +166,7 @@ Section proof.
subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
{ iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
- iApply "HΦ". iFrame.
+ iApply "HΦ". iFrame. done.
* iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
- destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
@@ -207,7 +207,7 @@ Section proof.
{ iFrame. iFrame "#". }
iNext. iIntros "HRf".
wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
- iFrame "#"; first by iFrame. eauto.
+ iFrame "#"; first by iFrame.
Qed.
Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
@@ -282,7 +282,7 @@ Section proof.
iIntros (P Q x) "#Hf".
iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
- { iFrame. iFrame "#". eauto. }
+ { iFrame. iFrame "#". }
iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
wp_let. wp_bind (loop _ _ _).
iApply (loop_spec with "[-Hx HoQ]")=>//.
@@ -290,13 +290,13 @@ Section proof.
iNext. iIntros (? ?) "Hs".
iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
destruct (decide (x = a)) as [->|Hneq].
- - iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
+ - iDestruct (saved_prop_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
- iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
+ iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
- iExFalso. iCombine "Hx" "Hx'" as "Hx".
iDestruct (own_valid with "Hx") as %[_ H1].
- rewrite pair_op //= in H1=>//. apply to_agree_comp_valid in H1.
- fold_leibniz. done.
+ rewrite //= in H1.
+ by apply agree_op_inv' in H1.
Qed.
End proof.
diff --git a/theories/misc.v b/theories/misc.v
index 89557c4..19269fd 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -3,7 +3,6 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap agree.
-From iris.prelude Require Import countable.
From iris.base_logic Require Import big_op auth fractional.
Import uPred.
@@ -36,8 +35,9 @@ Section heap_extra.
~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
p ↦{q1} a ∗ p ↦{q2} b ⊢ False.
Proof.
- iIntros (?) "Hp".
- iDestruct (@mapsto_valid_2 with "Hp") as %H'. done.
+ iIntros (?) "Hp".
+ iDestruct "Hp" as "[Hl Hr]".
+ iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
Qed.
End heap_extra.
@@ -81,6 +81,6 @@ Section pair.
iIntros "[Ho Ho']".
iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
subst. iCombine "Ho" "Ho'" as "Ho".
- rewrite pair_op frac_op' agree_idemp. by iFrame.
+ by iFrame.
Qed.
End pair.
diff --git a/theories/peritem.v b/theories/peritem.v
index 76a54ad..156600d 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -54,7 +54,7 @@ Section proofs.
{ iFrame. iExists [], l.
iFrame. simpl. eauto. }
iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
- iApply "HΦ". iFrame "#".
+ iApply "HΦ". iFrame "#". done.
Qed.
Lemma push_spec (s: loc) (x: val):
diff --git a/theories/simple_sync.v b/theories/simple_sync.v
index c15ce1e..a27fbc9 100644
--- a/theories/simple_sync.v
+++ b/theories/simple_sync.v
@@ -33,7 +33,7 @@ Section syncer.
iSpecialize ("Hf" with "[R HP]"); first by iFrame.
iApply wp_wand_r. iSplitL "Hf"; first done.
iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
- iApply (release_spec with "[$HR $Hl $Hlocked]").
+ iApply (release_spec with "[$Hl $HR $Hlocked]").
iNext. iIntros "_". by wp_seq.
Qed.
End syncer.
diff --git a/theories/treiber.v b/theories/treiber.v
index 86608d4..40aa648 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -64,17 +64,17 @@ Section proof.
simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
iExFalso. iDestruct "Hxs" as (?) "Hhd'".
(* FIXME: If I dont use the @ here and below through this file, it loops. *)
- by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
+ by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
- induction ys as [|y ys' IHys'].
+ iIntros (hd) "(Hxs & Hys)".
simpl.
iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
iDestruct "Hys" as (?) "Hhd'".
- by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
+ by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
- iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %[= Heq].
+ iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
by subst.
Qed.
@@ -173,9 +173,9 @@ Section proof.
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
destruct xs as [|x' xs''].
- simpl. iDestruct "Hhd''" as (?) "H".
- iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1 $H]") as %?.
+ iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?.
- simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
- iDestruct (@mapsto_agree with "[$Hhd1 $Hhd'']") as %[=].
+ iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=].
subst.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
--
GitLab