diff options
Diffstat (limited to 'dev/ci')
64 files changed, 656 insertions, 340 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index bb13587e94..665b3768a4 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -36,9 +36,8 @@ On the condition that: - You do not push, to the branches that we test, commits that haven't been first tested to compile with the corresponding branch(es) of Coq. -- Your development compiles in less than 35 minutes with just two threads. - If this is not the case, consider adding a "lite" target that compiles just - part of it. +- You maintain a reasonable build time for your development, or you provide + a "lite" target that we can use. In case you forget to comply with these last three conditions, we would reach out to you and give you a 30-day grace period during which your development @@ -48,15 +47,16 @@ CI. ### Add your development by submitting a pull request -Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at -[`ci-coq-dpdgraph.sh`](/dev/ci/ci-coq-dpdgraph.sh) or -[`ci-fiat-parsers.sh`](/dev/ci/ci-fiat-parsers.sh) for simple examples); +Add a new `ci-mydev.sh` script to [`dev/ci`](.) (have a look at +[`ci-coq-dpdgraph.sh`](ci-coq-dpdgraph.sh) or +[`ci-fiat-parsers.sh`](ci-fiat-parsers.sh) for simple examples); set the corresponding variables in -[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding -target to [`Makefile.ci`](/Makefile.ci); add new jobs to -[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that -this new target is run. **Do not hesitate to submit an incomplete pull request -if you need help to finish it.** +[`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the corresponding +target to [`Makefile.ci`](../../Makefile.ci); add new jobs to +[`.gitlab-ci.yml`](../../.gitlab-ci.yml), +[`.circleci/config.yml`](../../.circleci/config.yml) and +[`.travis.yml`](../../.travis.yml) so that this new target is run. **Do not +hesitate to submit an incomplete pull request if you need help to finish it.** You may also be interested in having your development tested in our performance benchmark. Currently this is done by providing an OPAM package @@ -71,62 +71,118 @@ When you submit a pull request (PR) on Coq GitHub repository, this will automatically launch a battery of CI tests. The PR will not be integrated unless these tests pass. -Currently, we have two CI platforms: +We are currently running tests on the following platforms: -- Travis is the main CI platform. It tests the compilation of Coq, of the +- GitLab CI is the main CI platform. It tests the compilation of Coq, of the documentation, and of CoqIDE on Linux with several versions of OCaml / camlp5, and with warnings as errors; it runs the test-suite and tests the - compilation of several external developments. It also tests the compilation - of Coq on OS X. + 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 + `./configure`. It should allow complying with this discipline without pain. - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. -You can anticipate the results of these tests prior to submitting your PR -by having them run of your fork of Coq, on GitHub or GitLab. This can be -especially helpful given that our Travis platform is often overloaded and -therefore there can be a significant delay before these tests are actually -run on your PR. To take advantage of this, simply create a Travis account -and link it to your GitHub account, or activate the pipelines on your GitLab -fork. +GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit +message to bypass CI. Do not use this unless your commit only changes files +that are not compiled (e.g. Markdown files like this one, or files under +[`.github/`](../../.github/)). -You can also run one CI target locally (using `make ci-somedev`). +You can anticipate the results of most of these tests prior to submitting your +PR by running GitLab CI on your private branches. To do so follow these steps: + +1. Log into GitLab CI (the easiest way is to sign in with your GitHub account). +2. Click on "New Project". +3. Choose "CI / CD for external repository" then click on "GitHub". +4. Find your fork of the Coq repository and click on "Connect". +5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project). +6. You are encouraged to go to the CI / CD general settings and increase the + timeout from 1h to 2h for better reliability. -Whenever your PR breaks tested developments, you should either adapt it -so that it doesn't, or provide a branch fixing these developments (or at -least work with the author of the development / other Coq developers to -prepare these fixes). Then, add an overlay in -[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there) -in a separate commit in your PR. +Now everytime you push (including force-push unless you changed the default +GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and +CI will be run. You will receive an e-mail with a report of the failures if +there are some. -The process to merge your PR is then to submit PRs to the external -development repositories, merge the latter first (if the fixes are -backward-compatible), drop the overlay commit and merge the PR on Coq then. +You can also run one CI target locally (using `make ci-somedev`). + +See also [`test-suite/README.md`](../../test-suite/README.md) for information about adding new tests to the test-suite. -See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. +### Breaking changes +When your PR breaks an external project we test in our CI, you must prepare a +patch (or ask someone to prepare a patch) to fix the project: -Travis specific information ---------------------------- +1. Fork the external project, create a new branch, push a commit adapting + the project to your changes. +2. Test your pull request with your adapted version of the external project by + adding an overlay file to your pull request (cf. + [`dev/ci/user-overlays/README.md`](user-overlays/README.md)). +3. Fixes to external libraries (pure Coq projects) *must* be backward + compatible (i.e. they should also work with the development version of Coq, + and the latest stable version). This will allow you to open a PR on the + external project repository to have your changes merged *before* your PR on + Coq can be integrated. -Travis rebuilds all of Coq's executables and stdlib for each job. Coq -is built with `./configure -local`, then used for the job's test. + On the other hand, patches to plugins (projects linking to the Coq ML API) + can very rarely be made backward compatible and plugins we test will + generally have a dedicated branch per Coq version. + You can still open a pull request but the merging will be requested by the + developer who merges the PR on Coq. There are plans to improve this, cf. + [#6724](https://github.com/coq/coq/issues/6724). +Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file. -GitLab specific information ---------------------------- +Advanced GitLab CI information +------------------------------ -GitLab is set up to use the "build artifact" feature to avoid -rebuilding Coq. In one job, Coq is built with `./configure -prefix -install` and `make install` is run, then the `install` directory +GitLab CI is set up to use the "build artifact" feature to avoid +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, in two different copies varying in the OCaml - version used to build Coq + 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. As an exception to the above, jobs testing that compilation triggers -no Ocaml warnings build Coq in parallel with other tests. +no OCaml warnings build Coq in parallel with other tests. + +### GitLab and Windows + +If your repository has access to runners tagged `windows`, setting the +secret variable `WINDOWS` to `enabled` will add jobs building Windows +versions of Coq (32bit and 64bit). + +The Windows jobs are enabled on Coq's repository, where pipelines for +pull requests run. + +### GitLab and Docker + +System and opam packages are installed in a Docker image. The image is +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), +and [`Dockerfile`](docker/bionic_coq/Dockerfile) + +The Docker building job reuses the uploaded image if it is available, +but if you wish to save more time you can skip the job by setting +`SKIP_DOCKER` to `true`. + +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.. + +See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 524a55a423..7bf9ad8c9b 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -1,9 +1,15 @@ #!/bin/bash + set -e -x + +APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c + wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c -eval $(opam config env) -opam install -y ocamlfind camlp5 -cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate + +opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH +eval "$(opam config env)" +opam install -y num ocamlfind camlp5 ounit + +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 48e01e9e93..87d837b387 100644..100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -11,6 +11,8 @@ ######################################################################## : "${mathcomp_CI_BRANCH:=master}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" +: "${oddorder_CI_BRANCH:=master}" +: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}" ######################################################################## # UniMath @@ -19,13 +21,13 @@ : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}" ######################################################################## -# Unicoq + Metacoq +# Unicoq + Mtac2 ######################################################################## : "${unicoq_CI_BRANCH:=master}" : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}" -: "${metacoq_CI_BRANCH:=master}" -: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}" +: "${mtac2_CI_BRANCH:=master-sync}" +: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}" ######################################################################## # Mathclasses + Corn @@ -91,6 +93,12 @@ : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}" ######################################################################## +# cross-crypto +######################################################################## +: "${cross_crypto_CI_BRANCH:=master}" +: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}" + +######################################################################## # fiat_parsers ######################################################################## : "${fiat_parsers_CI_BRANCH:=master}" @@ -142,7 +150,7 @@ ######################################################################## # Equations ######################################################################## -: "${Equations_CI_BRANCH:=8.8+alpha}" +: "${Equations_CI_BRANCH:=master}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" ######################################################################## @@ -150,3 +158,27 @@ ######################################################################## : "${Elpi_CI_BRANCH:=coq-master}" : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}" + +######################################################################## +# fcsl-pcm +######################################################################## +: "${fcsl_pcm_CI_BRANCH:=master}" +: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" + +######################################################################## +# pidetop +######################################################################## +: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" + +######################################################################## +# ext-lib +######################################################################## +: "${ext_lib_CI_BRANCH:=master}" +: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}" + +######################################################################## +# quickchick +######################################################################## +: "${quickchick_CI_BRANCH:=master}" +: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}" diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index c90e516ae9..0082919679 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -6,11 +6,11 @@ ci_dir="$(dirname "$0")" # Let's avoid to source ci-common twice in this case if [ -z "${CI_BUILD_DIR}" ]; then - source ${ci_dir}/ci-common.sh + . "${ci_dir}/ci-common.sh" fi -bignums_CI_DIR=${CI_BUILD_DIR}/Bignums +bignums_CI_DIR="${CI_BUILD_DIR}/Bignums" -git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR} +git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}" -( cd ${bignums_CI_DIR} && make && make install) +( cd "${bignums_CI_DIR}" && make && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 558e8cbb8c..8ce5f2418f 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" CoLoR_CI_DIR=${CI_BUILD_DIR}/color # Compile CoLoR -git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR} -( cd ${CoLoR_CI_DIR} && make ) +git_checkout "${CoLoR_CI_BRANCH}" "${CoLoR_CI_GITURL}" "${CoLoR_CI_DIR}" +( cd "${CoLoR_CI_DIR}" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index d7a356930e..85df249d38 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,8 +8,13 @@ export NJOBS if [ -n "${GITLAB_CI}" ]; then + export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi else if [ -n "${TRAVIS}" ]; then @@ -20,8 +25,10 @@ else export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" else # assume local - export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH fi + export OCAMLPATH="$PWD:$OCAMLPATH" export COQBIN="$PWD/bin" fi export PATH="$COQBIN:$PATH" @@ -35,10 +42,10 @@ ls "$COQBIN" CI_BUILD_DIR="$PWD/_build_ci" # shellcheck source=ci-basic-overlay.sh -source "${ci_dir}/ci-basic-overlay.sh" +. "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null - source "${overlay}" + . "${overlay}" done mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" @@ -66,11 +73,6 @@ git_checkout() echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } -checkout_mathcomp() -{ - git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} -} - make() { # +x: add x only if defined @@ -88,19 +90,29 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp "${mathcomp_CI_DIR}" + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + ( cd "${mathcomp_CI_DIR}/mathcomp" && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make Makefile.coq && make -f Makefile.coq all && make install ) + 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' + + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + + ( cd "${mathcomp_CI_DIR}/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 6a0ce2aefa..8d490591b6 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,11 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert +CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" -opam install -j "$NJOBS" -y menhir -git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} +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 "${CompCert_CI_DIR}" && ./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 5d6bd6a368..5d57fce1c7 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph +coq_dpdgraph_CI_DIR="${CI_BUILD_DIR}/coq-dpdgraph" -git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} +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 "${coq_dpdgraph_CI_DIR}" && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 40eff03b78..d86d61ef6a 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot +Coquelicot_CI_DIR="${CI_BUILD_DIR}/coquelicot" install_ssreflect -git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR} +git_checkout "${Coquelicot_CI_BRANCH}" "${Coquelicot_CI_GITURL}" "${Coquelicot_CI_DIR}" -( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd "${Coquelicot_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 54cad5df4c..9298fc70af 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Corn_CI_DIR=${CI_BUILD_DIR}/corn +Corn_CI_DIR="${CI_BUILD_DIR}/corn" -git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} +git_checkout "${Corn_CI_BRANCH}" "${Corn_CI_GITURL}" "${Corn_CI_DIR}" -( cd ${Corn_CI_DIR} && make && make install ) +( cd "${Corn_CI_DIR}" && make && make install ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh index 8b725f6fec..ca759c7b39 100755 --- a/dev/ci/ci-cpdt.sh +++ b/dev/ci/ci-cpdt.sh @@ -1,10 +1,9 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" wget http://adam.chlipala.net/cpdt/cpdt.tgz tar xvfz cpdt.tgz ( cd cpdt && make clean && make ) - diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh new file mode 100755 index 0000000000..a0d3aa6551 --- /dev/null +++ b/dev/ci/ci-cross-crypto.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +cross_crypto_CI_DIR="${CI_BUILD_DIR}/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 ) diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index c44e0a6552..9c58034be1 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Elpi_CI_DIR=${CI_BUILD_DIR}/elpi +Elpi_CI_DIR="${CI_BUILD_DIR}/elpi" -git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR} +git_checkout "${Elpi_CI_BRANCH}" "${Elpi_CI_GITURL}" "${Elpi_CI_DIR}" -( cd ${Elpi_CI_DIR} && make && make install ) +( cd "${Elpi_CI_DIR}" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 62854afac6..98735b4ec4 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Equations_CI_DIR=${CI_BUILD_DIR}/Equations +Equations_CI_DIR="${CI_BUILD_DIR}/Equations" -git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR} +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 "${Equations_CI_DIR}" && 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 new file mode 100755 index 0000000000..cf212c2fb5 --- /dev/null +++ b/dev/ci/ci-ext-lib.sh @@ -0,0 +1,16 @@ +#!/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 + +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) diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh new file mode 100755 index 0000000000..fdc4c729b6 --- /dev/null +++ b/dev/ci/ci-fcsl-pcm.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +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}" + +( cd "${fcsl_pcm_CI_DIR}" && make ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 5ca3ac47fc..48a1366aba 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,11 +1,14 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto +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 ) +git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" -( cd ${fiat_crypto_CI_DIR} && make lite ) +( 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} ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 292331b813..35c2284050 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat +fiat_parsers_CI_DIR="${CI_BUILD_DIR}/fiat" -git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} +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 "${fiat_parsers_CI_DIR}" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index ec19bd9939..8599e4d50e 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Flocq_CI_DIR=${CI_BUILD_DIR}/flocq +Flocq_CI_DIR="${CI_BUILD_DIR}/flocq" -git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR} +git_checkout "${Flocq_CI_BRANCH}" "${Flocq_CI_GITURL}" "${Flocq_CI_DIR}" -( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd "${Flocq_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 53eb55fc45..118d151500 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology +formal_topology_CI_DIR="${CI_BUILD_DIR}/formal-topology" -git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} +git_checkout "${formal_topology_CI_BRANCH}" "${formal_topology_CI_GITURL}" "${formal_topology_CI_DIR}" -( cd ${formal_topology_CI_DIR} && make ) +( cd "${formal_topology_CI_DIR}" && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 8e6448e764..24cd9c4272 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq +GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq" -git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} +git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}" -( cd ${GeoCoq_CI_DIR} && \ - ./configure-ci.sh && \ - make ) +install_ssralg + +( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 693135a4c9..6ded97984e 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT +HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT -git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} +git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}" -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) +( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 267e13359b..1af0f634c4 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -1,41 +1,34 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${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 +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 -# Add or update the opam repo we need for dependency resolution -opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev - # Setup lambdaRust first -git_checkout ${lambdaRust_CI_BRANCH} ${lambdaRust_CI_GITURL} ${lambdaRust_CI_DIR} +git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}" # Extract required version of Iris -Iris_VERSION=$(cat ${lambdaRust_CI_DIR}/opam | fgrep coq-iris | egrep 'dev\.([0-9.-]+)' -o) -Iris_URL=$(opam show coq-iris.$Iris_VERSION -f upstream-url) -read -a Iris_URL_PARTS <<< $(echo $Iris_URL | tr '#' ' ') +Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris -git_checkout ${Iris_CI_BRANCH} ${Iris_URL_PARTS[0]} ${Iris_CI_DIR} ${Iris_URL_PARTS[1]} +git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}" # Extract required version of std++ -stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o) -stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url) -read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ') +stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ -git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} +git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}" # Build std++ -( cd ${stdpp_CI_DIR} && make && make install ) +( cd "${stdpp_CI_DIR}" && 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 ) +( cd "${Iris_CI_DIR}" && make && (test -n "${TRAVIS}" || make validate) && make install ) # Build lambdaRust -( cd ${lambdaRust_CI_DIR} && make && make install ) +( cd "${lambdaRust_CI_DIR}" && make && make install ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 820ff89eec..5981aaaae7 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2 +ltac2_CI_DIR="${CI_BUILD_DIR}/ltac2" -git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} +git_checkout "${ltac2_CI_BRANCH}" "${ltac2_CI_GITURL}" "${ltac2_CI_DIR}" -( cd ${ltac2_CI_DIR} && make && make tests && make install ) +( cd "${ltac2_CI_DIR}" && make && make tests && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index db4a31e549..6a064b2971 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes +math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes" -git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} +git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}" -( cd ${math_classes_CI_DIR} && make && make install ) +( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 701403f2cf..20328baf2a 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -2,14 +2,13 @@ # $0 is not the safest way, but... ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp +mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" +oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order" -checkout_mathcomp ${mathcomp_CI_DIR} +git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" +git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}" -# odd_order takes too much time for travis. -( cd ${mathcomp_CI_DIR}/mathcomp && \ - sed -i.bak '/PFsection/d' Make && \ - sed -i.bak '/stripped_odd_order_theorem/d' Make && \ - make Makefile.coq && make -f Makefile.coq all ) +( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install ) +( cd "${oddorder_CI_DIR}/" && make ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh deleted file mode 100755 index c813b1fe99..0000000000 --- a/dev/ci/ci-metacoq.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh - -unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq -metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq - -# Setup UniCoq - -git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} - -( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make && make install ) - -# Setup MetaCoq - -git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR} - -( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh new file mode 100755 index 0000000000..1372acb8e5 --- /dev/null +++ b/dev/ci/ci-mtac2.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq +mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2 + +# Setup UniCoq + +git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" + +( 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 ) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh new file mode 100755 index 0000000000..32cba0808e --- /dev/null +++ b/dev/ci/ci-pidetop.sh @@ -0,0 +1,22 @@ +#!/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}" + +# Travis / Gitlab have different filesystem layout due to use of +# `-local`. We need to improve this divergence but if we use Dune this +# "local" oddity goes away automatically so not bothering... +if [ -d "$COQBIN/../lib/coq" ]; then + COQLIB="$COQBIN/../lib/coq/" +else + COQLIB="$COQBIN/../" +fi + +( cd "${pidetop_CI_DIR}" && jbuilder build @install ) + +echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh new file mode 100755 index 0000000000..fc39e2685d --- /dev/null +++ b/dev/ci/ci-quickchick.sh @@ -0,0 +1,18 @@ +#!/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" + +install_ssreflect + +git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}" + +( cd "${quickchick_CI_DIR}" && make && make install) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 4e8c7e145e..58bbb7229f 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -1,35 +1,16 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR} -wget -qO- ${sf_lf_CI_TARURL} | tar xvz -wget -qO- ${sf_plf_CI_TARURL} | tar xvz -wget -qO- ${sf_vfa_CI_TARURL} | tar xvz +mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" || exit 1 +wget -qO- "${sf_lf_CI_TARURL}" | tar xvz +wget -qO- "${sf_plf_CI_TARURL}" | tar xvz +wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v -# Delete useless calls to try omega; unfold -patch vfa/SearchTree.v <<EOF -*** SearchTree.v.bak 2017-09-06 19:12:59.000000000 +0200 ---- SearchTree.v 2017-11-21 16:34:41.000000000 +0100 -*************** -*** 674,683 **** - forall i j : key, ~ (i > j) -> ~ (i < j) -> i=j. - Proof. - intros. -- try omega. (* Oops! [omega] cannot solve this one. -- The problem is that [i] and [j] have type [key] instead of type [nat]. -- The solution is easy enough: *) -- unfold key in *. - omega. - - (** So, if you get stuck on an [omega] that ought to work, ---- 674,679 ---- -EOF - ( cd lf && make clean && make ) ( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh index 25da01a822..e77a553047 100755 --- a/dev/ci/ci-template.sh +++ b/dev/ci/ci-template.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" Template_CI_BRANCH=master Template_CI_GITURL=https://github.com/Template/Template -Template_CI_DIR=${CI_BUILD_DIR}/Template +Template_CI_DIR="${CI_BUILD_DIR}/Template" -git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR} +git_checkout "${Template_CI_BRANCH}" "${Template_CI_GITURL}" "${Template_CI_DIR}" -( cd ${Template_CI_DIR} && make ) +( cd "${Template_CI_DIR}" && make ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 8ecd8c441d..31387c8ddc 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -tlc_CI_DIR=${CI_BUILD_DIR}/tlc +tlc_CI_DIR="${CI_BUILD_DIR}/tlc" -git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} +git_checkout "${tlc_CI_BRANCH}" "${tlc_CI_GITURL}" "${tlc_CI_DIR}" -( cd ${tlc_CI_DIR} && make ) +( cd "${tlc_CI_DIR}" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 66b56add77..aa20fe1ff0 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,14 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath +UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" -git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} - -( cd ${UniMath_CI_DIR} && \ - sed -i.bak '/Folds/d' Makefile && \ - sed -i.bak '/HomologicalAlgebra/d' Makefile && \ - make BUILD_COQ=no ) +git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" +( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 5760fbafb0..7a097eaab4 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -1,13 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -VST_CI_DIR=${CI_BUILD_DIR}/VST +VST_CI_DIR="${CI_BUILD_DIR}/VST" -# opam install -j ${NJOBS} -y menhir -git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} +git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" -# Targets are: msl veric floyd progs , we remove progs to save time -# Patch to avoid the upper version limit -( cd ${VST_CI_DIR} && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd ) +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md new file mode 100644 index 0000000000..919e2a735f --- /dev/null +++ b/dev/ci/docker/README.md @@ -0,0 +1,36 @@ +## Overall Docker Setup for Coq's CI. + +This directory provides Docker images to be used by Coq's CI. The +images do support Docker autobuild on `hub.docker.com` and Gitlab's +private registry. + +Gitlab CI will build and tag a Docker by default for every job if the +`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this +variable is usually set to `false` indeed to avoid booting a useless +job. + +## Manual Building + +You can also manually build and push any image: + +- Build the image `docker build -t base:$VERSION .` + +To upload/push to your hub: + +- Create a https://hub.docker.com account. +- Login into your space `docker login --username=$USER` +- Push the image: + + `docker tag base:$VERSION $USER/base:$VERSION` + + `docker push $USER/base:$VERSION` + +## Debugging / Misc + +To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>` + +Each `RUN` command creates an "layer", thus a Docker build is +incremental and it always help to put things updated more often at the +end. + +## Possible Improvements: + +- Use ARG for customizing versions, centralize variable setup; diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile new file mode 100644 index 0000000000..1a83593f50 --- /dev/null +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -0,0 +1,54 @@ +# CACHEKEY: "bionic_coq-V2018-06-04-V2" +# ^^ Update when modifying this file. + +FROM ubuntu:bionic +LABEL maintainer="e@x80.org" + +ENV DEBIAN_FRONTEND="noninteractive" + +RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \ + libgtk2.0-dev libgtksourceview2.0-dev \ + texlive-latex-extra texlive-fonts-recommended texlive-science \ + python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip + +RUN pip3 install antlr4-python3-runtime + +# Basic OPAM setup +ENV NJOBS="2" \ + OPAMROOT=/root/.opamcache \ + OPAMROOTISOK="true" + +# Base opam is the set of base packages required by Coq +ENV COMPILER="4.02.3" + +RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update + +# 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 jbuilder.1.0+beta20 ounit.2.0.8" \ + CI_OPAM="menhir.20180530 elpi.1.0.3 ocamlgraph.1.8.8" + +# BASE switch; CI_OPAM contains Coq's CI dependencies. +ENV CAMLP5_VER="6.14" \ + COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" + +RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM + +# base+32bit switch +RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER + +# EDGE switch +ENV COMPILER_EDGE="4.06.1" \ + CAMLP5_VER_EDGE="7.05" \ + COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" + +RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE + +# EDGE+flambda switch, we install CI_OPAM as to be able to use +# `ci-template-flambda` with everything. +RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat new file mode 100644 index 0000000000..70278e6d09 --- /dev/null +++ b/dev/ci/gitlab.bat @@ -0,0 +1,50 @@ +@ECHO OFF + +REM This script builds and signs the Windows packages on Gitlab + +if %ARCH% == 32 ( + SET ARCHLONG=i686 + SET CYGROOT=C:\cygwin + SET SETUP=setup-x86.exe +) + +if %ARCH% == 64 ( + SET ARCHLONG=x86_64 + SET CYGROOT=C:\cygwin64 + SET SETUP=setup-x86_64.exe +) + +powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')" +SET CYGCACHE=%CYGROOT%\var\cache\setup +SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/% +SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/% +SET DESTCOQ=C:\coq%ARCH%_inst +SET COQREGTESTING=Y +SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin + +if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build +if exist %DESTCOQ%\ rd /s /q %DESTCOQ% + +call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ + -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^ + -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ + -addon=bignums -make=N ^ + -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit + +copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit +7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit + +REM DO NOT echo the signing command below, as this would leak secrets in the logs +IF DEFINED WIN_CERTIFICATE_PATH ( + IF DEFINED WIN_CERTIFICATE_PASSWORD ( + ECHO Signing package + @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe + signtool verify /pa dev\nsis\*.exe + ) +) + +GOTO :EOF + +:ErrorExit + ECHO ERROR %0 failed + EXIT /b 1 diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index 7716bcb59a..e9ba114148 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,3 +1,5 @@ +#!/bin/sh + if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh deleted file mode 100644 index c2e3670380..0000000000 --- a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then - Equations_CI_BRANCH=rm-local-polymorphic-flag - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh new file mode 100644 index 0000000000..f4cb71cf19 --- /dev/null +++ b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "6454" ] || [ "$CI_BRANCH" = "evar+strict_to_constr" ]; then + + # ltac2_CI_BRANCH=econstr+more_fix + # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=evar+strict_to_constr + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations +fi diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh deleted file mode 100644 index 78789a6fc5..0000000000 --- a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then - HoTT_CI_BRANCH=check-poly-effects - HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git -fi diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh deleted file mode 100644 index 9677b35253..0000000000 --- a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then - Equations_CI_BRANCH=API-removal - Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git - coq_dpdgraph_CI_BRANCH=API-removal - coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git - ltac2_CI_BRANCH=API-removal - ltac2_CI_GITURL=https://github.com/gares/ltac2.git -fi diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh deleted file mode 100644 index 4b681909d6..0000000000 --- a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh +++ /dev/null @@ -1,7 +0,0 @@ - if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then - ltac2_CI_BRANCH=econstr+more_fix - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=econstr+more_fix - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh deleted file mode 100644 index 8a50fb1111..0000000000 --- a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then - Equations_CI_BRANCH=fix-6535 - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh deleted file mode 100644 index 2451657d43..0000000000 --- a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then - ltac2_CI_BRANCH=fix-for/6676 - ltac2_CI_GITURL=https://github.com/gares/ltac2.git - Equations_CI_BRANCH=fix-for/6676 - Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh deleted file mode 100644 index 3a3ab44e03..0000000000 --- a/dev/ci/user-overlays/06686-ccnv-no-proj.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then - Equations_CI_BRANCH=ccnv-fixes - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh deleted file mode 100644 index d1d61fec2e..0000000000 --- a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh +++ /dev/null @@ -1,13 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then - ltac2_CI_BRANCH=located+vernac - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+vernac - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - fiat_parsers_CI_BRANCH=located+vernac - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - - Elpi_CI_BRANCH=located+vernac - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06775-univ-cumul-weak.sh b/dev/ci/user-overlays/06775-univ-cumul-weak.sh deleted file mode 100644 index 8afcbf78a3..0000000000 --- a/dev/ci/user-overlays/06775-univ-cumul-weak.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6775" ] || [ "$CI_BRANCH" = "univ-cumul" ]; then - Elpi_CI_BRANCH=coq-master - Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh deleted file mode 100644 index df3e9cef28..0000000000 --- a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh +++ /dev/null @@ -1,14 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then - - ltac2_CI_BRANCH=located+vernac_2 - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+vernac_2 - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - # fiat_parsers_CI_BRANCH=located+vernac - # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - - Elpi_CI_BRANCH=located+vernac_2 - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh deleted file mode 100644 index a785290e7c..0000000000 --- a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then - - ltac2_CI_BRANCH=located+libnames - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+libnames - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - Elpi_CI_BRANCH=located+libnames - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - - coq_dpdgraph_CI_BRANCH=located+libnames - coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git - -fi diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh new file mode 100644 index 0000000000..b22ab36302 --- /dev/null +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || \ + [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then + + pidetop_CI_BRANCH=stm+top + pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git + +fi diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh deleted file mode 100644 index 5dedca0ca5..0000000000 --- a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; then - - Equations_CI_BRANCH=ssr+correct_packing - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - ltac2_CI_BRANCH=ssr+correct_packing - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Elpi_CI_BRANCH=ssr+correct_packing - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - -fi diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh deleted file mode 100644 index 333a9e84bd..0000000000 --- a/dev/ci/user-overlays/06923-ppedrot-export-options.sh +++ /dev/null @@ -1,7 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then - ltac2_CI_BRANCH=export-options - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - - Equations_CI_BRANCH=export-options - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh new file mode 100644 index 0000000000..cf2af9ae95 --- /dev/null +++ b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "6960" ] || [ "$CI_BRANCH" = "ltac+tacdepr" ]; then + + # Equations_CI_BRANCH=ssr+correct_packing + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + ltac2_CI_BRANCH=ltac+tacdepr + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + # Elpi_CI_BRANCH=ssr+correct_packing + # Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + +fi diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh new file mode 100644 index 0000000000..e6c48d10a6 --- /dev/null +++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then + Equations_CI_BRANCH=unification-returns-option + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/ci/user-overlays/07136-evar-map-econstr.sh b/dev/ci/user-overlays/07136-evar-map-econstr.sh new file mode 100644 index 0000000000..06aa62726d --- /dev/null +++ b/dev/ci/user-overlays/07136-evar-map-econstr.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "7136" ] || [ "$CI_BRANCH" = "evar-map-econstr" ]; then + Equations_CI_BRANCH=8.9+alpha + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git + + Elpi_CI_BRANCH=coq-7136 + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh new file mode 100644 index 0000000000..7e554684e8 --- /dev/null +++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then + + # Equations_CI_BRANCH=ssr+correct_packing + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + # ltac2_CI_BRANCH=ssr+correct_packing + # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Elpi_CI_BRANCH=api+vernac_expr_iso + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + +fi diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh new file mode 100644 index 0000000000..ea9cd8ee07 --- /dev/null +++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then + + # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550 + # + # equations + # ltac2 + + # The below developments should instead use a backwards compatible fix. + # + # color + # iris-lambda-rust + # math-classes + # formal-topology + + ltac2_CI_BRANCH=tactics+push_fix_naming_out + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=tactics+push_fix_naming_out + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 0000000000..517088a247 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh new file mode 100644 index 0000000000..6939ead2ba --- /dev/null +++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then + + # this branch contains a commit not present on coq-master that triggers + # the universe restriction bug #7472 + Elpi_CI_BRANCH=overlay-7495 + Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git + +fi diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh new file mode 100644 index 0000000000..115f29f1ee --- /dev/null +++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh @@ -0,0 +1,14 @@ +if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then + + _OVERLAY_BRANCH=vernac+move_parser + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + ltac2_CI_BRANCH="$_OVERLAY_BRANCH" + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh new file mode 100644 index 0000000000..b4f7161395 --- /dev/null +++ b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=misctypes+bye2 + +if [ "$CI_PULL_REQUEST" = "7677" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9f0377ceea..41212568d8 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -1,16 +1,31 @@ # Add overlays for your pull requests in this directory -An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh). +When your pull request breaks an external project we test in our CI and you +have prepared a branch with the fix, you can add an "overlay" to your pull +request to test it with the adapted version of the external project. -The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`. +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. + +Moreover, the file contains very simple logic to test the pull request number +or branch name and apply it only in this case. + +The name of your overlay file should start with a five-digit pull request +number, followed by a dash, anything (for instance your GitHub nickname +and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). 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_GITURL=https://github.com/maximedenes/math-comp.git fi ``` -(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh)) +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) |