Commit 753aaaae authored by Ralf Jung's avatar Ralf Jung

fix build with latest iris

parent 70104c0f
Pipeline #3331 passed with stage
in 8 minutes and 27 seconds
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0cc2c6e098bfb05c056783b9212c9218fa46aa5e
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b212b3faddae4b089f30ef1c7a27d43ebd3a1675
......@@ -66,7 +66,7 @@ Section user.
Lemma incr_2_safe:
(x: Z), (WP incr_2 #x {{ _, True }})%I.
Proof.
iIntros (x) "". (* FIXME: I did iIntros, this should not be needed. *)
iIntros (x).
rewrite /incr_2 /=.
wp_lam.
wp_alloc l as "Hl".
......
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import dec_agree frac.
From iris.algebra Require Import agree frac.
From iris_atomic Require Import sync atomic_sync.
Import uPred.
Section atomic_pair.
Context `{!heapG Σ, !lockG Σ, !syncG Σ,
!inG Σ (prodR fracR (dec_agreeR (val * val)))} (N : namespace).
!inG Σ (prodR fracR (agreeR (prodC valC valC)))} (N : namespace).
Definition pcas_seq : val :=
λ: "ls" "ab",
......
......@@ -2,9 +2,11 @@
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import dec_agree frac.
From iris.algebra Require Import deprecated frac.
From iris_atomic Require Import atomic sync misc.
Import dec_agree.
Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
......
(* evmap.v -- generalized heap-like monoid composite *)
From iris.base_logic Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.algebra Require Export auth frac gmap dec_agree.
From iris.algebra Require Export auth frac gmap.
From iris.algebra Require deprecated.
From iris.proofmode Require Import tactics.
Export deprecated.dec_agree.
Section evmap.
Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
Definition evkR := prodR Q (dec_agreeR A).
......
......@@ -4,10 +4,12 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import auth frac agree excl dec_agree gset gmap.
From iris.algebra Require Import auth frac agree excl deprecated gset gmap.
From iris.base_logic Require Import big_op saved_prop.
From iris_atomic Require Import misc peritem sync evmap.
Import dec_agree.
Definition doOp : val :=
λ: "p",
match: !"p" with
......
......@@ -2,10 +2,11 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap dec_agree.
From iris.algebra Require Import auth frac gmap deprecated.
From iris.prelude Require Import countable.
From iris.base_logic Require Import big_op auth fractional.
Import uPred.
Import uPred dec_agree.
Section lemmas.
Lemma pair_l_frac_op' (p q: Qp) (g g': val):
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth gmap dec_agree csum.
From iris.algebra Require Import frac auth gmap deprecated csum.
From iris.base_logic Require Import big_op.
From iris_atomic Require Export treiber misc evmap.
Import dec_agree.
Section defs.
Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
Context (R: val iProp Σ) `{ x, TimelessP (R x)}.
......
......@@ -3,7 +3,7 @@
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import dec_agree frac.
From iris.algebra Require Import frac.
From iris_atomic Require Import sync.
Import uPred.
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth gmap dec_agree csum.
From iris.algebra Require Import frac auth gmap deprecated csum.
From iris.base_logic Require Import big_op.
From iris_atomic Require Import atomic misc.
Import dec_agree.
Definition new_stack: val := λ: <>, ref (ref NONE).
Definition push: val :=
......
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