Commit 63f64743 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers

add opam and CI stuff (with preliminary names)

parent c82f6e43
image: ralfjung/opam-ci:latest
stdpp-coq8.6:
tags:
- coq
script:
# prepare
- . build/opam-ci.sh coq 8.6
# build
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- 'make validate'
cache:
key: "coq8.6"
paths:
- opamroot/
only:
- master
- ci
- timing
......@@ -3,13 +3,8 @@ 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,-several-object-files
endif
# Configure Coq warnings
COQ_MAKEFILE_FLAGS ?= -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
......@@ -32,9 +27,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
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-prelude "$$(pwd)#HEAD" -k git -n -y
opam install coq-prelude --deps-only $(YFLAG)
opam pin remove coq-prelude
opam pin add coq-stdpp "$$(pwd)#HEAD" -k git -n -y
opam install coq-stdpp --deps-only $(YFLAG)
opam pin remove coq-stdpp
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
#!/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
# Install fixed versions of some dependencies
echo
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
VERSION="$1" ; shift
# Check if the pin is already set
if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
echo "[opam-ci] $PACKAGE already pinned to $VERSION"
else
echo "[opam-ci] Pinning $PACKAGE to $VERSION"
opam pin add "$PACKAGE" "$VERSION" -k version -y
fi
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
if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
echo "[opam-pins] $PACKAGE already at commit $HASH"
else
echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
fi
echo
done
opam-version: "1.2"
name: "coq-stdpp"
version: "dev"
maintainer: "Robbert Krebbers"
authors: "Robbert Krebbers"
bug-reports: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues"
license: "BSD"
dev-repo: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git"
build: [
[make "-j%{jobs}%"]
]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/coq-stdpp'" ]
depends: [
"coq" { ((>= "8.6" & < "8.7~") | (= "dev"))}
]
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