new build-dep handling without opam.pins

.gitignore

@@ -9,5 +9,6 @@
 *~
 *.bak
 .coq-native/
+build-dep/
 Makefile.coq*
 *.crashcoqide

.gitlab-ci.yml

@@ -47,7 +47,7 @@ iris-coq8.6.1:
   variables:
     COQ_VERSION: "8.6.1"
     SSR_VERSION: "1.6.1"
-    VALIDATE: 1
+    VALIDATE: "1"
   artifacts:
     paths:
     - build-time.txt

Makefile

-# 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,16 +10,25 @@ 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:
-	opam pin add opam-builddep-temp "$$(pwd)" -k path -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
+	@echo "build-dep package is $$BUILD_DEP_PACKAGE"
+	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
+	@# Compute the package name, add the pin and install it
+	opam pin add "$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" "$$(pwd)/build-dep" -k path $(OPAMFLAGS)
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;

build/opam-ci.sh

@@ -16,7 +16,7 @@ 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
@@ -25,11 +25,15 @@ test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-s
 opam pin remove coq-stdpp -n
 opam pin remove coq-iris -n
 
-# Install fixed versions of some dependencies
+# 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"
@@ -39,12 +43,12 @@ while (( "$#" )); do # while there are arguments left
     fi
 done
 
-# Upgrade cached things
+# Upgrade cached things.
 opam upgrade -y
 
-# Install build-dependencies
+# Install build-dependencies.
 echo
-make build-dep Y=1
+make build-dep OPAMFLAGS=-y
 
 # done
 echo

opam

@@ -7,11 +7,9 @@ homepage: "http://iris-project.org/"
 bug-reports: "https://gitlab.mpi-sws.org/FP/iris-coq/issues"
 license: "BSD"
 dev-repo: "https://gitlab.mpi-sws.org/FP/iris-coq.git"
-build: [
-  [make "-j%{jobs}%"]
-]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ]
+remove: ["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'"]
 depends: [
   "coq" { (>= "8.6.1" & < "8.8~") }
   "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev")) }