new opam-based CI and build system

.gitignore

@@ -11,3 +11,4 @@
 .coq-native/
 iris-enabled
 Makefile.coq
+opamroot

.gitlab-ci.yml

-image: coq:8.5
+image: opam
 
-stages:
-  - iris
-  - lrust
-
-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
-
-lrust:
-  stage: lrust
+lrust-coq8.5.3:
   tags:
   - coq
   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.3-2"
+    paths:
+    - opamroot/
   only:
   - master
   - ci

.gitmodules

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

Makefile

@@ -12,15 +12,10 @@ clean: Makefile.coq
 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
+build-dep:
+	cat opam.pins | build/opam-pins.sh
+	opam pin add coq-lambda-rust "$$(pwd)#HEAD" -k git -y -n
+	opam install coq-lambda-rust --deps-only -y
 
 _CoqProject: ;
 

README.md

@@ -6,21 +6,17 @@ This is the Coq formalization of lambda-Rust.
 
 This version is known to compile with:
 
- - Coq 8.5pl2
+ - Coq 8.5pl3
  - Ssreflect 1.6
+ - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
 
-You will furthermore need an up-to-date version of
-[Iris](https://gitlab.mpi-sws.org/FP/iris-coq/).  Run `git submodule status` to
-see which git commit of Iris is known to work.  You can pick between using a
-system-installed Iris (from Coq's `user-contrib`) or a version of Iris locally
-compiled for lambda-Rust.
+The easiest way to install the correct versions of the dependencies is through
+opam.  Once you got opam set up, just run `make build-dep` to install the right
+versions of the dependencies.
 
-## Building Instructions
+Alternatively, you can manually determine the required Iris commit by consulting
+the `opam.pins` file.
 
-To use the system-installed Iris (which is the default), run `make iris-system`.
-This only works if you previously built and installed a compatible version of the
-Iris Coq formalization.  To use a local Iris (which will always be the right
-version), run `make iris-local`.  Run this command again later to update the
-local Iris, in case the preferred Iris version changed.
+## Building Instructions
 
-Now run `make` to build the full development.
+Run `make` to build the full development.

_CoqProject

 -Q theories lrust
--Q iris-enabled iris
 theories/adequacy.v
 theories/derived.v
 theories/heap.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 -n)
+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...
+
+# Pick fixed versions of some dependencies
+echo
+for PIN in "${@}"
+do
+    echo "Applying pin: $PIN"
+    opam pin add $PIN -k version -y -n
+done
+
+# Install/upgrade build-dependencies
+echo
+opam upgrade -y
+make build-dep
+
+# done
+echo
+coqc -v

build/opam-pins.sh

+#!/bin/bash
+set -e
+# Process an opam.pins file from 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"
+    fi
+    echo "Applying pin: $PACKAGE -> $PIN"
+    opam pin add "$PACKAGE" "$PIN" -k git -y -n
+done

iris @ 243fdd13

-Subproject commit 243fdd139ccdf1370e5b186650e4323d5e73e54b

opam

@@ -13,5 +13,5 @@ build: [
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dep.lrust") }
+  "coq-iris"
 ]

opam.pins

+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#243fdd139ccdf1370e5b186650e4323d5e73e54b