CI: depend on std++ via opam; prepare for automatic opam releases

.gitlab-ci.yml

 image: ralfjung/opam-ci:latest
 
+stages:
+  - build
+  - opam
+
 variables:
   CPU_CORES: "9"
 
 .template: &template
+  stage: build
   tags:
   - fp-timing
   script:
@@ -23,6 +28,14 @@ variables:
   - master
   - /^ci/
 
+opam:
+  stage: opam
+  script:
+  # Send a trigger to the repository doing the work
+  - curl --fail -X POST -F "token=$OPAM_UPDATE_SECRET" -F "ref=master" -F "variables[REPO]=${CI_PROJECT_URL}.git" -F "variables[REF]=$CI_COMMIT_REF_NAME" -F "variables[SHA]=$CI_COMMIT_SHA" -F "variables[NAME]=coq-iris" https://gitlab.mpi-sws.org/api/v3/projects/581/trigger/builds
+  only:
+  - master
+
 iris-coq8.7:
   <<: *template
   variables:

Makefile

@@ -22,9 +22,7 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
 
 # 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 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/opam-ci.sh

@@ -19,6 +19,11 @@ 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/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+
+# Make sure we have no undesired pins left from opam.pins times
+opam pin remove coq-stdpp -n
+opam pin remove coq-iris -n
 
 # Install fixed versions of some dependencies
 echo
@@ -34,6 +39,9 @@ while (( "$#" )); do # while there are arguments left
     fi
 done
 
+# Upgrade cached things
+opam upgrade -y
+
 # Install build-dependencies
 echo
 make build-dep Y=1

build/opam-pins.sh

-#!/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

descr

+This is the Coq development of the Iris Project.

opam

@@ -13,7 +13,7 @@ build: [
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ]
 depends: [
-  "coq" { (>= "8.6.1" & < "8.8~") } # replace with (= "dev") if you want to test against a development version of Coq
+  "coq" { (>= "8.6.1" & < "8.8~") }
   "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev")) }
-  "coq-stdpp"
+  "coq-stdpp" { ((= "dev.2017-09-18.1") | (= "dev")) }
 ]

opam.pins

-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 7d7c9871312719a4e1296d52eb95ea0ac959249f