use OPAM-based CI

.gitlab-ci.yml

-image: coq:8.5
+image: ralfjung/opam-ci:latest
 
-stages:
-  - iris
-  - iris-atomic
-
-iris:
-  stage: iris
-  tags:
-  - coq
-  script:
-  - coqc -v
-  # see if the Iris submodule needs cleaning, then build it
-  - 'git submodule status iris | egrep "^ " || (git submodule update --init iris && cd iris && git clean -xfd)'
-  - 'cd iris && make -j8'
-  only:
-  - master
-  - ci
-
-iris-atomic:
-  stage: iris-atomic
-  tags:
-  - coq
+iris_atomic-coq8.5.3:
   script:
-  - coqc -v
-  # prepare the environment, safeguard against outdated submodule
-  - 'git submodule status iris | egrep "^ "'
-  - 'ln -s iris iris-enabled'
-  # build local repo
+  # prepare
+  - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
+  # build
   - 'time make -j8'
+  cache:
+    key: "coq8.5"
+    paths:
+    - opamroot/
   only:
   - master
   - ci

.gitmodules

-[submodule "iris"]
-	path = iris
-	url = https://gitlab.mpi-sws.org/FP/iris-coq.git

Makefile

+# 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 ?=
+
+ifeq ($(COQ_VERSION), 8.6)
+	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection
+endif
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@
 
-# Compile this project
 all: Makefile.coq
 	+@make -f Makefile.coq all
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
+	find \( -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
 Makefile.coq: _CoqProject Makefile
-	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
-
-# Use local Iris dependency
-iris-local:
-	git submodule update --init iris # If not initialized, then initialize; If not updated with this remote, then update
-	ln -nsf iris iris-enabled # If not linked, then link
-	+make -C iris -f Makefile # If not built, then build
-
-# Use system-installed Iris dependency
-iris-system: clean
-	rm -f iris-enabled
-
-_CoqProject: ;
-
+	@# we want to pass the correct name to coq_makefile or it will be confused.
+	coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
+	mv Makefile.coq Makefile.coq.tmp
+	@# The sed script is for Coq 8.5 only, it fixes 'make verify'.
+	@# The awk script fixes 'make uninstall'.
+	sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' < Makefile.coq.tmp \
+	  | awk '/^uninstall:/{print "uninstall:";print "\tif [ -d \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ ]; then find \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ -name \"*.vo\" -print -delete; fi";getline;next}1' > 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 coq-iris-atomic "$$(pwd)#HEAD" -k git -n -y
+	opam install coq-iris-atomic --deps-only $(YFLAG)
+	opam pin remove coq-iris-atomic
+
+# some fiels that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
+_CoqProject: ;
 
+# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
 phony: ;
-
-.PHONY: all clean phony iris-local iris-system
+.PHONY: all clean phony

_CoqProject

 -Q theories iris_atomic
--Q iris-enabled iris
 theories/atomic.v
 theories/sync.v
 theories/atomic_incr.v

build/opam-ci.sh

+#!/bin/bash
+set -e
+# This script installs the build dependencies for CI builds.
+
+# Prepare OPAM configuration
+export OPAMROOT="$(pwd)/opamroot"
+export OPAMJOBS=16
+export OPAM_EDITOR="$(which false)"
+
+# Make sure we got a good OPAM
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
+eval `opam conf env`
+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
+opam update
+opam install ocamlfind -y # Remove this once the Coq crew fixed their package...
+
+# Install fixed versions of some dependencies
+echo
+for PIN in "${@}"
+do
+    echo "Applying pin: $PIN"
+    opam pin add $PIN -k version -y
+done
+
+# Install build-dependencies
+echo
+make build-dep Y=1
+
+# done
+echo
+coqc -v

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
+
+# 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" 2> /dev/null | "$0"
+    fi
+    echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
+    opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+    echo
+done

iris @ b72a3301

-Subproject commit b72a3301d7ff957cfbb06d06bba85fb4ee9a2c39

opam

+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}%"]
+]
+install: [make "install"]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_atomic" ]
+depends: [
+  "coq-iris"
+]

opam.pins

+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b72a3301d7ff957cfbb06d06bba85fb4ee9a2c39