From 64ec23fe9ddf6e29046712ac6302435452ab82f6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 22 Sep 2017 10:52:51 +0200
Subject: [PATCH] update CI and build system and Iris

---
 .gitignore              |  4 ++--
 .gitlab-ci.yml          |  2 +-
 Makefile                | 38 ++++++++++++++++++++------------
 Makefile.coq.local      |  5 +++++
 awk.Makefile            |  3 ++-
 build/opam-ci.sh        | 48 ++++++++++++++++++++++++++++++-----------
 build/opam-pins.sh      | 26 ----------------------
 opam                    |  7 ++----
 opam.pins               |  1 -
 theories/.dir-locals.el |  1 -
 theories/flat.v         |  8 +++----
 11 files changed, 76 insertions(+), 67 deletions(-)
 create mode 100644 Makefile.coq.local
 delete mode 100755 build/opam-pins.sh
 delete mode 100644 opam.pins
 delete mode 100644 theories/.dir-locals.el

diff --git a/.gitignore b/.gitignore
index 5aced84..ba20ddf 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,6 @@
 *~
 *.bak
 Makefile.coq
+Makefile.coq.conf
 .coq-native/
-iris-enabled
-
+build-dep
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e8ebecf..5d24a4f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -16,7 +16,7 @@ variables:
   - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(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:
diff --git a/Makefile b/Makefile
index 7bfa06f..cff640c 100644
--- a/Makefile
+++ b/Makefile
@@ -1,38 +1,48 @@
-# 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 $@
 
 all: Makefile.coq
 	+@make -f Makefile.coq all
+.PHONY: all
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
 	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
+.PHONY: clean
 
-# 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/opam: opam
+	# Create the build-dep package.
+	@mkdir -p build-dep
+	@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
+
+build-dep: build-dep/opam 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.
+	# Add the pin and (re)install build-dep package.
+	@# 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".dev "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \
+	  opam reinstall "$$BUILD_DEP_PACKAGE"
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
 _CoqProject: ;
 awk.Makefile: ;
+opam: ;
 
-# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
+# Phony wildcard targets
 phony: ;
-.PHONY: all clean phony
+.PHONY: phony
diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 0000000..b261de9
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,5 @@
+uninstall::
+	@# This makes sure we also delete stale files in the destination directory
+	$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
+	echo "RM in $$df" &&\
+	if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi
diff --git a/awk.Makefile b/awk.Makefile
index 09ded0a..74f7d57 100644
--- a/awk.Makefile
+++ b/awk.Makefile
@@ -11,7 +11,8 @@
 
 # Patch the uninstall target to work properly, and to also uninstall stale files.
 # Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
-/^uninstall:/ {
+# This (and the section above) can be removed once we no longer support Coq 8.6.
+/^uninstall: / {
 	print "uninstall:";
 	print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
 	getline;
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 20d87f9..27ae623 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -1,42 +1,66 @@
 #!/bin/bash
 set -e
-# This script installs the build dependencies for CI builds.
+## This script installs the build dependencies for CI builds.
+function run_and_print() {
+    echo "$ $@"
+    "$@"
+}
 
 # Prepare OPAM configuration
 export OPAMROOT="$(pwd)/opamroot"
 export OPAMJOBS="$((2*$CPU_CORES))"
 export OPAM_EDITOR="$(which false)"
 
-# Make sure we got a good OPAM
-test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
+# Make sure we got a good OPAM.
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y)
 eval `opam conf env`
+# Delete old pins from opam.pins times.
+run_and_print opam pin remove coq-stdpp -n
+run_and_print opam pin remove coq-iris -n
+# Make sure the pin for the builddep package is not stale.
+run_and_print make build-dep/opam
+
+# Get us all the latest repositories
 if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
     # last update was more than a day ago
-    opam update
+    run_and_print opam update
 else
-    echo "[opam-ci] Not updating opam."
+    # only update iris-dev
+    if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi
 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-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/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev
+test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
+test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+echo
+
+# 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
+# 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"
     else
         echo "[opam-ci] Pinning $PACKAGE to $VERSION"
-        opam pin add "$PACKAGE" "$VERSION" -k version -y
+        run_and_print opam pin add "$PACKAGE" "$VERSION" -k version -y
     fi
 done
 
-# Install build-dependencies
+# Upgrade cached things.
+echo
+echo "[opam-ci] Upgrading opam"
+run_and_print 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 5291cb2..0000000
--- 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 3e4c2bf..c59c276 100644
--- a/opam
+++ b/opam
@@ -1,16 +1,13 @@
 opam-version: "1.2"
 name: "coq-iris-atomic"
-version: "dev"
 maintainer: "Zhen Zhang, Ralf Jung"
 authors: "Zhen Zhang"
 homepage: "http://plv.mpi-sws.org/iris/"
 bug-reports: "https://gitlab.mpi-sws.org/FP/iris-atomic/issues"
 dev-repo: "https://gitlab.mpi-sws.org/FP/iris-atomic.git"
-build: [
-  [make "-j%{jobs}%"]
-]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_atomic" ]
 depends: [
-  "coq-iris"
+  "coq-iris" { (= "dev.2017-09-21.3") | (= "dev") }
 ]
diff --git a/opam.pins b/opam.pins
deleted file mode 100644
index 9087d1e..0000000
--- a/opam.pins
+++ /dev/null
@@ -1 +0,0 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33
diff --git a/theories/.dir-locals.el b/theories/.dir-locals.el
deleted file mode 100644
index a1777c6..0000000
--- a/theories/.dir-locals.el
+++ /dev/null
@@ -1 +0,0 @@
-((coq-mode . ((coq-prog-name . "/usr/local/bin/coqtop"))))
diff --git a/theories/flat.v b/theories/flat.v
index 35ec113..2a65a35 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -154,7 +154,7 @@ Section proof.
       iModIntro. wp_match. wp_proj. wp_proj.
       wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
       { iApply "Hf'". iFrame. }
-      iIntros (v) "[HR HQ]". wp_value.
+      iIntros (v) "[HR HQ]".
       iInv N as "Hx" "Hclose".
       iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
       * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
@@ -191,12 +191,12 @@ Section proof.
   Proof.
     induction xs as [|x xs' IHxs].
     - iIntros (hd Φ) "[Hxs ?] HΦ".
-      simpl. wp_rec. wp_value. wp_let.
+      simpl. wp_rec. wp_let.
       iDestruct "Hxs" as (?) "Hhd".
       wp_load. wp_match. by iApply "HΦ".
     - iIntros (hd Φ) "[Hxs HRf] HΦ". simpl.
       iDestruct "Hxs" as (hd' ?) "(Hhd & #Hinv & Hxs')".
-      wp_rec. wp_value. wp_let. wp_bind (! _)%E.
+      wp_rec. wp_let. wp_bind (! _)%E.
       iInv N as "H" "Hclose".
       iDestruct "H" as (ts p) "[>% #?]". subst.
       wp_load. iMod ("Hclose" with "[]").
@@ -291,7 +291,7 @@ Section proof.
     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.
-      wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
+      wp_let. iDestruct (uPred.ofe_funC_equivI with "Heq") as "Heq".
       iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
     - iExFalso. iCombine "Hx" "Hx'" as "Hx".
       iDestruct (own_valid with "Hx") as %[_ H1].
-- 
GitLab