diff --git a/Makefile b/Makefile
index 9ae0abe160351d96193e9d912c75949c14161c48..df9d03fb53ba382cf31b6221438b1bd6eb2bc2ee 100644
--- a/Makefile
+++ b/Makefile
@@ -3,14 +3,6 @@ ifeq ($(Y), 1)
YFLAG=-y
endif
-# Determine Coq version
-COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
-COQ_MAKEFILE_FLAGS ?=
-
-ifeq ($(COQ_VERSION), 8.6)
- COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-endif
-
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
@@ -32,9 +24,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
build-dep:
build/opam-pins.sh < opam.pins
opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
- opam pin add coq-lambda-rust "$$(pwd)#HEAD" -k git -n -y
- opam install coq-lambda-rust --deps-only $(YFLAG)
- opam pin remove coq-lambda-rust
+ opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
+ opam install opam-builddep-temp --deps-only $(YFLAG)
+ opam pin remove opam-builddep-temp
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
diff --git a/_CoqProject b/_CoqProject
index edaf7f5f49f9b5b3a0c923d3d8fc63841f10a1db..65799cfc1c5a0f6fab9b2b84cef4518e3b7d9163 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,5 @@
-Q theories lrust
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/lifetime/model/definitions.v
theories/lifetime/model/faking.v
theories/lifetime/model/creation.v
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
index 669cd99b833df5259808f3b8f3fae1f96f466271..aafd133f2e420f9f6fa737ad654482b6b70c1a58 100755
--- a/build/opam-pins.sh
+++ b/build/opam-pins.sh
@@ -4,18 +4,23 @@ set -e
## Usage:
## ./opam-pins.sh < opam.pins
+if ! which curl; then
+ echo "opam-pins needs curl. Please install curl and try again."
+ exit 1
+fi
+
# Process stdin
while read PACKAGE URL HASH; do
if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
echo "[opam-pins] Recursing into $URL"
# an MPI URL -- try doing recursive pin processing
- curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
+ curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
fi
if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
echo "[opam-pins] $PACKAGE already at commit $HASH"
else
echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+ echo
fi
- echo
done
diff --git a/opam.pins b/opam.pins
index 642f2e56a3400e35bac618a9b5ed355c9fef0386..8868ac832f86730265e263d3f020bf51de135b91 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b0418bd57b9341dbf5e58669c689201daa561bd7
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b863cfd7640f5dccb14c17e9ffefb475f1b7d0d8
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index b5c53cd372102560077256c6852c4a0370004f16..f3f69a16ec4acd4a46b088adfc0446138b8e090f 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -1,5 +1,5 @@
From Coq Require Import Min.
-From iris.prelude Require Import coPset.
+From stdpp Require Import coPset.
From iris.algebra Require Import cmra_big_op gmap frac agree.
From iris.algebra Require Import csum excl auth.
From iris.base_logic Require Import big_op lib.fractional.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index e770632fbf7d41725a99a49e31628cf26450cfb4..96df4989001e658b8b1338391126d58c3746768e 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,6 +1,6 @@
From iris.program_logic Require Export language ectx_language ectxi_language.
-From iris.prelude Require Export strings.
-From iris.prelude Require Import gmap.
+From stdpp Require Export strings.
+From stdpp Require Import gmap.
Set Default Proof Using "Type".
Open Scope Z_scope.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 1ba1a13fa8399c8656945f0235f17e2b5b30d6aa..6cc6f95bddf46888244d815208fd880e2c9e425d 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import gmap.
+From stdpp Require Import gmap.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import adequacy.
From lrust.lang Require Import tactics.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 99dc74648ca31bca924fd04e2d46dfb1beb3bafe..7ebfc8c5e1f8b48e8c9b3668f79e216f8e868400 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import fin_maps.
+From stdpp Require Import fin_maps.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index c6171e0bc002b1cc9a9da73bafb35c95dd552770..4684b65d115f0ae967368e629234dcd33e5d3632 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -1,5 +1,5 @@
From iris.algebra Require Import frac.
-From iris.prelude Require Export gmultiset strings.
+From stdpp Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes fractional.
Set Default Proof Using "Type".
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index c373300da32e5cdf98f408aca4d3d10062461164..ac08fb9dadd677ec76c972688d96d7dd314ccb55 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -182,7 +182,7 @@ Section ref_functions.
- destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
iExists None. iFrame. iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
- apply op_local_update_cancellable_empty, _. }
+ apply cancel_local_update_empty, _. }
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
@@ -191,7 +191,7 @@ Section ref_functions.
iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc.
rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
- apply (op_local_update_cancellable_empty (reading_st q ν)), _. }
+ apply (cancel_local_update_empty (reading_st q ν)), _. }
iExists ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
iSplitR; first done. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 396076aa1f2fdd951792dde4fda5694df4e885c3..fa185e27664170c2c25f383903b3be0cfba20f5e 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -184,7 +184,7 @@ Section refcell_functions.
{ apply auth_update_alloc,
(op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
split; [|split].
- - by rewrite -Hag /= agree_idemp.
+ - by rewrite /= -Hag agree_idemp.
- change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index a6dfcd1244e8f67f1b73690b4055b1290a70bc7f..e3e528509b0b42e3d578f1975ed676a98760d888 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -147,7 +147,7 @@ Section refmut_functions.
iMod ("Hcloseβ" with ">[H↦lrc H◠H◯ Hb] Hna") as "[Hβ Hna]".
{ iExists None. iFrame. iMod (own_update_2 with "Hâ— Hâ—¯") as "$"; last done.
apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
- apply op_local_update_cancellable_empty, _. }
+ apply cancel_local_update_empty, _. }
iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
iAssert (elctx_interp [☀ α] qE) with "[Hα]" as "HE".
{ by rewrite /elctx_interp big_sepL_singleton. }