diff options
Diffstat (limited to 'dev/ci')
94 files changed, 1304 insertions, 534 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md new file mode 100644 index 0000000000..6ca3aa2981 --- /dev/null +++ b/dev/ci/README-developers.md @@ -0,0 +1,165 @@ +Information for developers about the CI system +---------------------------------------------- + +When you submit a pull request (PR) on the Coq GitHub repository, this will +automatically launch a battery of CI tests. The PR will not be integrated +unless these tests pass. + +We are currently running tests on the following platforms: + +- 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 and with warnings as errors; it runs the test-suite and + tests the compilation of several external developments. + +- 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 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. + +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. + +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. + +### 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. There is experimental support for an improved workflow, see +[the next section](#experimental-automatic-overlay-creation-and-building), below +are the steps to manually prepare a patch: + +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. + + 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.md`](../../CHANGES.md) file. + +### Experimental automatic overlay creation and building + +If you break external projects that are hosted on GitHub, you can use +the `create-overlays.sh` script to automatically perform most of the +above steps. In order to do so, call the script as: +``` +./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac +``` +replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR +number. The script will: + +- checkout the contributions and prepare the branch/remote so you can + just commit the fixes and push, +- add the corresponding overlay file in `dev/ci/user-overlays`. + +For problems related to ML-plugins, if you use `dune build` to build +Coq, it will actually be aware of the broken contributions and perform +a global build. This is very convenient when using `merlin` as you +will get a coherent view of all the broken plugins, with full +incremental cross-project rebuild. + +Advanced GitLab CI information +------------------------------ + +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 + +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 + + Additionally, an experimental Dune build is provided: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev + +- the Coq documentation, built in the `doc:*` jobs. When submitting + a documentation PR, this can help reviewers checking the rendered result: + + + Coq's Reference Manual [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + + Coq's Standard Library Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base + + Coq's ML API Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc + +### 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). + +If the secret variable `WINDOWS` is set to `enabled_all_addons`, +an extended set of addons will be added to the Windows installer. +This leads to a considerable runtime in CI so this is not enabled +by default for pipelines for pull requests. + +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) +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/README-users.md b/dev/ci/README-users.md new file mode 100644 index 0000000000..01769aeddb --- /dev/null +++ b/dev/ci/README-users.md @@ -0,0 +1,85 @@ +Information for external library / Coq plugin authors +----------------------------------------------------- + +You are encouraged to consider submitting your development for addition to +Coq's CI. This means that: + +- Any time that a proposed change is breaking your development, Coq developers + will send you patches to adapt it or, at the very least, will work with you + to see how to adapt it. + +On the condition that: + +- At the time of the submission, your development works with Coq's + `master` branch. + +- Your development is publicly available in a git repository and we can easily + send patches to you (e.g. through pull / merge requests). + +- You react in a timely manner to discuss / integrate those patches. + +- 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. + + For that, we recommend setting a CI system for you development, see + [supported CI images for Coq](#supported-ci-images-for-coq) below. + +- 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 +would be moved into our "allow failure" category. At the end of the grace +period, in the absence of progress, the development would be removed from our +CI. + +### Timely merging of overlays + +A pitfall of the current CI setup is that when a breaking change is +merged in Coq upstream, CI for your contrib will be broken until you +merge the corresponding pull request with the fix for your contribution. + +As of today, you have to worry about synchronizing with Coq upstream +every once in a while; we hope we will improve this in the future by +using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is +to give merge permissions to someone from the Coq team as to help with +these kind of merges. + +### Add your development by submitting a pull request + +Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding +variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the +corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to +[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run. +Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an +example. **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 +in https://github.com/coq/opam-coq-archive and opening an issue at +https://github.com/coq/coq-bench/issues. + +### Recommended branching policy. + +It is sometimes the case that you will need to maintain a branch of +your development for particular Coq versions. This is in fact very +likely if your development includes a Coq ML plugin. + +We thus recommend a branching convention that mirrors Coq's branching +policy. Then, you would have a `master` branch that follows Coq's +`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so +on. + +This convention will be supported by tools in the future to make some +developer commands work more seamlessly. + +### Supported CI images for Coq + +The Coq developers and contributors provide official Docker and Nix +images for testing against Coq master. Using these images is highly +recommended: + +- For Docker, see: https://github.com/coq-community/docker-coq +- For Nix, see the setup at + https://github.com/coq-community/manifesto/wiki/Continuous-Integration-with-Nix diff --git a/dev/ci/README.md b/dev/ci/README.md index bb13587e94..afbfab3ac6 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -6,127 +6,15 @@ breakage on our Continuous Integration (CI) platforms *before* integration, so as to ensure better robustness and catch problems as early as possible. These tests include the compilation of several external libraries / plugins. -This document contains information for both external library / plugin authors, -who might be interested in having their development tested, and for Coq -developers / contributors, who must ensure that they don't break these -external developments accidentally. +This README is split into two specific documents: -*Remark:* the CI policy outlined in this document is susceptible to evolve and -specific accommodations are of course possible. +- [README-users.md](./README-users.md) which contains information for + authors of external libraries and plugins who might be interested in + having their development tested in our CI system. -Information for external library / plugin authors -------------------------------------------------- +- [README-developers.md](./README-developers.md) for Coq developers / + contributors, who must ensure that they don't break these external + developments accidentally. -You are encouraged to consider submitting your development for addition to -our CI. This means that: - -- Any time that a proposed change is breaking your development, Coq developers - will send you patches to adapt it or, at the very least, will work with you - to see how to adapt it. - -On the condition that: - -- At the time of the submission, your development works with Coq master branch. - -- Your development is publicly available in a git repository and we can easily - send patches to you (e.g. through pull / merge requests). - -- You react in a timely manner to discuss / integrate those patches. - -- 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. - -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 -would be moved into our "allow failure" category. At the end of the grace -period, in the absence of progress, the development would be removed from our -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); -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.** - -You may also be interested in having your development tested in our -performance benchmark. Currently this is done by providing an OPAM package -in https://github.com/coq/opam-coq-archive and opening an issue at -https://github.com/coq/coq-bench/issues. - - -Information for developers --------------------------- - -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: - -- Travis 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. - -- 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. - -You can also run one CI target locally (using `make ci-somedev`). - -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. - -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. - -See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. - - -Travis specific information ---------------------------- - -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. - - -GitLab specific 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 -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 - -As an exception to the above, jobs testing that compilation triggers -no Ocaml warnings build Coq in parallel with other tests. +*Remark:* the CI policy outlined in these documents is susceptible to +evolve and specific accommodations are of course possible. diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 524a55a423..abeb039c0e 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -1,9 +1,15 @@ #!/bin/bash + set -e -x + +APPVEYOR_OPAM_SWITCH=4.07.0+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 ounit + +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-aac_tactics.sh b/dev/ci/ci-aac_tactics.sh new file mode 100755 index 0000000000..19f1f43746 --- /dev/null +++ b/dev/ci/ci-aac_tactics.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download aac_tactics + +( cd "${CI_BUILD_DIR}/aac_tactics" && make && make install ) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 48e01e9e93..96bc5be7ff 100644..100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -9,116 +9,162 @@ ######################################################################## # MathComp ######################################################################## -: "${mathcomp_CI_BRANCH:=master}" -: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" +: "${mathcomp_CI_REF:=master}" +: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" +: "${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_GITURL:=https://github.com/UniMath/UniMath.git}" +: "${UniMath_CI_REF:=master}" +: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" +: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}" ######################################################################## -# Unicoq + Metacoq +# Unicoq + Mtac2 ######################################################################## -: "${unicoq_CI_BRANCH:=master}" -: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}" +: "${unicoq_CI_REF:=master}" +: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" +: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" -: "${metacoq_CI_BRANCH:=master}" -: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}" +: "${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.git}" +: "${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.git}" +: "${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_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}" -: "${Iris_CI_BRANCH:=master}" -: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}" +# NB: stdpp and Iris refs are gotten from the opam files in the Iris +# and lambdaRust repos respectively. +: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" +: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" + +: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" +: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" -: "${lambdaRust_CI_BRANCH:=master}" -: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}" +: "${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_GITURL:=https://github.com/HoTT/HoTT.git}" +: "${HoTT_CI_REF:=master}" +: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" +: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" + +######################################################################## +# CoqHammer +######################################################################## +: "${coqhammer_CI_REF:=master}" +: "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}" +: "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}" ######################################################################## # Ltac2 ######################################################################## -: "${ltac2_CI_BRANCH:=master}" -: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}" +: "${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_GITURL:=https://github.com/GeoCoq/GeoCoq.git}" +: "${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_GITURL:=https://gitlab.inria.fr/flocq/flocq.git}" +: "${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_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}" +# The URL for downloading a tgz snapshot of the master branch is +# https://scm.gforge.inria.fr/anonscm/gitweb?p=coquelicot/coquelicot.git;a=snapshot;h=refs/heads/master;sf=tgz +# See https://gforge.inria.fr/scm/browser.php?group_id=3599 +# Since this URL doesn't fit to our standard mechanism and since Coquelicot doesn't seem to change frequently, +# we use a fixed version, which has a download path which does fit to our standard mechanism. +# ATTENTION: The archive URL might depend on the version! +: "${Coquelicot_CI_REF:=coquelicot-3.0.2}" +: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" +: "${Coquelicot_CI_ARCHIVEURL:=https://gforge.inria.fr/frs/download.php/file/37523}" ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_BRANCH:=master}" -: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}" +: "${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_GITURL:=https://github.com/PrincetonUniversity/VST.git}" +: "${vst_CI_REF:=master}" +: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}" + +######################################################################## +# cross-crypto +######################################################################## +: "${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_GITURL:=https://github.com/mit-plv/fiat.git}" +: "${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_GITURL:=https://github.com/mit-plv/fiat-crypto.git}" +: "${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_GITURL:=https://github.com/bmsherman/topology.git}" +: "${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 ######################################################################## -: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}" -: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" +: "${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_GITURL:=https://github.com/fblanqui/color.git}" +: "${color_CI_REF:=master}" +: "${color_CI_GITURL:=https://github.com/fblanqui/color}" +: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" ######################################################################## # SF @@ -130,23 +176,89 @@ ######################################################################## # TLC ######################################################################## -: "${tlc_CI_BRANCH:=master}" -: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}" +: "${tlc_CI_REF:=master}" +: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}" ######################################################################## # Bignums ######################################################################## -: "${bignums_CI_BRANCH:=master}" -: "${bignums_CI_GITURL:=https://github.com/coq/bignums.git}" +: "${bignums_CI_REF:=master}" +: "${bignums_CI_GITURL:=https://github.com/coq/bignums}" +: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" + +######################################################################## +# bedrock2 +######################################################################## +: "${bedrock2_CI_REF:=master}" +: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" +: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" ######################################################################## # Equations ######################################################################## -: "${Equations_CI_BRANCH:=8.8+alpha}" -: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" +: "${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_GITURL:=https://github.com/LPCIC/coq-elpi.git}" +: "${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_REF:=master}" +: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" +: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" + +######################################################################## +# ext-lib +######################################################################## +: "${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_REF:=master}" +: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" +: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" + +######################################################################## +# plugin_tutorial +######################################################################## +: "${plugin_tutorial_CI_REF:=master}" +: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" +: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" + +######################################################################## +# menhirlib +######################################################################## +: "${menhirlib_CI_REF:=master}" +: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}" +: "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" + +######################################################################## +# aac_tactics +######################################################################## +: "${aac_tactics_CI_REF:=master}" +: "${aac_tactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" +: "${aac_tactics_CI_ARCHIVEURL:=${aac_tactics_CI_GITURL}/archive}" + +######################################################################## +# paramcoq +######################################################################## +: "${paramcoq_CI_REF:=master}" +: "${paramcoq_CI_GITURL:=https://github.com/coq-community/paramcoq}" +: "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh new file mode 100755 index 0000000000..5205946261 --- /dev/null +++ b/dev/ci/ci-bedrock2.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download bedrock2 + +( 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 c90e516ae9..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 - source ${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 558e8cbb8c..a0094b1006 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -1,10 +1,8 @@ #!/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 +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 d7a356930e..a5aa54144c 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,22 +8,30 @@ export NJOBS if [ -n "${GITLAB_CI}" ]; then + # Gitlab build, Coq installed into `_install_ci` + export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" -else - if [ -n "${TRAVIS}" ]; - then - export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" - export CI_BRANCH="$TRAVIS_BRANCH" - elif [ -n "${CIRCLECI}" ]; + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] then - export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" - export CI_BRANCH="$CIRCLE_BRANCH" - else # assume local - export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" fi +elif [ -d "$PWD/_build/install/default/" ]; +then + # Dune build + export OCAMLPATH="$PWD/_build/install/default/lib/" + export COQBIN="$PWD/_build/install/default/bin" + export COQLIB="$PWD/_build/install/default/lib/coq" + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH +else + # We assume we are in `-profile devel` build, thus `-local` is set + export OCAMLPATH="$PWD:$OCAMLPATH" export COQBIN="$PWD/bin" + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH fi + export PATH="$COQBIN:$PATH" # Coq's tools need an ending slash :S, we should fix them. @@ -31,44 +39,51 @@ 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 -source "${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" - -# 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() -{ - 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 checkout "${_COMMIT}" && \ - echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) -} - -checkout_mathcomp() +set +x +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" +set -x + +# [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() { - git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} + 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() @@ -86,21 +101,27 @@ make() # this installs just the ssreflect library of math-comp install_ssreflect() { - echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - - checkout_mathcomp "${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 ) - - echo -en 'travis_fold:end:ssr.install\\r' + echo 'Installing ssreflect' + + git_download mathcomp + + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ + make Makefile.coq && \ + make -f Makefile.coq ssreflect/all_ssreflect.vo && \ + make -f Makefile.coq install ) + +} + +# this installs just the ssreflect + algebra library of math-comp +install_ssralg() +{ + echo 'Installing ssralg' + + git_download mathcomp + + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ + make Makefile.coq && \ + make -f Makefile.coq algebra/all_algebra.vo && \ + make -f Makefile.coq install ) } diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 6a0ce2aefa..59a85e4726 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,11 +1,9 @@ #!/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 +git_download compcert -opam install -j "$NJOBS" -y menhir -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 deleted file mode 100755 index 5d6bd6a368..0000000000 --- a/dev/ci/ci-coq-dpdgraph.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh - -coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/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 ) diff --git a/dev/ci/ci-coq_dpdgraph.sh b/dev/ci/ci-coq_dpdgraph.sh new file mode 100755 index 0000000000..2373ea6c62 --- /dev/null +++ b/dev/ci/ci-coq_dpdgraph.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coq_dpdgraph + +( cd "${CI_BUILD_DIR}/coq_dpdgraph" && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-coqhammer.sh b/dev/ci/ci-coqhammer.sh new file mode 100755 index 0000000000..4384e6c828 --- /dev/null +++ b/dev/ci/ci-coqhammer.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coqhammer + +( cd "${CI_BUILD_DIR}/coqhammer" && make ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 40eff03b78..5d8817491d 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,11 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh - -Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot +. "${ci_dir}/ci-common.sh" 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 54cad5df4c..7d5d70cf90 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -1,10 +1,8 @@ #!/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 +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-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..900d12c1dd --- /dev/null +++ b/dev/ci/ci-cross-crypto.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download cross_crypto + +( 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 c44e0a6552..d60bf34ba2 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -1,10 +1,8 @@ #!/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 +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 62854afac6..b58a794da2 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -1,10 +1,9 @@ #!/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 +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 new file mode 100755 index 0000000000..5eb167d97d --- /dev/null +++ b/dev/ci/ci-ext-lib.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download ext_lib + +( 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 new file mode 100755 index 0000000000..cb951630c8 --- /dev/null +++ b/dev/ci/ci-fcsl-pcm.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssreflect + +git_download fcsl_pcm + +( 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..6bf3138346 --- /dev/null +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -0,0 +1,14 @@ +#!/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 && \ + ./etc/ci/remove_autogenerated.sh && \ + 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 5ca3ac47fc..7e8013be9b 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 +FORCE_GIT=1 +git_download 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 ) +# 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} && make lite ) +( 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 292331b813..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -1,10 +1,9 @@ #!/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 +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 ec19bd9939..e87483df0a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,10 +1,8 @@ #!/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 +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 53eb55fc45..8be5a06ed2 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -1,10 +1,8 @@ #!/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 +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 8e6448e764..8c57318477 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,12 +1,10 @@ #!/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 +install_ssralg -git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} +git_download GeoCoq -( cd ${GeoCoq_CI_DIR} && \ - ./configure-ci.sh && \ - make ) +( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 693135a4c9..c8e6fe690f 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -1,10 +1,8 @@ #!/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 +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 -skip-submodules && ./configure && make && make validate ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 267e13359b..95f143bb95 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -1,41 +1,30 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${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 +. "${ci_dir}/ci-common.sh" 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_download lambdaRust # 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_CI_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_URL_PARTS[0]} ${Iris_CI_DIR} ${Iris_URL_PARTS[1]} +git_download Iris # 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_CI_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_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} +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 820ff89eec..4df22bf249 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -1,10 +1,8 @@ #!/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 +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 db4a31e549..ae31a8e7f8 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,10 +1,8 @@ #!/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 +git_download math_classes -git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} - -( cd ${math_classes_CI_DIR} && 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 701403f2cf..a74f9fa4d3 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -2,14 +2,12 @@ # $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 +git_download mathcomp -checkout_mathcomp ${mathcomp_CI_DIR} +( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install ) -# 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 ) +git_download oddorder + +( cd "${CI_BUILD_DIR}/oddorder" && 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..7075d4d7f6 --- /dev/null +++ b/dev/ci/ci-mtac2.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download unicoq + +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) + +git_download mtac2 + +( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh new file mode 100755 index 0000000000..c641af2abb --- /dev/null +++ b/dev/ci/ci-paramcoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download paramcoq + +( cd "${CI_BUILD_DIR}/paramcoq" && make && make install ) diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh new file mode 100755 index 0000000000..6c26a71a21 --- /dev/null +++ b/dev/ci/ci-plugin_tutorial.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download plugin_tutorial + +( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ + pushd tuto0 && make && popd && \ + pushd tuto1 && make && popd && \ + pushd tuto2 && make && popd && \ + pushd tuto3 && make && popd ) diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh new file mode 100755 index 0000000000..08686d7ced --- /dev/null +++ b/dev/ci/ci-quickchick.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +install_ssreflect + +git_download quickchick + +( cd "${CI_BUILD_DIR}/quickchick" && make && make install) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 4f7e9517f4..60436e672c 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -1,18 +1,13 @@ #!/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 - -sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v -sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v - -( cd lf && make clean && make ) - -( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) +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 +( cd lf && make clean && make ) +( cd plf && make clean && make ) ( cd vfa && make clean && make ) 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 25da01a822..0000000000 --- a/dev/ci/ci-template.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -source ${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 8ecd8c441d..a2f0bea555 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -1,10 +1,9 @@ #!/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 +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 66b56add77..a7644fee23 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,14 +1,8 @@ #!/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 - -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_download UniMath +( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 5760fbafb0..169d1a41db 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -1,13 +1,8 @@ #!/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 +git_download vst -# opam install -j ${NJOBS} -y menhir -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 "${CI_BUILD_DIR}/vst" && 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..3fc6dce4e5 --- /dev/null +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -0,0 +1,67 @@ +# CACHEKEY: "bionic_coq-V2018-11-08-V1" +# ^^ 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 --no-install-recommends -y -qq \ + # Dependencies of the image, the test-suite and external projects + m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \ + # Dependencies of lablgtk (for CoqIDE) + libgtk2.0-dev libgtksourceview2.0-dev \ + # Dependencies of stdlib and sphinx doc + texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ + xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + # Dependencies of source-doc and coq-makefile + texlive-science tipa + +# More dependencies of the sphinx doc +RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 + +# We need to install OPAM 2.0 manually for now. +RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam + +# Basic OPAM setup +ENV NJOBS="2" \ + OPAMJOBS="2" \ + OPAMROOT=/root/.opamcache \ + OPAMROOTISOK="true" \ + OPAMYES="true" + +# Base opam is the set of base packages required by Coq +ENV COMPILER="4.05.0" + +# 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.4.0 ounit.2.0.8 odoc.1.3.0" \ + CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" + +# BASE switch; CI_OPAM contains Coq's CI dependencies. +ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" + +# base switch +RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ + opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM + +# base+32bit switch +RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ + opam install $BASE_OPAM + +# EDGE switch +ENV COMPILER_EDGE="4.07.1" \ + COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ + BASE_OPAM_EDGE="dune-release.1.1.0" + +RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ + opam install $BASE_OPAM $BASE_OPAM_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 create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ + opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + +RUN opam clean -a -c diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat new file mode 100755 index 0000000000..918d289ae2 --- /dev/null +++ b/dev/ci/gitlab.bat @@ -0,0 +1,137 @@ +@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+ECHO "Start Time"
+TIME /T
+
+REM List currently used cygwin and target folders for debugging / maintenance purposes
+
+ECHO "Currently used cygwin folders"
+DIR C:\ci\cygwin*
+ECHO "Currently used target folders"
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
+
+if %ARCH% == 32 (
+ SET ARCHLONG=i686
+ SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+ SET ARCHLONG=x86_64
+ SET SETUP=setup-x86_64.exe
+)
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
+
+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 COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+IF "%WINDOWS%" == "enabled_all_addons" (
+ SET EXTRA_ADDONS=^
+ -addon=mathcomp ^
+ -addon=menhir ^
+ -addon=menhirlib ^
+ -addon=compcert ^
+ -addon=extlib ^
+ -addon=quickchick ^
+ -addon=coquelicot
+ REM addons with build issues
+ REM -addon=vst ^
+ REM -addon=aactactics ^
+) ELSE (
+ SET "EXTRA_ADDONS= "
+)
+
+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 ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
+ %EXTRA_ADDONS% ^
+ -make=N ^
+ -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+mkdir artifacts
+
+CALL :CopyLogFiles
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
+REM The open source archive is only required for release builds
+IF DEFINED WIN_CERTIFICATE_PATH (
+ 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+) ELSE (
+ REM In non release builds, create a dummy file
+ ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
+)
+
+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
+ )
+)
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+ ECHO Copy log files for artifact upload
+ MKDIR artifacts\buildlogs
+ COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
+ MKDIR artifacts\filelists
+ COPY %CYGROOT%\build\filelists\* artifacts\filelists
+ MKDIR artifacts\flagfiles
+ COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
+ GOTO :EOF
+
+:CleanupFolders
+ ECHO "Cleaning %CYGROOT%"
+ RMDIR /S /Q "%CYGROOT%"
+ ECHO "Cleaning %DESTCOQ%"
+ RMDIR /S /Q "%DESTCOQ%"
+ GOTO :EOF
+
+:MakeUniqueFolder
+ REM Create a uniquely named folder
+ REM This script is safe because folder creation is atomic - either we create it or fail
+ REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
+ REM %2 = name of the variable which receives the unique folder name
+ SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
+ MKDIR "%UNIQUENAME%"
+ IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
+ SET "%2=%UNIQUENAME%"
+ GOTO :EOF
+
+:ErrorCopyLogFilesAndExit
+ CALL :CopyLogFiles
+ REM fall through
+
+:ErrorExit
+ CALL :CleanupFolders
+ ECHO ERROR %0 failed
+ EXIT /b 1
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix new file mode 100644 index 0000000000..4c5cfd83da --- /dev/null +++ b/dev/ci/nix/CoLoR.nix @@ -0,0 +1,5 @@ +{ bignums }: + +{ + buildInputs = [ bignums ]; +} diff --git a/dev/ci/nix/CompCert.nix b/dev/ci/nix/CompCert.nix new file mode 100644 index 0000000000..db1721e5f5 --- /dev/null +++ b/dev/ci/nix/CompCert.nix @@ -0,0 +1,7 @@ +{ ocamlPackages }: + +{ + buildInputs = with ocamlPackages; [ ocaml findlib menhir ]; + configure = "./configure -ignore-coq-version x86_64-linux"; + make = "make all check-proof"; +} diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix new file mode 100644 index 0000000000..18c7750279 --- /dev/null +++ b/dev/ci/nix/Corn.nix @@ -0,0 +1,5 @@ +{ bignums, math-classes }: + +{ + buildInputs = [ bignums math-classes ]; +} diff --git a/dev/ci/nix/Elpi.nix b/dev/ci/nix/Elpi.nix new file mode 100644 index 0000000000..0a6ed20295 --- /dev/null +++ b/dev/ci/nix/Elpi.nix @@ -0,0 +1,4 @@ +{ ocamlPackages }: +{ + buildInputs = with ocamlPackages; [ ocaml findlib elpi ]; +} diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix new file mode 100644 index 0000000000..a86fb2c44a --- /dev/null +++ b/dev/ci/nix/GeoCoq.nix @@ -0,0 +1,5 @@ +{ mathcomp }: +{ + buildInputs = [ mathcomp ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/HoTT.nix b/dev/ci/nix/HoTT.nix new file mode 100644 index 0000000000..dea0aeeb55 --- /dev/null +++ b/dev/ci/nix/HoTT.nix @@ -0,0 +1,6 @@ +{ autoconf, automake }: +{ + buildInputs = [ autoconf automake ]; + configure = "./autogen.sh && ./configure"; + make = "make all validate"; +} diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md new file mode 100644 index 0000000000..1685b084e9 --- /dev/null +++ b/dev/ci/nix/README.md @@ -0,0 +1,19 @@ +# Working on third-party developments with *this* version of Coq + +Aim: getting an environment suitable for working on a third-party development +using the current version of Coq (i.e., built from the current state of this +repository). + +Dive into such an environment, for the project `example` by running, from the +root of this repository: + + ./dev/ci/nix/shell example + +This will build Coq and the other dependencies of the `example` project, then +open a shell with all these dependencies available (e.g., `coqtop` is in path). + +Additionally, three environment variables are set, to abstract over the +build-system of that project: `configure`, `make`, and `clean`. Therefore, after +changing the working directory to the root of the sources of that project, the +contents of these variables can be evaluated to respectively set-up, build, and +clean the project. diff --git a/dev/ci/nix/VST.nix b/dev/ci/nix/VST.nix new file mode 100644 index 0000000000..3e2629a0b6 --- /dev/null +++ b/dev/ci/nix/VST.nix @@ -0,0 +1,6 @@ +{}: + +rec { + make = "make IGNORECOQVERSION=true"; + clean = "${make} clean"; +} diff --git a/dev/ci/nix/bedrock2.nix b/dev/ci/nix/bedrock2.nix new file mode 100644 index 0000000000..552d9297e2 --- /dev/null +++ b/dev/ci/nix/bedrock2.nix @@ -0,0 +1,5 @@ +{}: +{ + configure = "git submodule update --init --recursive"; + clean = "(cd deps/bbv && make clean); (cd deps/riscv-coq && make clean); (cd compiler && make clean); (cd bedrock2 && make clean)"; +} diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix new file mode 100644 index 0000000000..1d931c858e --- /dev/null +++ b/dev/ci/nix/bignums.nix @@ -0,0 +1,5 @@ +{ ocamlPackages }: + +{ + buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ]; +} diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix new file mode 100644 index 0000000000..ecd280e58d --- /dev/null +++ b/dev/ci/nix/coq.nix @@ -0,0 +1,9 @@ +{ stdenv, callPackage, branch, wd }: + +let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version = "8.9"; }; in + +coq.overrideAttrs (o: { + name = "coq-local-${branch}"; + src = fetchGit "${wd}"; + enableParallelBuilding = true; +}) diff --git a/dev/ci/nix/coq_dpdgraph.nix b/dev/ci/nix/coq_dpdgraph.nix new file mode 100644 index 0000000000..611e2fcca5 --- /dev/null +++ b/dev/ci/nix/coq_dpdgraph.nix @@ -0,0 +1,7 @@ +{ autoconf, ocamlPackages }: + +{ + buildInputs = [ autoconf ] ++ (with ocamlPackages; [ ocaml findlib camlp5 ocamlgraph ]); + configure = "autoconf && ./configure"; + make = "make all test-suite"; +} diff --git a/dev/ci/nix/cross_crypto.nix b/dev/ci/nix/cross_crypto.nix new file mode 100644 index 0000000000..98f74f9474 --- /dev/null +++ b/dev/ci/nix/cross_crypto.nix @@ -0,0 +1,5 @@ +{}: +{ + configure = "git submodule update --init --recursive"; + clean = "make cleanall"; +} diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix new file mode 100644 index 0000000000..4acfae48e4 --- /dev/null +++ b/dev/ci/nix/default.nix @@ -0,0 +1,72 @@ +{ pkgs ? import <nixpkgs> {} +, branch +, wd +, project ? "xyz" +, bn ? "release" +}: + +with pkgs; + +# Coq from this directory +let coq = callPackage ./coq.nix { inherit branch wd; }; in + +# Third-party libraries, built with this Coq +let coqPackages = mkCoqPackages coq; in +let mathcomp = coqPackages.mathcomp.overrideAttrs (o: { + name = "coq-git-mathcomp-git"; + src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz; + }); in +let bignums = coqPackages.bignums.overrideAttrs (o: + if bn == "release" then {} else + if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else + { src = fetchTarball bn; } + ); in +let coqprime = coqPackages.coqprime.override { inherit coq bignums; }; in +let math-classes = + (coqPackages.math-classes.override { inherit coq bignums; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz"; + }); in + +let unicoq = callPackage ./unicoq.nix { inherit coq; }; in + +let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in + +# Environments for building CI libraries with this Coq +let projects = { + bedrock2 = callPackage ./bedrock2.nix {}; + bignums = callPackage ./bignums.nix {}; + CoLoR = callPackage ./CoLoR.nix {}; + CompCert = callPackage ./CompCert.nix {}; + coq_dpdgraph = callPackage ./coq_dpdgraph.nix {}; + Corn = callPackage ./Corn.nix {}; + cross_crypto = callPackage ./cross_crypto.nix {}; + Elpi = callPackage ./Elpi.nix {}; + fiat_crypto = callPackage ./fiat_crypto.nix {}; + fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; + flocq = callPackage ./flocq.nix {}; + GeoCoq = callPackage ./GeoCoq.nix {}; + HoTT = callPackage ./HoTT.nix {}; + math_classes = callPackage ./math_classes.nix {}; + mathcomp = {}; + mtac2 = callPackage ./mtac2.nix {}; + oddorder = callPackage ./oddorder.nix {}; + VST = callPackage ./VST.nix {}; +}; in + +if !builtins.hasAttr project projects +then throw "Unknown project “${project}”; choose from: ${pkgs.lib.concatStringsSep ", " (builtins.attrNames projects)}." +else + +let prj = projects."${project}"; in + +stdenv.mkDerivation { + name = "shell-for-${project}-in-${branch}"; + + buildInputs = [ coq ] ++ (prj.buildInputs or []); + + configure = prj.configure or "true"; + make = prj.make or "make"; + clean = prj.clean or "make clean"; + +} diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix new file mode 100644 index 0000000000..7b37e6e8e4 --- /dev/null +++ b/dev/ci/nix/fiat_crypto.nix @@ -0,0 +1,6 @@ +{ coqprime }: +{ + buildInputs = [ coqprime ]; + configure = "git submodule update --init --recursive && ulimit -s 32768"; + make = "make new-pipeline c-files"; +} diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix new file mode 100644 index 0000000000..3248665579 --- /dev/null +++ b/dev/ci/nix/fiat_crypto_legacy.nix @@ -0,0 +1,6 @@ +{}: + +{ + configure = "./etc/ci/remove_autogenerated.sh"; + make = "make print-old-pipeline-lite old-pipeline-lite lite-display"; +} diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix new file mode 100644 index 0000000000..e153043557 --- /dev/null +++ b/dev/ci/nix/flocq.nix @@ -0,0 +1,7 @@ +{ autoconf, automake }: + +{ + buildInputs = [ autoconf automake ]; + configure = "./autogen.sh && ./configure"; + make = "./remake"; +} diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix new file mode 100644 index 0000000000..b0fa2fe795 --- /dev/null +++ b/dev/ci/nix/math_classes.nix @@ -0,0 +1,6 @@ +{ bignums }: + +{ + buildInputs = [ bignums ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix new file mode 100644 index 0000000000..9a2353c5cf --- /dev/null +++ b/dev/ci/nix/mtac2.nix @@ -0,0 +1,5 @@ +{ coq, unicoq }: +{ + buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix new file mode 100644 index 0000000000..3b8fdbab51 --- /dev/null +++ b/dev/ci/nix/oddorder.nix @@ -0,0 +1,4 @@ +{ mathcomp }: +{ + buildInputs = [ mathcomp ]; +} diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell new file mode 100755 index 0000000000..2e4462ed40 --- /dev/null +++ b/dev/ci/nix/shell @@ -0,0 +1,20 @@ +#!/usr/bin/env sh + +## This file should be run from the root of the Coq source tree + +BRANCH=$(git rev-parse --abbrev-ref HEAD) +echo "Branch: $BRANCH in $PWD" + +if [ "$#" -ne 1 ]; then + PROJECT="" +else + PROJECT="--argstr project $1" +fi + +if [ "$BN" ]; then + BN="--argstr bn ${BN}" +else + BN="" +fi + +nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq.nix new file mode 100644 index 0000000000..093c262cde --- /dev/null +++ b/dev/ci/nix/unicoq.nix @@ -0,0 +1,11 @@ +{ stdenv, coq }: + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-unicoq-0.0-git"; + src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz; + + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); + + configurePhase = "coq_makefile -f Make -o Makefile"; + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; +} diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh deleted file mode 100644 index 7716bcb59a..0000000000 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ /dev/null @@ -1,4 +0,0 @@ -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 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/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/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/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh new file mode 100644 index 0000000000..b05d02c5be --- /dev/null +++ b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh @@ -0,0 +1,14 @@ +_OVERLAY_BRANCH=clean-transp-state + +if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="$_OVERLAY_BRANCH" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + + equations_CI_REF="$_OVERLAY_BRANCH" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + mtac2_CI_REF="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh new file mode 100644 index 0000000000..482792d7cd --- /dev/null +++ b/dev/ci/user-overlays/08850-poly-local-univs.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then + formal_topology_CI_REF=poly-local-univs + formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology + + paramcoq_CI_REF=poly-local-univs + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh new file mode 100644 index 0000000000..17eb5fffae --- /dev/null +++ b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then + + Equations_CI_REF=program-hook-obligation-subst + Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh new file mode 100644 index 0000000000..08112d3054 --- /dev/null +++ b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then + + aactactics_CI_REF=ltac+use_atts_in_ast + aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics + + coqhammer_CI_REF=ltac+use_atts_in_ast + coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer + + Equations_CI_REF=ltac+use_atts_in_ast + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=ltac+use_atts_in_ast + mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh new file mode 100644 index 0000000000..1c5157ba12 --- /dev/null +++ b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then + + quickchick_CI_REF=lib+better_boot_coqproject + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh new file mode 100644 index 0000000000..e74e53fa40 --- /dev/null +++ b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8933" ] || [ "$CI_BRANCH" = "solve-remaining-evars-initial-arg" ]; then + plugin_tutorial_CI_REF=solve-remaining-evars-initial-arg + plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials +fi diff --git a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh new file mode 100644 index 0000000000..d7130cc67a --- /dev/null +++ b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then + + elpi_CI_REF=use_coq_gramlib + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh new file mode 100644 index 0000000000..c8bea0c868 --- /dev/null +++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then + + equations_CI_REF=legacy_proof_eng_clean + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh new file mode 100644 index 0000000000..61ffa4a197 --- /dev/null +++ b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then + + ltac2_CI_REF=vernac+move_extend_ast + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + +fi diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh new file mode 100644 index 0000000000..14e7c0d7f0 --- /dev/null +++ b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then + + equations_CI_REF=camlp5-safe-api-strikes-back + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + ltac2_CI_REF=camlp5-safe-api-strikes-back + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9f0377ceea..7fb73e447d 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -1,16 +1,43 @@ # 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 / 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. + +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 + mathcomp_CI_REF=ssr-merge + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp 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)) + +### Branching conventions + +We suggest you use the convention of identical branch names for the +Coq branch and the CI project branch used in the overlay. For example, +if your Coq PR is coming from the branch `more_efficient_tc`, and that +breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch +named `more_efficient_tc`. |