From cbf35dd56d432b407d589595ab109ac2e22c83d6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 14 Dec 2016 09:37:20 +0100
Subject: [PATCH] use opam-based CI
---
.gitignore | 1 +
.gitlab-ci.yml | 98 +++++++-----------------------------------
.gitmodules | 3 --
coq/build/opam-ci.sh | 34 +++++++++++++++
coq/build/opam-pins.sh | 17 ++++++++
coq/iris | 1 -
coq/ra/Makefile | 47 ++++++++++++++++----
coq/ra/_CoqProject | 1 -
opam | 17 ++++++++
opam.pins | 1 +
10 files changed, 123 insertions(+), 97 deletions(-)
delete mode 100644 .gitmodules
create mode 100755 coq/build/opam-ci.sh
create mode 100755 coq/build/opam-pins.sh
delete mode 160000 coq/iris
create mode 100644 opam
create mode 100644 opam.pins
diff --git a/.gitignore b/.gitignore
index 3321a46b..0240dcae 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,3 +17,4 @@
auto
*.fmt
coq/*/Makefile.coq
+*~
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a2721c10..a9d10061 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,89 +1,21 @@
-image: coq:8.5
+image: ralfjung/opam-ci:latest
-stages:
- - depsquick
- - depsfull
- - quickbuild
- - quickcheck
- - fullbuild
-
-iris-quick:
- stage: depsquick
- tags:
- - coq
- script: >
- (git --version || (apt-get update && apt-get install -y git));
- git submodule update --init --recursive;
- cd coq/iris;
- cat _CoqProject | grep -v '^test' > _CoqProject_filtered;
- mv _CoqProject_filtered _CoqProject;
- make -j8 quick;
- git checkout _CoqProject
- only:
- - master
-
-iris-full:
- stage: depsfull
- tags:
- - coq
- script: >
- (git --version || (apt-get update && apt-get install -y git));
- git submodule update --init --recursive;
- cd coq/iris;
- cat _CoqProject | grep -v '^test' > _CoqProject_filtered;
- mv _CoqProject_filtered _CoqProject;
- make -j8;
- git checkout _CoqProject
- only:
- - master
-
-# vio:
-# stage: quickbuild
-# tags:
-# - coq
-# script: >
-# cd coq/ra/;
-# coqc -v;
-# time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt;
-# cat build-log-vio.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt
-# only:
-# - master
-# cache:
-# paths:
-# - coq/ra/*.vio
-# artifacts:
-# paths:
-# - coq/ra/build-time-vio.txt
-
-# vio2vo:
-# stage: quickcheck
-# tags:
-# - coq
-# script: >
-# cd coq/ra/;
-# coqc -v;
-# time make -j8 TIMED=y vio2vo J=8 2>&1 | tee build-log-vio2vo.txt;
-# cat build-log-vio2vo.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio2vo.txt
-# only:
-# - master
-# allow_failure: true
-# artifacts:
-# paths:
-# - coq/ra/build-time-vio2vo.txt
-
-full:
- stage: fullbuild
- tags:
- - coq
- script: >
- cd coq/ra/;
- coqc -v;
- make clean;
- time make -j8 TIMED=y 2>&1 | tee build-log-full.txt;
- fgrep Axiom build-log-full.txt && exit 1;
- cat build-log-full.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-full.txt;
+gps-coq8.5.3:
+ script:
+ # prepare
+ - cd coq
+ - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
+ # build (the script above switched us to the right directory)
+ - 'time make -j8 TIMED=y 2>&1 | tee build-log-full.txt'
+ - 'if fgrep Axiom build-log-full.txt >/dev/null; then exit 1; fi'
+ - 'cat build-log-full.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-full.txt'
+ cache:
+ key: "coq8.5.3"
+ paths:
+ - coq/opamroot/
only:
- master
+ - opam-ci
artifacts:
paths:
- coq/ra/build-time-full.txt
diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 0f782ad0..00000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "coq/iris"]
- path = coq/iris
- url = https://gitlab.mpi-sws.org/FP/iris-coq.git
diff --git a/coq/build/opam-ci.sh b/coq/build/opam-ci.sh
new file mode 100755
index 00000000..d29ed6e5
--- /dev/null
+++ b/coq/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 --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
+cd ra
+make build-dep Y=1
+
+# done
+echo
+coqc -v
diff --git a/coq/build/opam-pins.sh b/coq/build/opam-pins.sh
new file mode 100755
index 00000000..aebd23ca
--- /dev/null
+++ b/coq/build/opam-pins.sh
@@ -0,0 +1,17 @@
+#!/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
diff --git a/coq/iris b/coq/iris
deleted file mode 160000
index 6e00aa34..00000000
--- a/coq/iris
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2
diff --git a/coq/ra/Makefile b/coq/ra/Makefile
index ff1ccd39..f26c5ef7 100644
--- a/coq/ra/Makefile
+++ b/coq/ra/Makefile
@@ -1,22 +1,51 @@
-# Makefile originally taken from coq-club
+# 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 $@
+ +@make -f Makefile.coq $@
all: Makefile.coq
- +make -f Makefile.coq all
+ +@make -f Makefile.coq all
clean: Makefile.coq
- +make -f Makefile.coq clean
+ +@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
-
-_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-gps "$$(pwd)/../..#HEAD" -k git -n -y
+ opam install coq-gps --deps-only $(YFLAG)
+ opam pin remove coq-gps
+
+# 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
diff --git a/coq/ra/_CoqProject b/coq/ra/_CoqProject
index 946ef7b8..0c87d9c3 100644
--- a/coq/ra/_CoqProject
+++ b/coq/ra/_CoqProject
@@ -1,5 +1,4 @@
-R . ra
--Q ../iris iris
./infrastructure.v
./types.v
./views.v
diff --git a/opam b/opam
new file mode 100644
index 00000000..69ed1f36
--- /dev/null
+++ b/opam
@@ -0,0 +1,17 @@
+opam-version: "1.2"
+name: "coq-gps"
+version: "dev"
+maintainer: "Jan-Oliver Kaiser, Hoang-Hai Dang"
+authors: "Jan-Oliver Kaiser, Hoang-Hai Dang"
+# homepage: "?"
+bug-reports: "https://gitlab.mpi-sws.org/FP/sra-gps/issues"
+dev-repo: "https://gitlab.mpi-sws.org/FP/sra-gps.git"
+build: [
+ [make "-j%{jobs}%"]
+]
+install: [make "install"]
+# TODO: probably we want to install things to a different folder, "ra" is rather undescriptive
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/ra" ]
+depends: [
+ "coq-iris"
+]
diff --git a/opam.pins b/opam.pins
new file mode 100644
index 00000000..9625cdc6
--- /dev/null
+++ b/opam.pins
@@ -0,0 +1 @@
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2
--
GitLab