diff options
Diffstat (limited to 'dev')
43 files changed, 287 insertions, 282 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index da5ac2b15c..8a49b97dac 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -793,7 +793,7 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then + if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h @@ -1387,12 +1387,12 @@ function make_coq_installer { # Provides BigN, BigZ, BigQ that used to be part of Coq standard library function make_addon_bignums { - bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_BRANCH" | cut -f 1) + bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_REF" | cut -f 1) if [[ "$bignums_SHA" == "" ]]; then - # $bignums_CI_BRANCH must have been a tag and not a branch - bignums_SHA="$bignums_CI_BRANCH" + # $bignums_CI_REF must have been a tag / commit and not a branch + bignums_SHA="$bignums_CI_REF" fi - if build_prep "${bignums_CI_GITURL}/archive" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then + if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local log1 make all @@ -1405,12 +1405,12 @@ function make_addon_bignums { # A new (experimental) tactic language function make_addon_ltac2 { - ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_BRANCH" | cut -f 1) + ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1) if [[ "$ltac2_SHA" == "" ]]; then - # $ltac2_CI_BRANCH must have been a tag and not a branch - ltac2_SHA="$ltac2_CI_BRANCH" + # $ltac2_CI_REF must have been a tag / commit and not a branch + ltac2_SHA="$ltac2_CI_REF" fi - if build_prep "${ltac2_CI_GITURL}/archive" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then + if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then log1 make all log2 make install build_post @@ -1421,12 +1421,12 @@ function make_addon_ltac2 { # A function definition plugin function make_addon_equations { - Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_BRANCH" | cut -f 1) + Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1) if [[ "$Equations_SHA" == "" ]]; then - # $Equations_CI_BRANCH must have been a tag and not a branch - Equations_SHA="$Equations_CI_BRANCH" + # $Equations_CI_REF must have been a tag / commit and not a branch + Equations_SHA="$Equations_CI_REF" fi - if build_prep "${Equations_CI_GITURL}/archive" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then + if build_prep "$Equations_CI_ARCHIVEURL" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then # Note: PATH is autmatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile @@ -1448,10 +1448,10 @@ function make_addons { export CI_BRANCH="" export CI_PULL_REQUEST="" fi - . /build/ci-basic-overlay.sh for overlay in /build/user-overlays/*.sh; do . "$overlay" done + . /build/ci-basic-overlay.sh for addon in $COQ_ADDONS; do "make_addon_$addon" diff --git a/dev/ci/README.md b/dev/ci/README.md index 45176581cd..b4ea6838bf 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -75,9 +75,6 @@ We are currently running tests on the following platforms: camlp5, and with warnings as errors; it runs the test-suite and tests the compilation of several external developments. -- Circle CI runs tests that are redundant with GitLab CI and may be removed - eventually. - - Travis CI is used to test the compilation of Coq and run the test-suite on macOS. It also runs a linter that checks whitespace discipline. A [pre-commit hook](../tools/pre-commit) is automatically installed by @@ -139,15 +136,35 @@ 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: -- the Coq executables and stdlib, in three copies varying in - architecture and OCaml version used to build Coq. -- the Coq documentation, built only in the `build:base` job. When submitting - a documentation PR, this can help reviewers checking the rendered result. +### 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: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + +- the Coq documentation, built in the `doc:*` jobs. When submitting + a documentation PR, this can help reviewers checking the rendered result: -As an exception to the above, jobs testing that compilation triggers -no OCaml warnings build Coq in parallel with other tests. + + 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 @@ -165,8 +182,7 @@ automatically built and uploaded to your GitLab registry, and is loaded by subsequent jobs. **IMPORTANT**: When updating Coq's CI docker image, you must modify -the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml), +the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) and [`Dockerfile`](docker/bionic_coq/Dockerfile) The Docker building job reuses the uploaded image if it is available, @@ -175,6 +191,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 a68cd0933e..7af648f0a6 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -20,10 +20,6 @@ else then export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" export CI_BRANCH="$TRAVIS_BRANCH" - elif [ -n "${CIRCLECI}" ]; - then - export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" - export CI_BRANCH="$CIRCLE_BRANCH" else # assume local CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH @@ -38,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() @@ -88,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 new file mode 100755 index 0000000000..e0395754e5 --- /dev/null +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +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 "${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 48a1366aba..7e8013be9b 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -3,12 +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 ) - -fiat_crypto_CI_TARGETS1="printlite lite lite-display" -fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display" -( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) +( 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 6ded97984e..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 ) +( 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..d22b9c8f7c 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" && jbuilder build @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/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 diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 2bec09de2b..bccd3fefb4 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -33,7 +33,7 @@ if [ -z "$GUESS_CHECKER" ]; then -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ - -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ + -I $COQTOP/plugins/firstorder \ -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 70a9756e51..ec72f96509 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -33,7 +33,7 @@ (defun coqdev-default-directory () "Return the Coq repository containing `default-directory'." - (let ((dir (locate-dominating-file default-directory "META.coq"))) + (let ((dir (locate-dominating-file default-directory "META.coq.in"))) (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index c8385da618..98190b05b5 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -17,7 +17,7 @@ let ppripos (ri,pos) = | Reloc_getglobal kn -> print_string ("getglob "^(Constant.to_string kn)^"\n") | Reloc_proj_name p -> - print_string ("proj "^(Constant.to_string p)^"\n") + print_string ("proj "^(Projection.Repr.to_string p)^"\n") ); print_flush () |