From cc1b8ab0262e334b2c09bb1b13cfef619471a356 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Sep 2017 15:52:53 +0200
Subject: [PATCH] update Iris; get rid of opam.pins
---
.gitignore | 3 +--
.gitlab-ci.yml | 4 ++--
Makefile | 28 ++++++++++++++++------------
build/opam-ci.sh | 24 +++++++++++++++++++-----
build/opam-pins.sh | 26 --------------------------
opam | 6 ++----
opam.pins | 1 -
theories/lang/lang.v | 2 +-
theories/lang/races.v | 16 ++++++++--------
theories/lifetime/model/creation.v | 8 ++++++--
theories/lifetime/model/reborrow.v | 2 +-
theories/typing/type.v | 2 +-
12 files changed, 57 insertions(+), 65 deletions(-)
delete mode 100755 build/opam-pins.sh
delete mode 100644 opam.pins
diff --git a/.gitignore b/.gitignore
index ecdc2641..e9ad8dad 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,5 @@
*~
*.bak
.coq-native/
-iris-enabled
+build-dep/
Makefile.coq*
-opamroot
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 28d98512..9fbfc552 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -16,7 +16,7 @@ variables:
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
- 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
cache:
- key: "coq$COQ_VERSION-ssr$SSR_VERSION"
+ key: "coq.$COQ_VERSION-ssr.$SSR_VERSION"
paths:
- opamroot/
only:
@@ -34,7 +34,7 @@ lrust-coq8.6.1:
variables:
COQ_VERSION: "8.6.1"
SSR_VERSION: "1.6.1"
- VALIDATE: 1
+ VALIDATE: "1"
artifacts:
paths:
- build-time.txt
diff --git a/Makefile b/Makefile
index 7bfa06f8..a8c1e057 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,3 @@
-# Process flags
-ifeq ($(Y), 1)
- YFLAG=-y
-endif
-
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
@@ -15,18 +10,27 @@ clean: Makefile.coq
find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
-# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
+# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies
-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 opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
- opam install opam-builddep-temp --deps-only $(YFLAG)
- opam pin remove opam-builddep-temp
+build-dep: phony
+ @# We want opam to not just instal the build-deps now, but to also keep satisfying these
+ @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
+ @# that are incompatible with our build requirements.
+ @# To achieve this, we create a fake opam package that has our build-dependencies as
+ @# dependencies, but does not actually install anything.
+ mkdir -p build-dep
+ # Create the build-dep package, add the pin and (re)install it.
+ @sed <opam 's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/' > build-dep/opam
+ @fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
+ @# Reinstallation is needed in case the pin already exists, but the builddep package changed.
+ @BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
+ opam pin add "$$BUILD_DEP_PACKAGE" "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \
+ opam reinstall "$$BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 20d87f9d..94c738e5 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -1,6 +1,6 @@
#!/bin/bash
set -e
-# This script installs the build dependencies for CI builds.
+## This script installs the build dependencies for CI builds.
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
@@ -16,15 +16,24 @@ if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
else
echo "[opam-ci] Not updating opam."
fi
-test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
+test -d "$OPAMROOT/repo/coq-extra-dev" && opam repo remove coq-extra-dev
test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
-# Install fixed versions of some dependencies
+# Make sure we have no undesired pins left from opam.pins times
+opam pin remove coq-stdpp -n
+opam pin remove coq-iris -n
+
+# We really want to run all of the following in one opam transaction, but due to opam limitations,
+# that is not currently possible.
+
+# Install fixed versions of some dependencies.
echo
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
VERSION="$1" ; shift
+
# Check if the pin is already set
if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
echo "[opam-ci] $PACKAGE already pinned to $VERSION"
@@ -34,9 +43,14 @@ while (( "$#" )); do # while there are arguments left
fi
done
-# Install build-dependencies
+# Upgrade cached things.
+echo "[opam-ci] Upgrading opam"
+opam upgrade -y
+
+# Install build-dependencies.
echo
-make build-dep Y=1
+echo "[opam-ci] Installing build-dependencies"
+make build-dep OPAMFLAGS=-y
# done
echo
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
deleted file mode 100755
index 5291cb23..00000000
--- a/build/opam-pins.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/bash
-set -e
-## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
-## Usage:
-## ./opam-pins.sh < opam.pins
-
-if ! which curl >/dev/null; 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/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
-done
diff --git a/opam b/opam
index e92373cb..b5f67af6 100644
--- a/opam
+++ b/opam
@@ -6,11 +6,9 @@ authors: "The RustBelt Team"
homepage: "http://plv.mpi-sws.org/rustbelt/"
bug-reports: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq/issues"
dev-repo: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq.git"
-build: [
- [make "-j%{jobs}%"]
-]
+build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-iris"
+ "coq-iris" { (= "dev.2017-09-19.0") | (= "dev") }
]
diff --git a/opam.pins b/opam.pins
deleted file mode 100644
index 2c200453..00000000
--- a/opam.pins
+++ /dev/null
@@ -1 +0,0 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e2c5c25aea886acc7d0925d435fe856ffa6ac14
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index b7abe7f6..e3c8981a 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -443,7 +443,7 @@ Proof.
assert (∀ (l : loc) ls (X : gset block),
l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
{ induction 1; set_solver. }
- rewrite /fresh_block /shift_loc /= -not_elem_of_dom -elem_of_elements.
+ rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
move=> /(help _ _ ∅) /=. apply is_fresh.
Qed.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 5baaf0a7..8fa7a547 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -120,17 +120,17 @@ Proof.
destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
(* Oh my. FIXME. *)
- eapply lit_neq_state; last done.
- setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
- cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+ setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+ cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
- eapply lit_eq_state; last done.
- setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
- cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+ setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+ cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
- eapply lit_neq_state; last done.
- setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
- cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+ setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+ cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
- eapply lit_eq_state; last done.
- setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
- cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+ setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+ cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
Qed.
Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' o1 a2 l :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index befd40f2..b25469ef 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -55,6 +55,10 @@ Proof.
iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame.
Qed.
+(* FIXME: Get rid of this hack. If we just remove this line, the next lemma
+ statement breaks. *)
+Remove Hints finite.finite_countable : typeclass_instances.
+
Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
K ⊥ K' →
@@ -168,12 +172,12 @@ Proof.
iIntros (κ [[Hκ HκI]%elem_of_filter HκK]%elem_of_difference) "Halive".
rewrite /lft_inv. iLeft. iFrame "Halive". iPureIntro.
apply lft_alive_in_insert_false; last done.
- move: HκK. rewrite elem_of_kill_set -elem_of_dom. set_solver +HκI.
+ move: HκK. rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)). set_solver +HκI.
- iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!#".
rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
+ iLeft. iFrame. iPureIntro.
apply lft_alive_in_insert_false; last done. intros ?.
- assert (κ ∈ K) by (rewrite elem_of_kill_set -elem_of_dom HI elem_of_union; auto).
+ assert (κ ∈ K) by (rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)) HI elem_of_union; auto).
eapply HK'', Hκ. rewrite elem_of_union. auto.
+ iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
Qed.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 2e7d4d9a..f73146de 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -70,7 +70,7 @@ Proof.
iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hnâ—".
iIntros (I) "Hinv [HP HPb] #Hκ†".
rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
- iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
+ iDestruct (own_bor_auth with "HI Hi") as %?%(elem_of_dom (D:=gset lft)).
iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
rewrite lft_inv_alive_unfold.
iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 21cefb19..73f80838 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -13,7 +13,7 @@ Class typeG Σ := TypeG {
type_frac_borrowG :> frac_borG Σ
}.
-Definition lftE := ↑lftN.
+Definition lftE : coPset := ↑lftN.
Definition lrustN := nroot .@ "lrust".
Definition shrN := lrustN .@ "shr".
--
GitLab