Skip to content
Snippets Groups Projects
Commit 7321b9c0 authored by Ralf Jung's avatar Ralf Jung
Browse files

update and enable CI

parent e46cc7f7
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
+ 31
− 15
View file @ 7321b9c0
image: ralfjung/opam-ci:latest image: ralfjung/opam-ci:latest
stages:
- build
variables: variables:
CPU_CORES: "9" CPU_CORES: "10"
.template: &template .template: &template
stage: build
tags: tags:
- fp-timing - fp
script: script:
# prepare # prepare
- . build/opam-ci.sh coq "$COQ_VERSION" coq-mathcomp-ssreflect "$SSR_VERSION" - . build/opam-ci.sh $OPAM_PINS
- env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt - env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build # build
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt' - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi' - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt' - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
- 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi' # maybe validate
- 'if [[ -n "$VALIDATE" ]]; then make validate; fi'
cache: cache:
key: "coq.$COQ_VERSION-ssr.$SSR_VERSION" key: "$CI_JOB_NAME"
paths: paths:
- opamroot/ - opamroot/
only: only:
- master - gen_proofmode_WIP
- /^ci/ - /^ci/
except:
- triggers
build-coq8.7: ## Build jobs
<<: *template
variables:
COQ_VERSION: "8.7.dev"
SSR_VERSION: "dev"
build-coq8.6.1: build-coq.8.7.1:
<<: *template <<: *template
variables: variables:
COQ_VERSION: "8.6.1" OPAM_PINS: "coq version 8.7.1 coq-mathcomp-ssreflect version 1.6.4"
SSR_VERSION: "1.6.1" tags:
VALIDATE: "1" - fp-timing
artifacts: artifacts:
paths: paths:
- build-time.txt - build-time.txt
- build-env.txt - build-env.txt
build-coq.8.6.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.4"
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1 coq-mathcomp-ssreflect version 1.6.4 coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
except:
only:
- triggers
Makefile
+ 7
− 6
View file @ 7321b9c0
...@@ -15,12 +15,12 @@ clean: Makefile.coq ...@@ -15,12 +15,12 @@ clean: Makefile.coq
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real # Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics. # filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq "$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies # Install build-dependencies
build-dep/opam: opam Makefile build-dep/opam: opam Makefile
# Create the build-dep package. # Creating the build-dep package.
@mkdir -p build-dep @mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam @sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check @fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
...@@ -31,11 +31,12 @@ build-dep: build-dep/opam phony ...@@ -31,11 +31,12 @@ build-dep: build-dep/opam phony
@# that are incompatible with our build requirements. @# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as @# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything. @# dependencies, but does not actually install anything.
# Add the pin and (re)install build-dep package. @# Upgrading is needed in case the pin already exists, but the builddep package changed.
@# Reinstallation is needed in case the pin already exists, but the builddep package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \ @BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
opam pin add "$$BUILD_DEP_PACKAGE".dev "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \ echo "# Pinning build-dep package." && \
opam reinstall "$$BUILD_DEP_PACKAGE" opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
echo "# Updating build-dep package." && \
opam upgrade "$$BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq # Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ; Makefile: ;
......
build/opam-ci.sh
+ 25
− 24
View file @ 7321b9c0
#!/bin/bash #!/bin/bash
set -e set -e
set -x
## This script installs the build dependencies for CI builds. ## This script installs the build dependencies for CI builds.
function run_and_print() {
echo "$ $@"
"$@"
}
# Prepare OPAM configuration # Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot" export OPAMROOT="$(pwd)/opamroot"
...@@ -12,26 +9,27 @@ export OPAMJOBS="$((2*$CPU_CORES))" ...@@ -12,26 +9,27 @@ export OPAMJOBS="$((2*$CPU_CORES))"
export OPAM_EDITOR="$(which false)" export OPAM_EDITOR="$(which false)"
# Make sure we got a good OPAM. # Make sure we got a good OPAM.
test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y) test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
eval `opam conf env` eval `opam conf env`
# Delete old pins from opam.pins times.
run_and_print opam pin remove coq-stdpp -n
run_and_print opam pin remove coq-iris -n
# Make sure the pin for the builddep package is not stale. # Make sure the pin for the builddep package is not stale.
run_and_print make build-dep/opam make build-dep/opam
# Update repositories
opam update
# Get us all the latest repositories # Make sure we got the right set of repositories registered
if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then if echo "$@" | fgrep "dev" > /dev/null; then
# last update was more than a day ago # We are compiling against a dev version of something. Get ourselves the dev repositories.
run_and_print opam update test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
else else
# only update iris-dev # No dev version, make sure we do not have the dev repositories.
if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi test -d "$OPAMROOT/repo/coq-extra-dev" && opam repo remove coq-extra-dev
test -d "$OPAMROOT/repo/coq-core-dev" && opam repo remove coq-core-dev
fi fi
test -d "$OPAMROOT/repo/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5 test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
echo echo
# We really want to run all of the following in one opam transaction, but due to opam limitations, # We really want to run all of the following in one opam transaction, but due to opam limitations,
...@@ -41,21 +39,23 @@ echo ...@@ -41,21 +39,23 @@ echo
echo echo
while (( "$#" )); do # while there are arguments left while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift PACKAGE="$1" ; shift
KIND="$1" ; shift
VERSION="$1" ; shift VERSION="$1" ; shift
# Check if the pin is already set # Check if the pin is already set
if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]"))
echo "[opam-ci] $PACKAGE already pinned to $VERSION" if [[ "${PIN[1]}" == "$KIND" && "${PIN[2]}" == "$VERSION" ]]; then
echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION"
else else
echo "[opam-ci] Pinning $PACKAGE to $VERSION" echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION"
run_and_print opam pin add "$PACKAGE" "$VERSION" -k version -y opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
fi fi
done done
# Upgrade cached things. # Upgrade cached things.
echo echo
echo "[opam-ci] Upgrading opam" echo "[opam-ci] Upgrading opam"
run_and_print opam upgrade -y opam upgrade -y --fixup && opam upgrade -y
# Install build-dependencies. # Install build-dependencies.
echo echo
...@@ -63,5 +63,6 @@ echo "[opam-ci] Installing build-dependencies" ...@@ -63,5 +63,6 @@ echo "[opam-ci] Installing build-dependencies"
make build-dep OPAMFLAGS=-y make build-dep OPAMFLAGS=-y
# done # done
set +x
echo echo
coqc -v coqc -v
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