From 73391eeb4cd223e011caf705bc1a077ab8be459b Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 24 Nov 2016 17:48:07 +0100
Subject: [PATCH] new opam-based CI and build system
---
.gitignore | 1 +
.gitlab-ci.yml | 34 +++++++++-------------------------
.gitmodules | 3 ---
Makefile | 13 ++++---------
README.md | 22 +++++++++-------------
_CoqProject | 1 -
build/opam-ci.sh | 34 ++++++++++++++++++++++++++++++++++
build/opam-pins.sh | 13 +++++++++++++
iris | 1 -
opam | 2 +-
opam.pins | 1 +
11 files changed, 72 insertions(+), 53 deletions(-)
create mode 100755 build/opam-ci.sh
create mode 100755 build/opam-pins.sh
delete mode 160000 iris
create mode 100644 opam.pins
diff --git a/.gitignore b/.gitignore
index e0c831da..30ee28f8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,3 +11,4 @@
.coq-native/
iris-enabled
Makefile.coq
+opamroot
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 20e39e3f..d65bd34b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,33 +1,17 @@
-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
diff --git a/.gitmodules b/.gitmodules
index 941d913e..e69de29b 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +0,0 @@
-[submodule "iris"]
- path = iris
- url = https://gitlab.mpi-sws.org/FP/iris-coq.git
diff --git a/Makefile b/Makefile
index fa51a2f7..da7fa86f 100644
--- a/Makefile
+++ b/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: ;
diff --git a/README.md b/README.md
index b55b3347..a7cda08d 100644
--- a/README.md
+++ b/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.
diff --git a/_CoqProject b/_CoqProject
index cd1cc58d..a8fc5450 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,4 @@
-Q theories lrust
--Q iris-enabled iris
theories/adequacy.v
theories/derived.v
theories/heap.v
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
new file mode 100755
index 00000000..dadba5da
--- /dev/null
+++ b/build/opam-ci.sh
@@ -0,0 +1,34 @@
+#!/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
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
new file mode 100755
index 00000000..784100b2
--- /dev/null
+++ b/build/opam-pins.sh
@@ -0,0 +1,13 @@
+#!/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
diff --git a/iris b/iris
deleted file mode 160000
index 243fdd13..00000000
--- a/iris
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 243fdd139ccdf1370e5b186650e4323d5e73e54b
diff --git a/opam b/opam
index 57ec4af8..7718aea8 100644
--- a/opam
+++ b/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"
]
diff --git a/opam.pins b/opam.pins
new file mode 100644
index 00000000..e8f36d38
--- /dev/null
+++ b/opam.pins
@@ -0,0 +1 @@
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#243fdd139ccdf1370e5b186650e4323d5e73e54b
--
GitLab