diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5d814ea3b9691bd5e8708eefac72a0e4dd1ba6ae..e8564be163f796cbecaf6c3f4267985002102aab 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -12,7 +12,7 @@ variables: - fp script: # prepare - - . build/opam-ci.sh $OPAM_PINS + - . ci/prepare-opam $OPAM_PINS - env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt # build - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt' diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000000000000000000000000000000000000..53648fdc2581a4d79760bf124d570b7692157ba8 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "ci"] + path = ci + url = https://gitlab.mpi-sws.org/FP/iris-ci.git diff --git a/build/opam-ci.sh b/build/opam-ci.sh deleted file mode 100755 index bc51df87ef1e4c3867512df9f8b309111109a151..0000000000000000000000000000000000000000 --- a/build/opam-ci.sh +++ /dev/null @@ -1,68 +0,0 @@ -#!/bin/bash -set -e -set -x -## This script installs the build dependencies for CI builds. - -# Prepare OPAM configuration -export OPAMROOT="$(pwd)/opamroot" -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` - -# Make sure the pin for the builddep package is not stale. -make build-dep/opam - -# Update repositories -opam update - -# Make sure we got the right set of repositories registered -if echo "$@" | fgrep "dev" > /dev/null; then - # We are compiling against a dev version of something. Get ourselves the dev repositories. - 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 - # No dev version, make sure we do not have the dev repositories. - 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 -test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10 -test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20 -echo - -# We really want to run all of the following in one opam transaction, but due to opam limitations, -# that is not currently possible. - -# Install fixed versions of some dependencies. -echo -while (( "$#" )); do # while there are arguments left - PACKAGE="$1" ; shift - KIND="$1" ; shift - VERSION="$1" ; shift - - # Check if the pin is already set - read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]")) - if [[ "${PIN[1]}" == "$KIND" && "${PIN[2]}" == "$VERSION" ]]; then - echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION" - else - echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION" - opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION" - fi -done - -# Upgrade cached things. -echo -echo "[opam-ci] Upgrading opam" -opam upgrade -y --fixup && opam upgrade -y - -# Install build-dependencies. -echo -echo "[opam-ci] Installing build-dependencies" -make build-dep OPAMFLAGS=-y - -# done -set +x -echo -coqc -v diff --git a/ci b/ci new file mode 160000 index 0000000000000000000000000000000000000000..799685e2c96af0e3c0a39e4584633affe55df051 --- /dev/null +++ b/ci @@ -0,0 +1 @@ +Subproject commit 799685e2c96af0e3c0a39e4584633affe55df051