diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 23a0de02cc717953c8b27edfb8c93575ff7b2cf0..78000ee0daa608bc2090904e29424a66b00900b9 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -5,23 +5,14 @@ stages: variables: CPU_CORES: "10" + GIT_SUBMODULE_STRATEGY: "recursive" .template: &template stage: build tags: - fp script: - # prepare - - . build/opam-ci.sh $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' - - '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' - # maybe validate - - 'if [[ -n "$VALIDATE" ]]; then make validate; fi' - # maybe create opam package - - 'if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == gen_proofmode ]]; then curl --fail -X POST -F "token=$OPAM_UPDATE_SECRET" -F "ref=master" -F "variables[REPO]=$CI_PROJECT_URL.git" -F "variables[REF]=$CI_COMMIT_REF_NAME" -F "variables[SHA]=$CI_COMMIT_SHA" -F "variables[NAME]=$OPAM_PKG" -F "variables[OPAM_PREFIX]=branch.gen_proofmode" https://gitlab.mpi-sws.org/api/v4/projects/581/trigger/pipeline; fi' + - ci/buildjob cache: key: "$CI_JOB_NAME" paths: @@ -52,12 +43,11 @@ build-coq.8.7.2: variables: OPAM_PINS: "coq version 8.7.2" OPAM_PKG: "coq-iris" + OPAM_PKG_BRANCH: "gen_proofmode" + TIMING_PROJECT: "iris" + TIMING_CONF: "coq-8.7.2" tags: - fp-timing - artifacts: - paths: - - build-time.txt - - build-env.txt build-coq.8.7.1: <<: *template 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..b58c3b6db3087e19b01e54ec640b465e7262935e --- /dev/null +++ b/ci @@ -0,0 +1 @@ +Subproject commit b58c3b6db3087e19b01e54ec640b465e7262935e