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

use new CI machine

parent 0671cb48
No related branches found
No related tags found
No related merge requests found
Pipeline #
image: ralfjung/opam-ci:latest
variables:
CPU_CORES: "9"
stdpp-coq8.5:
tags:
- coq
- fp-timing
script:
# prepare
- . build/opam-ci.sh coq 8.5.3
# build
- 'time make -j8'
- 'time make -j$CPU_CORES'
cache:
key: "coq8.5"
paths:
......@@ -19,12 +22,13 @@ stdpp-coq8.5:
stdpp-coq8.6:
tags:
- coq
- fp-timing
script:
# prepare
- . build/opam-ci.sh coq 8.6
- env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'time make -j$CPU_CORES 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'
- 'if (( RANDOM % 10 == 0 )); then make validate; fi'
......@@ -39,3 +43,4 @@ stdpp-coq8.6:
artifacts:
paths:
- build-time.txt
- build-env.txt
......@@ -4,16 +4,21 @@ set -e
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS=16
export OPAMJOBS="$((2*$CPU_CORES))"
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`
if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
# last update was more than a day ago
opam update
else
echo "[opam-ci] Not updating opam."
fi
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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment