Merge branch 'ci' into 'master'

New opam-based CI and build system

Submodules are gone. If you have opam set up, `make build-dep` will install the right version of everything.

This is *not* exactly what we discussed last week; I think I found something better. In particular, this approach lets us also figure out for historic lambdaRust versions, which commit of iris they needed. No magic branches in other repositories are needed, everything is local here.

Essentially, since the `opam` files do not support documenting detailed enough version information, I added a new file `opam.pins` that "enhances" the opam file appropriately. This file contains pins (one per line) that have to be set to compile lambdaRust. The script in `build/opam-pins.sh` applies those pins - and crucially, it does so recursively: When it finds a pin that is one of our git repositories, it will download the `opam.pins` files for *that* commit and also apply its pins. So if lambdaRust pins a particular commit of iris, and iris pins a particular commit of the prelude, then doing `make build-dep` in lambdaRust will follow this transitive chain and install the correct versions of iris and the prelude.

Cc @jjourdan @robbertkrebbers

See merge request !2

.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