diff options
Diffstat (limited to 'dev/ci')
43 files changed, 264 insertions, 281 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index a814e4914e..95892ebe0a 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -136,12 +136,38 @@ rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci` and `make install` is run, then the `_install_ci` directory persists to and is used by the next jobs. -Artifacts can also be downloaded from the GitLab repository. -Currently, available artifacts are: +### Artifacts + +Build artifacts from GitLab can be linked / downloaded in a systematic +way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts) +for more information. For example, to access the documentation of the +`master` branch, you can do: + +https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + +Browsing artifacts is also possible: +https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + +Above, you can replace `master` and `job` by the desired GitLab branch and job name. + +Currently available artifacts are: + - the Coq executables and stdlib, in four copies varying in - architecture and OCaml version used to build Coq. -- the Coq documentation, built in the `documentation` job. When submitting - a documentation PR, this can help reviewers checking the rendered result. + architecture and OCaml version used to build Coq: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + + Additionally, an experimental Dune build is provided: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune + +- the Coq documentation, built in the `doc:*` jobs. When submitting + a documentation PR, this can help reviewers checking the rendered result: + + + Coq's Reference Manual [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + + Coq's Standard Library Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman + + Coq's ML API Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api ### GitLab and Windows @@ -168,6 +194,6 @@ but if you wish to save more time you can skip the job by setting This means you will need to change its value when the Docker image needs to be updated. You can do so for a single pipeline by starting -it through the web interface.. +it through the web interface. See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 28321d13e2..63d5541f48 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -9,124 +9,147 @@ ######################################################################## # MathComp ######################################################################## -: "${mathcomp_CI_BRANCH:=master}" +: "${mathcomp_CI_REF:=master}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" -: "${oddorder_CI_BRANCH:=master}" +: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" + +: "${oddorder_CI_REF:=master}" : "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" +: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}" ######################################################################## # UniMath ######################################################################## -: "${UniMath_CI_BRANCH:=master}" +: "${UniMath_CI_REF:=master}" : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" +: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}" ######################################################################## # Unicoq + Mtac2 ######################################################################## -: "${unicoq_CI_BRANCH:=master}" +: "${unicoq_CI_REF:=master}" : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" +: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" -: "${mtac2_CI_BRANCH:=master-sync}" +: "${mtac2_CI_REF:=master-sync}" : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" +: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" ######################################################################## # Mathclasses + Corn ######################################################################## -: "${math_classes_CI_BRANCH:=master}" -: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes}" +: "${math_classes_CI_REF:=master}" +: "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" +: "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" -: "${Corn_CI_BRANCH:=master}" -: "${Corn_CI_GITURL:=https://github.com/c-corn/corn}" +: "${Corn_CI_REF:=master}" +: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}" +: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}" ######################################################################## # Iris ######################################################################## -: "${stdpp_CI_BRANCH:=master}" +: "${stdpp_CI_REF:=master}" : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" +: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_BRANCH:=master}" +: "${Iris_CI_REF:=master}" : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" +: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" -: "${lambdaRust_CI_BRANCH:=master}" +: "${lambdaRust_CI_REF:=master}" : "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" +: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" ######################################################################## # HoTT ######################################################################## -: "${HoTT_CI_BRANCH:=master}" +: "${HoTT_CI_REF:=master}" : "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" +: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" ######################################################################## # Ltac2 ######################################################################## -: "${ltac2_CI_BRANCH:=master}" +: "${ltac2_CI_REF:=master}" : "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}" +: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}" ######################################################################## # GeoCoq ######################################################################## -: "${GeoCoq_CI_BRANCH:=master}" +: "${GeoCoq_CI_REF:=master}" : "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" +: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}" ######################################################################## # Flocq ######################################################################## -: "${Flocq_CI_BRANCH:=master}" +: "${Flocq_CI_REF:=master}" : "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" +: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}" ######################################################################## # Coquelicot ######################################################################## -: "${Coquelicot_CI_BRANCH:=master}" +: "${Coquelicot_CI_REF:=master}" : "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_BRANCH:=master}" +: "${CompCert_CI_REF:=master}" : "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" +: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -: "${VST_CI_BRANCH:=master}" +: "${VST_CI_REF:=master}" : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" ######################################################################## # cross-crypto ######################################################################## -: "${cross_crypto_CI_BRANCH:=master}" +: "${cross_crypto_CI_REF:=master}" : "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" +: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" ######################################################################## # fiat_parsers ######################################################################## -: "${fiat_parsers_CI_BRANCH:=master}" +: "${fiat_parsers_CI_REF:=master}" : "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}" +: "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}" ######################################################################## # fiat_crypto ######################################################################## -: "${fiat_crypto_CI_BRANCH:=master}" +: "${fiat_crypto_CI_REF:=master}" : "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## # formal-topology ######################################################################## -: "${formal_topology_CI_BRANCH:=ci}" +: "${formal_topology_CI_REF:=ci}" : "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" +: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## # coq-dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_BRANCH:=coq-master}" +: "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" +: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}" ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_BRANCH:=master}" +: "${CoLoR_CI_REF:=master}" : "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" +: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" ######################################################################## # SF @@ -138,53 +161,68 @@ ######################################################################## # TLC ######################################################################## -: "${tlc_CI_BRANCH:=master}" +: "${tlc_CI_REF:=master}" : "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}" ######################################################################## # Bignums ######################################################################## -: "${bignums_CI_BRANCH:=master}" +: "${bignums_CI_REF:=master}" : "${bignums_CI_GITURL:=https://github.com/coq/bignums}" +: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_BRANCH:=master}" +: "${bedrock2_CI_REF:=master}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" +: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" ######################################################################## # Equations ######################################################################## -: "${Equations_CI_BRANCH:=master}" +: "${Equations_CI_REF:=master}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" +: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_BRANCH:=coq-master}" +: "${Elpi_CI_REF:=coq-master}" : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm ######################################################################## -: "${fcsl_pcm_CI_BRANCH:=master}" +: "${fcsl_pcm_CI_REF:=master}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" +: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## # pidetop ######################################################################## -: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_REF:=v8.9}" : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" +: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" ######################################################################## # ext-lib ######################################################################## -: "${ext_lib_CI_BRANCH:=master}" +: "${ext_lib_CI_REF:=master}" : "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}" +: "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" + +######################################################################## +# simple-io +######################################################################## +: "${simple_io_CI_REF:=master}" +: "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" +: "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" ######################################################################## # quickchick ######################################################################## -: "${quickchick_CI_BRANCH:=master}" +: "${quickchick_CI_REF:=master}" : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" +: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 447076e092..5205946261 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -3,9 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -bedrock2_CI_DIR="${CI_BUILD_DIR}/bedrock2" +FORCE_GIT=1 +git_download bedrock2 -git_checkout "${bedrock2_CI_BRANCH}" "${bedrock2_CI_GITURL}" "${bedrock2_CI_DIR}" -( cd "${bedrock2_CI_DIR}" && git submodule update --init --recursive ) - -( cd "${bedrock2_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index 0082919679..756f54dfbd 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -1,16 +1,8 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" -# This script could be included inside other ones -# Let's avoid to source ci-common twice in this case -if [ -z "${CI_BUILD_DIR}" ]; -then - . "${ci_dir}/ci-common.sh" -fi +git_download bignums -bignums_CI_DIR="${CI_BUILD_DIR}/Bignums" - -git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}" - -( cd "${bignums_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/bignums" && make && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 8ce5f2418f..dc696f69d9 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CoLoR_CI_DIR=${CI_BUILD_DIR}/color +git_download CoLoR -# Compile CoLoR -git_checkout "${CoLoR_CI_BRANCH}" "${CoLoR_CI_GITURL}" "${CoLoR_CI_DIR}" -( cd "${CoLoR_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/CoLoR" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 9259a6e0c8..7af648f0a6 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -34,39 +34,48 @@ export COQBIN="$COQBIN/" ls "$COQBIN" -# Where we clone and build external developments +# Where we download and build external developments CI_BUILD_DIR="$PWD/_build_ci" -# shellcheck source=ci-basic-overlay.sh -. "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" -mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" - -# git_checkout branch url dest will create a git repository -# in <dest> (if it does not exist already) and checkout the -# remote branch <branch> from <url> -git_checkout() +# [git_download project] will download [project] and unpack it +# in [$CI_BUILD_DIR/project] if the folder does not exist already; +# if it does, it will do nothing except print a warning (this can be +# useful when building locally). +# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty +# (local build), it uses git clone to perform the download. +git_download() { - local _BRANCH=${1} - local _URL=${2} - local _DEST=${3} - - # Allow an optional 4th argument for the commit - local _COMMIT=${4:-FETCH_HEAD} - local _DEPTH=() - if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi - - mkdir -p "${_DEST}" - ( cd "${_DEST}" && \ - if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \ - echo "Checking out ${_DEST}" && \ - git fetch "${_URL}" "${_BRANCH}" && \ - git -c advice.detachedHead=false checkout "${_COMMIT}" && \ - echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) + local PROJECT=$1 + local DEST="$CI_BUILD_DIR/$PROJECT" + + if [ -d "$DEST" ]; then + echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." + elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + git clone "$GITURL" "$DEST" + cd "$DEST" + git checkout "$REF" + else # When possible, we download tarballs to reduce bandwidth and latency + local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" + local ARCHIVEURL="${!ARCHIVEURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + mkdir -p "$DEST" + cd "$DEST" + wget "$ARCHIVEURL/$REF.tar.gz" + tar xvfz "$REF.tar.gz" --strip-components=1 + rm -f "$REF.tar.gz" + fi } make() @@ -84,31 +93,27 @@ make() # this installs just the ssreflect library of math-comp install_ssreflect() { - echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + echo 'Installing ssreflect' - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + git_download mathcomp - ( cd "${mathcomp_CI_DIR}/mathcomp" && \ + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ make Makefile.coq && \ make -f Makefile.coq ssreflect/all_ssreflect.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssr.install\\r' - } # this installs just the ssreflect + algebra library of math-comp install_ssralg() { - echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r' + echo 'Installing ssralg' - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + git_download mathcomp - ( cd "${mathcomp_CI_DIR}/mathcomp" && \ + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ make Makefile.coq && \ make -f Makefile.coq algebra/all_algebra.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssralg.install\\r' - } diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 8d490591b6..01c35ceb4a 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" +git_download CompCert -git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}" - -( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +( cd "${CI_BUILD_DIR}/CompCert" && \ + ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index 5d57fce1c7..2373ea6c62 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -coq_dpdgraph_CI_DIR="${CI_BUILD_DIR}/coq-dpdgraph" +git_download coq_dpdgraph -git_checkout "${coq_dpdgraph_CI_BRANCH}" "${coq_dpdgraph_CI_GITURL}" "${coq_dpdgraph_CI_DIR}" - -( cd "${coq_dpdgraph_CI_DIR}" && autoconf && ./configure && make && make test-suite ) +( cd "${CI_BUILD_DIR}/coq_dpdgraph" && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index d86d61ef6a..5d8817491d 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -3,10 +3,9 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Coquelicot_CI_DIR="${CI_BUILD_DIR}/coquelicot" - install_ssreflect -git_checkout "${Coquelicot_CI_BRANCH}" "${Coquelicot_CI_GITURL}" "${Coquelicot_CI_DIR}" +FORCE_GIT=1 +git_download Coquelicot -( cd "${Coquelicot_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 9298fc70af..7d5d70cf90 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Corn_CI_DIR="${CI_BUILD_DIR}/corn" +git_download Corn -git_checkout "${Corn_CI_BRANCH}" "${Corn_CI_GITURL}" "${Corn_CI_DIR}" - -( cd "${Corn_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/Corn" && make && make install ) diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh index a0d3aa6551..900d12c1dd 100755 --- a/dev/ci/ci-cross-crypto.sh +++ b/dev/ci/ci-cross-crypto.sh @@ -3,9 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto" +FORCE_GIT=1 +git_download cross_crypto -git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}" -( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive ) - -( cd "${cross_crypto_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/cross_crypto" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index 9c58034be1..9b4a06fd5b 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Elpi_CI_DIR="${CI_BUILD_DIR}/elpi" +git_download Elpi -git_checkout "${Elpi_CI_BRANCH}" "${Elpi_CI_GITURL}" "${Elpi_CI_DIR}" - -( cd "${Elpi_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/Elpi" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 98735b4ec4..998d50faa7 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Equations_CI_DIR="${CI_BUILD_DIR}/Equations" +git_download Equations -git_checkout "${Equations_CI_BRANCH}" "${Equations_CI_GITURL}" "${Equations_CI_DIR}" - -( cd "${Equations_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install) +( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ + make && make test-suite && make examples && make install) diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh index cf212c2fb5..5eb167d97d 100755 --- a/dev/ci/ci-ext-lib.sh +++ b/dev/ci/ci-ext-lib.sh @@ -1,16 +1,8 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" -# This script could be included inside other ones -# Let's avoid to source ci-common twice in this case -if [ -z "${CI_BUILD_DIR}" ]; -then - . "${ci_dir}/ci-common.sh" -fi +git_download ext_lib -ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib" - -git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}" - -( cd "${ext_lib_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/ext_lib" && make && make install) diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh index fdc4c729b6..cb951630c8 100755 --- a/dev/ci/ci-fcsl-pcm.sh +++ b/dev/ci/ci-fcsl-pcm.sh @@ -3,10 +3,8 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fcsl_pcm_CI_DIR="${CI_BUILD_DIR}/fcsl-pcm" - install_ssreflect -git_checkout "${fcsl_pcm_CI_BRANCH}" "${fcsl_pcm_CI_GITURL}" "${fcsl_pcm_CI_DIR}" +git_download fcsl_pcm -( cd "${fcsl_pcm_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/fcsl_pcm" && make ) diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 9429344159..e0395754e5 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -3,12 +3,11 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" - -git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" - -( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) +FORCE_GIT=1 +git_download fiat_crypto fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) + +( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ + make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 659511dbea..7e8013be9b 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -3,10 +3,12 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" +FORCE_GIT=1 +git_download fiat_crypto -git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" +# We need a larger stack size to not overflow ocamlopt+flambda when +# building the executables. +# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 -( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) - -( cd "${fiat_crypto_CI_DIR}" && make new-pipeline ) +( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ + ulimit -s 32768 && make new-pipeline c-files ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 35c2284050..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fiat_parsers_CI_DIR="${CI_BUILD_DIR}/fiat" +FORCE_GIT=1 +git_download fiat_parsers -git_checkout "${fiat_parsers_CI_BRANCH}" "${fiat_parsers_CI_GITURL}" "${fiat_parsers_CI_DIR}" - -( cd "${fiat_parsers_CI_DIR}" && make parsers parsers-examples && make fiat-core ) +( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 8599e4d50e..e87483df0a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Flocq_CI_DIR="${CI_BUILD_DIR}/flocq" +git_download Flocq -git_checkout "${Flocq_CI_BRANCH}" "${Flocq_CI_GITURL}" "${Flocq_CI_DIR}" - -( cd "${Flocq_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 118d151500..8be5a06ed2 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -formal_topology_CI_DIR="${CI_BUILD_DIR}/formal-topology" +git_download formal_topology -git_checkout "${formal_topology_CI_BRANCH}" "${formal_topology_CI_GITURL}" "${formal_topology_CI_DIR}" - -( cd "${formal_topology_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 24cd9c4272..8c57318477 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,10 +3,8 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq" - -git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}" - install_ssralg -( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make ) +git_download GeoCoq + +( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 184b90a50b..7eeeb09372 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT +git_download HoTT -git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}" - -( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 1af0f634c4..6960a8b98a 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -3,32 +3,28 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -stdpp_CI_DIR="${CI_BUILD_DIR}/coq-stdpp" -Iris_CI_DIR="${CI_BUILD_DIR}/iris-coq" -lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust" - install_ssreflect # Setup lambdaRust first -git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}" +git_download lambdaRust # Extract required version of Iris -Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris -git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}" +git_download Iris # Extract required version of std++ -stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ -git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}" +git_download stdpp # Build std++ -( cd "${stdpp_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) -# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris -( cd "${Iris_CI_DIR}" && make && (test -n "${TRAVIS}" || make validate) && make install ) +# Build and validate Iris +( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install ) # Build lambdaRust -( cd "${lambdaRust_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 5981aaaae7..4df22bf249 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -ltac2_CI_DIR="${CI_BUILD_DIR}/ltac2" +git_download ltac2 -git_checkout "${ltac2_CI_BRANCH}" "${ltac2_CI_GITURL}" "${ltac2_CI_DIR}" - -( cd "${ltac2_CI_DIR}" && make && make tests && make install ) +( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 6a064b2971..ae31a8e7f8 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes" +git_download math_classes -git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}" - -( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install ) +( cd "${CI_BUILD_DIR}/math_classes" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 20328baf2a..a74f9fa4d3 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,11 +4,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" -oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order" +git_download mathcomp -git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" -git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}" +( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install ) -( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install ) -( cd "${oddorder_CI_DIR}/" && make ) +git_download oddorder + +( cd "${CI_BUILD_DIR}/oddorder" && make ) diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh index 1372acb8e5..7075d4d7f6 100755 --- a/dev/ci/ci-mtac2.sh +++ b/dev/ci/ci-mtac2.sh @@ -3,17 +3,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq -mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2 +git_download unicoq -# Setup UniCoq +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) -git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" +git_download mtac2 -( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install ) - -# Setup MetaCoq - -git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}" - -( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make ) +( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index 32cba0808e..1a9a26843c 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -1,12 +1,9 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" - -git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" +git_download pidetop # Travis / Gitlab have different filesystem layout due to use of # `-local`. We need to improve this divergence but if we use Dune this @@ -17,6 +14,6 @@ else COQLIB="$COQBIN/../" fi -( cd "${pidetop_CI_DIR}" && jbuilder build @install ) +( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install ) -echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds +echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh index fc39e2685d..08686d7ced 100755 --- a/dev/ci/ci-quickchick.sh +++ b/dev/ci/ci-quickchick.sh @@ -1,18 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" - -# This script could be included inside other ones -# Let's avoid to source ci-common twice in this case -if [ -z "${CI_BUILD_DIR}" ]; -then - . "${ci_dir}/ci-common.sh" -fi - -quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick" +. "${ci_dir}/ci-common.sh" install_ssreflect -git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}" +git_download quickchick -( cd "${quickchick_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/quickchick" && make && make install) diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple-io.sh new file mode 100755 index 0000000000..e7bcd80de7 --- /dev/null +++ b/dev/ci/ci-simple-io.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download simple_io + +( cd "${CI_BUILD_DIR}/simple_io" && make build && make install) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh deleted file mode 100755 index e77a553047..0000000000 --- a/dev/ci/ci-template.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -Template_CI_BRANCH=master -Template_CI_GITURL=https://github.com/Template/Template -Template_CI_DIR="${CI_BUILD_DIR}/Template" - -git_checkout "${Template_CI_BRANCH}" "${Template_CI_GITURL}" "${Template_CI_DIR}" - -( cd "${Template_CI_DIR}" && make ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 31387c8ddc..a2f0bea555 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -tlc_CI_DIR="${CI_BUILD_DIR}/tlc" +FORCE_GIT=1 +git_download tlc -git_checkout "${tlc_CI_BRANCH}" "${tlc_CI_GITURL}" "${tlc_CI_DIR}" - -( cd "${tlc_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/tlc" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index aa20fe1ff0..a7644fee23 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" +git_download UniMath -git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" - -( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) +( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 7a097eaab4..0fec19205a 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -VST_CI_DIR="${CI_BUILD_DIR}/VST" +git_download VST -git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" - -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true ) +( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 1361392dc8..7a649591dd 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-07-11-V2" +# CACHEKEY: "bionic_coq-V2018-08-27-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -28,8 +28,8 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml. # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.0.0 ounit.2.0.8" \ - CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8" +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.1.1 ounit.2.0.8" \ + CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV CAMLP5_VER="6.14" \ diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index e6a2c4460b..d812df3ec0 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,6 +1,6 @@ #!/bin/sh if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh new file mode 100644 index 0000000000..575df07425 --- /dev/null +++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=pure-sharing-flag + +if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh deleted file mode 100644 index 27f588e214..0000000000 --- a/dev/ci/user-overlays/07859-printers.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then - Equations_CI_BRANCH=fix-printers - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations -fi diff --git a/dev/ci/user-overlays/07908-proj-mind.sh b/dev/ci/user-overlays/07908-proj-mind.sh deleted file mode 100644 index 293eeb5a5a..0000000000 --- a/dev/ci/user-overlays/07908-proj-mind.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7908" ] || [ "$CI_BRANCH" = "proj-mind" ]; then - Equations_CI_BRANCH=fix-proj-mind - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations -fi diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh deleted file mode 100644 index 56c0dc3433..0000000000 --- a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then - Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field - Equations_CI_GITURL=https://github.com/bollu/Coq-Equations -fi diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh deleted file mode 100644 index 99a11b9fbf..0000000000 --- a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then - quickchick_CI_BRANCH=fix-for-pr-8063 - quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick -fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index d38d1b06d1..68afe7ee4a 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,10 +7,12 @@ request to test it with the adapted version of the external project. An overlay is a file which defines where to look for the patched version so that testing is possible. It redefines some variables from [`ci-basic-overlay.sh`](../ci-basic-overlay.sh): -give the name of your branch using a `_CI_BRANCH` variable and the location of -your fork using a `_CI_GITURL` variable. +give the name of your branch / commit using a `_CI_REF` variable and the +location of your fork using a `_CI_GITURL` variable. The `_CI_GITURL` variable should be the URL of the repository without a trailing `.git`. +If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is +necessary to redefine the `_CI_ARCHIVEURL` variable as well. Moreover, the file contains very simple logic to test the pull request number or branch name and apply it only in this case. @@ -25,7 +27,7 @@ Example: `00669-maximedenes-ssr-merge.sh` containing #!/bin/sh if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh new file mode 100644 index 0000000000..76aa37d380 --- /dev/null +++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then + HoTT_CI_REF=fix-for-numeral-notations + HoTT_CI_GITURL=https://github.com/JasonGross/HoTT + HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive +fi |