Commit 99470279 authored by Ralf Jung's avatar Ralf Jung

use OPAM-based CI

parent 5b128305
Pipeline #3303 failed with stage
in 17 minutes and 7 seconds
image: coq:8.5 image: ralfjung/opam-ci:latest
buildjob: iris-coq8.5.3:
tags: tags:
- coq - coq
script: script:
- coqc -v # prepare
- . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
# build
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt' - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'fgrep Axiom build-log.txt && exit 1' - 'fgrep Axiom build-log.txt && exit 1'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt' - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- make validate #- make validate
cache:
key: "coq8.5.3"
paths:
- opamroot/
only: only:
- master - master
- ci
- timing - timing
artifacts: artifacts:
paths: paths:
- build-time.txt - build-time.txt
iris-coq8.6beta:
tags:
- coq
script:
# prepare
- . build/opam-ci.sh 'coq 8.6.dev 'coq-mathcomp-ssreflect dev'
# build
- 'time make -j8'
cache:
key: "coq8.6"
paths:
- opamroot/
only:
- master
- ci
- timing
# Process flags
ifeq ($(Y), 1)
YFLAG=-y
endif
# Determine Coq version # Determine Coq version
COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]') COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
COQ_MAKEFILE_FLAGS ?= COQ_MAKEFILE_FLAGS ?=
...@@ -6,6 +11,7 @@ ifeq ($(COQ_VERSION), 8.6) ...@@ -6,6 +11,7 @@ ifeq ($(COQ_VERSION), 8.6)
COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection
endif endif
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony %: Makefile.coq phony
+@make -f Makefile.coq $@ +@make -f Makefile.coq $@
...@@ -17,18 +23,29 @@ clean: Makefile.coq ...@@ -17,18 +23,29 @@ clean: Makefile.coq
find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete 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 rm -f Makefile.coq
# Create Coq Makefile
Makefile.coq: _CoqProject Makefile Makefile.coq: _CoqProject Makefile
@# we want to pass the correct name to coq_makefile or it will be confused @# 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 coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp 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 \ 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 | 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 rm Makefile.coq.tmp
_CoqProject: ; # 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 "$$(pwd)#HEAD" -k git -n -y
opam install coq-iris --deps-only $(YFLAG)
opam pin remove coq-iris
# some fiels that do *not* need to be forwarded to Makefile.coq
Makefile: ; Makefile: ;
_CoqProject: ;
# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
phony: ; phony: ;
.PHONY: all clean phony .PHONY: all clean phony
#!/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
#!/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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment