From d46265ee7f32d720adb6d3272d839227d2569877 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 29 Nov 2016 13:57:55 +0100
Subject: [PATCH] update iris and fix build system to properly recompile iris
when needed
---
Makefile | 8 +-------
build/opam-ci.sh | 9 ++++-----
build/opam-pins.sh | 45 ++++++++++++++++++++++++++++++++++++++++++---
opam.pins | 2 +-
4 files changed, 48 insertions(+), 16 deletions(-)
diff --git a/Makefile b/Makefile
index aac88873..07992565 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,3 @@
-# Process flags
-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 ?=
@@ -33,9 +28,8 @@ Makefile.coq: _CoqProject Makefile
# Install build-dependencies
build-dep:
cat opam.pins | build/opam-pins.sh
- opam upgrade $(YFLAG)
opam pin add coq-lambda-rust "$$(pwd)#HEAD" -k git -n -y
- opam install coq-lambda-rust --deps-only $(YFLAG)
+ opam install coq-lambda-rust --deps-only -y
# some fiels that do *not* need to be forwarded to Makefile.coq
Makefile: ;
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 95f19e83..35117daf 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -16,18 +16,17 @@ test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.
opam update
opam install ocamlfind -y # Remove this once the Coq crew fixed their package...
-# Pick fixed versions of some dependencies
+# Install fixed versions of some dependencies
echo
for PIN in "${@}"
do
echo "Applying pin: $PIN"
- opam pin add $PIN -k version -y -n
+ opam pin add $PIN -k version -y
done
-# Install/upgrade build-dependencies
+# Install build-dependencies
echo
-opam upgrade -y
-make build-dep Y=1
+make build-dep
# done
echo
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
index 784100b2..d08fb314 100755
--- a/build/opam-pins.sh
+++ b/build/opam-pins.sh
@@ -1,13 +1,52 @@
#!/bin/bash
set -e
-# Process an opam.pins file from stdin.
+## Process an opam.pins file from stdin: Apply the pins and install the packages.
+## Usage: (Arguments have to be given in the given order!)
+## ./opam-pins.sh [--recursive]
+## Arguments:
+## -- recursive This is a recurisve call of the script to itself
+## (you should not pass this argument yourself manually).
+
+# Parse arguments
+if [[ "$1" == "--recursive" ]]; then
+ shift
+ IS_TOPLEVEL=0
+else
+ # We are the toplevel call. Record the old pin state.
+ IS_TOPLEVEL=1
+ OLD_PINS="$(mktemp)"
+ opam pin list > "$OLD_PINS"
+fi
+
+if [[ "$1" == "-n" ]]; then
+ shift
+ NFLAG="-n"
+else
+ NFLAG=""
+fi
+
+# Process stdin
while read PACKAGE PIN; do
if echo "$PIN" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
# an MPI URL -- try doing recursive pin processing
URL=$(echo "$PIN" | sed 's|#|/raw/|')/opam.pins
- curl -f "$URL" 2> /dev/null | "$0"
+ curl -f "$URL" 2> /dev/null | "$0" --recursive
fi
- echo "Applying pin: $PACKAGE -> $PIN"
+ echo "[opam-pins] Applying pin: $PACKAGE -> $PIN"
opam pin add "$PACKAGE" "$PIN" -k git -y -n
+ echo
done
+
+# If we are the toplevel call, see what pins changed and reinstall if necessary
+if [[ "$IS_TOPLEVEL" == "1" ]]; then
+ NEW_PINS="$(mktemp)"
+ opam pin list > "$NEW_PINS"
+ # Compare the pin lists and filter for the changed package names
+ PACKAGES=$(diff -u0 "$OLD_PINS" "$NEW_PINS" | egrep '^[+][^+]' | sed 's/+\([a-z0-9-]\+\)[ .].*$/\1/')
+ if [[ -n "$PACKAGES" ]]; then
+ echo "[opam-pins] Reinstalling packages:" $PACKAGES
+ opam reinstall $PACKAGES -y
+ fi
+ rm "$OLD_PINS" "$NEW_PINS"
+fi
diff --git a/opam.pins b/opam.pins
index 3c8dba6d..febb0c13 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#ce32b224b90b6c91eae1ddb60505107b2f66b263
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#90f773c0eb319320932edfd4a5fbe878673bb3de
--
GitLab