diff options
Diffstat (limited to 'dev/ci')
84 files changed, 1024 insertions, 458 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md new file mode 100644 index 0000000000..98ea594366 --- /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. 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. + +- Azure Pipelines is used to test the compilation of Coq and run the + test-suite on Windows and on macOS. It is expected to be used to build + macOS and Windows packages eventually. + +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 7853866f62..afbfab3ac6 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -6,199 +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. - -- 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. - -### 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. - - -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. - -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 / - camlp5, 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: - -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. - -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=doc:refman - + 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). +*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.bat b/dev/ci/appveyor.bat deleted file mode 100644 index 85a71baf7f..0000000000 --- a/dev/ci/appveyor.bat +++ /dev/null @@ -1,42 +0,0 @@ -REM This script either runs the test suite with OPAM (if USEOPAM is true) or -REM builds the Coq binary packages for windows (if USEOPAM is false). - -if %ARCH% == 32 ( - SET ARCHLONG=i686 - SET CYGROOT=C:\cygwin - SET SETUP=setup-x86.exe -) - -if %ARCH% == 64 ( - SET ARCHLONG=x86_64 - SET CYGROOT=C:\cygwin64 - SET SETUP=setup-x86_64.exe -) - -SET CYGCACHE=%CYGROOT%\var\cache\setup -SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/% -SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/% -SET DESTCOQ=C:\coq%ARCH%_inst -SET COQREGTESTING=Y - -if %USEOPAM% == false ( - call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ - -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^ - -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ - -addon=bignums -make=N ^ - -setup %CYGROOT%\%SETUP% || GOTO ErrorExit - copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit - 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit -) - -if %USEOPAM% == true ( - %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^ - -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time - %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit -) - -GOTO :EOF - -:ErrorExit - ECHO ERROR %0 failed - EXIT /b 1 diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index d2176e326c..f26e0904bc 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -2,14 +2,16 @@ set -e -x -APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c +APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c +NJOBS=2 -wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz +wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O 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 $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH -eval "$(opam config env)" -opam install -y num ocamlfind camlp5 ounit +opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing +eval "$(opam env)" +opam install -j $NJOBS -y num ocamlfind ounit -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate +# Full regular Coq Build +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh new file mode 100755 index 0000000000..04c7d5db91 --- /dev/null +++ b/dev/ci/azure-build.sh @@ -0,0 +1,7 @@ +#!/bin/bash + +set -e -x + +cd $(dirname $0)/../.. + +make -f Makefile.dune coq coqide-server diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh new file mode 100755 index 0000000000..9448a03f4f --- /dev/null +++ b/dev/ci/azure-opam.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +set -e -x + +OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c + +wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz +tar -xf opam64.tar.xz +bash opam64/install.sh + +opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing +eval "$(opam env)" +opam install -y num ocamlfind dune ounit diff --git a/dev/ci/azure-test.sh b/dev/ci/azure-test.sh new file mode 100755 index 0000000000..80a3d2e083 --- /dev/null +++ b/dev/ci/azure-test.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +set -e -x + +#NB: if we make test-suite from the main makefile we get environment +#too large for exec error +cd $(dirname $0)/../../ +make -f Makefile.dune test-suite diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh deleted file mode 100755 index 896a0ddf66..0000000000 --- a/dev/ci/ci-aac-tactics.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download aactactics - -( cd "${CI_BUILD_DIR}/aactactics" && make && make install ) 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 50d4d21637..62335ea5d0 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -13,6 +13,10 @@ : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" : "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" +: "${fourcolor_CI_REF:=master}" +: "${fourcolor_CI_GITURL:=https://github.com/math-comp/fourcolor}" +: "${fourcolor_CI_ARCHIVEURL:=${fourcolor_CI_GITURL}/archive}" + : "${oddorder_CI_REF:=master}" : "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" : "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}" @@ -20,9 +24,9 @@ ######################################################################## # UniMath ######################################################################## -: "${UniMath_CI_REF:=master}" -: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" -: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}" +: "${unimath_CI_REF:=master}" +: "${unimath_CI_GITURL:=https://github.com/UniMath/UniMath}" +: "${unimath_CI_ARCHIVEURL:=${unimath_CI_GITURL}/archive}" ######################################################################## # Unicoq + Mtac2 @@ -31,7 +35,7 @@ : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" -: "${mtac2_CI_REF:=master-sync}" +: "${mtac2_CI_REF:=master}" : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" : "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" @@ -70,6 +74,13 @@ : "${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_REF:=master}" @@ -106,16 +117,16 @@ ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_REF:=master}" -: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" -: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" +: "${compcert_CI_REF:=master}" +: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}" +: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -: "${VST_CI_REF:=master}" -: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" -: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" +: "${vst_CI_REF:=master}" +: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}" ######################################################################## # cross-crypto @@ -139,14 +150,14 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# formal-topology +# fiat_crypto_legacy ######################################################################## -: "${formal_topology_CI_REF:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" -: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" ######################################################################## -# coq-dpdgraph +# coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" @@ -155,9 +166,9 @@ ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_REF:=master}" -: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" -: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" +: "${color_CI_REF:=master}" +: "${color_CI_GITURL:=https://github.com/fblanqui/color}" +: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" ######################################################################## # SF @@ -189,16 +200,16 @@ ######################################################################## # Equations ######################################################################## -: "${Equations_CI_REF:=master}" -: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" -: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" +: "${equations_CI_REF:=master}" +: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" +: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_REF:=coq-master}" -: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" -: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" +: "${elpi_CI_REF:=coq-master}" +: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm @@ -208,13 +219,6 @@ : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## -# pidetop -######################################################################## -: "${pidetop_CI_REF:=v8.9}" -: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" -: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" - -######################################################################## # ext-lib ######################################################################## : "${ext_lib_CI_REF:=master}" @@ -224,7 +228,7 @@ ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=master}" +: "${simple_io_CI_REF:=dev}" : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" @@ -236,13 +240,6 @@ : "${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}" @@ -250,8 +247,52 @@ : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## -# aac-tactics +# 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}" + +######################################################################## +# relation-algebra +######################################################################## +: "${relation_algebra_CI_REF:=master}" +: "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" +: "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" + +######################################################################## +# StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft +######################################################################## +: "${struct_tact_CI_REF:=master}" +: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}" +: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}" + +: "${inf_seq_ext_CI_REF:=master}" +: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}" +: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}" + +: "${cheerios_CI_REF:=master}" +: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" +: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" + +: "${verdi_CI_REF:=master}" +: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" +: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" + +: "${verdi_raft_CI_REF:=master}" +: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" +: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" + +######################################################################## +# stdlib2 ######################################################################## -: "${aactactics_CI_REF:=master}" -: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" -: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}" +: "${stdlib2_CI_REF:=master}" +: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}" +: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 5205946261..2d242d80a4 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` ) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index dc696f69d9..a0094b1006 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CoLoR +git_download color -( cd "${CI_BUILD_DIR}/CoLoR" && make ) +( cd "${CI_BUILD_DIR}/color" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7a450d0d48..b4d2a9ca4e 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -46,8 +46,11 @@ for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done + +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; @@ -59,27 +62,30 @@ git_download() { local PROJECT=$1 local DEST="$CI_BUILD_DIR/$PROJECT" + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" 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" + local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1) + if [[ "$COMMIT" == "" ]]; then + # $REF must have been a tag or hash, not a branch + COMMIT="$REF" + fi + wget "$ARCHIVEURL/$COMMIT.tar.gz" + tar xvfz "$COMMIT.tar.gz" --strip-components=1 + rm -f "$COMMIT.tar.gz" fi } diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 01c35ceb4a..59a85e4726 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download CompCert +git_download compcert -( cd "${CI_BUILD_DIR}/CompCert" && \ +( cd "${CI_BUILD_DIR}/compcert" && \ ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq_dpdgraph.sh index 2373ea6c62..2373ea6c62 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq_dpdgraph.sh 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-elpi.sh b/dev/ci/ci-elpi.sh index 9b4a06fd5b..d60bf34ba2 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Elpi +git_download elpi -( cd "${CI_BUILD_DIR}/Elpi" && 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 998d50faa7..b58a794da2 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Equations +git_download equations -( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \ +( 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-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 6bf3138346..2af4b58201 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" FORCE_GIT=1 -git_download fiat_crypto +git_download fiat_crypto_legacy 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 && \ +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && 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 7e8013be9b..bba17314f7 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -10,5 +10,9 @@ git_download fiat_crypto # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +fiat_crypto_CI_TARGETS1="c-files printlite lite" +fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" + ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ - ulimit -s 32768 && make new-pipeline c-files ) + ulimit -s 32768 && \ + make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh index ac74ebf667..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat_parsers.sh diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh deleted file mode 100755 index 8be5a06ed2..0000000000 --- a/dev/ci/ci-formal-topology.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download formal_topology - -( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 7eeeb09372..c8e6fe690f 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download HoTT -( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index a74f9fa4d3..cae127ee7b 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -8,6 +8,10 @@ git_download mathcomp ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install ) +git_download fourcolor + +( cd "${CI_BUILD_DIR}/fourcolor" && make && make install ) + git_download oddorder ( cd "${CI_BUILD_DIR}/oddorder" && make ) diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh new file mode 100755 index 0000000000..d2e0ee89bf --- /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 && cd test-suite && make examples) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh deleted file mode 100755 index 1a9a26843c..0000000000 --- a/dev/ci/ci-pidetop.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download pidetop - -# Travis / Gitlab have different filesystem layout due to use of -# `-local`. We need to improve this divergence but if we use Dune this -# "local" oddity goes away automatically so not bothering... -if [ -d "$COQBIN/../lib/coq" ]; then - COQLIB="$COQBIN/../lib/coq/" -else - COQLIB="$COQBIN/../" -fi - -( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install ) - -echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-plugin-tutorial.sh b/dev/ci/ci-plugin-tutorial.sh deleted file mode 100755 index 6c26a71a21..0000000000 --- a/dev/ci/ci-plugin-tutorial.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/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-relation-algebra.sh b/dev/ci/ci-relation-algebra.sh new file mode 100755 index 0000000000..84bed5bdfe --- /dev/null +++ b/dev/ci/ci-relation-algebra.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download relation_algebra + +( cd "${CI_BUILD_DIR}/relation_algebra" && make && make install ) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 58bbb7229f..60436e672c 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -8,11 +8,6 @@ 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 ) - +( cd lf && make clean && make ) +( cd plf && make clean && make ) ( cd vfa && make clean && make ) diff --git a/dev/ci/ci-stdlib2.sh b/dev/ci/ci-stdlib2.sh new file mode 100755 index 0000000000..ec1c180d7d --- /dev/null +++ b/dev/ci/ci-stdlib2.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download stdlib2 + +( cd "${CI_BUILD_DIR}/stdlib2/src" && ./bootstrap && make && make install) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index a7644fee23..704e278a4b 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download UniMath +git_download unimath -( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no ) +( cd "${CI_BUILD_DIR}/unimath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh new file mode 100755 index 0000000000..3bcd52c464 --- /dev/null +++ b/dev/ci/ci-verdi-raft.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download struct_tact + +( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install ) + +git_download inf_seq_ext + +( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install ) + +git_download cheerios + +( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install ) + +git_download verdi + +( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install ) + +git_download verdi_raft + +( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 0fec19205a..169d1a41db 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download VST +git_download vst -( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) +( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh index 12a70176c2..9ca8f76054 100755 --- a/dev/ci/ci-wrapper.sh +++ b/dev/ci/ci-wrapper.sh @@ -6,13 +6,6 @@ set -eo pipefail -function travis_fold { - if [ -n "${TRAVIS}" ]; - then - echo "travis_fold:$1:$2" - fi -} - CI_NAME="$1" CI_SCRIPT="ci-${CI_NAME}.sh" @@ -22,6 +15,5 @@ cd "${DIR}/../.." export TIMED=1 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log -travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' +echo 'Aggregating timing log...' python ./tools/make-one-time-file.py time-of-build.log -travis_fold 'end' 'coq.test.timing' diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f257c62dd3..e553cbed1b 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-04-V2" +# CACHEKEY: "bionic_coq-V2019-03-12-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -10,7 +10,7 @@ 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 \ + libgtksourceview-3.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 \ @@ -22,7 +22,7 @@ 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 +RUN wget https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam # Basic OPAM setup ENV NJOBS="2" \ @@ -37,33 +37,31 @@ 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.2.1 ounit.2.0.8 odoc.1.2.0" \ - CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \ + CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="7.03" \ - COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" +ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" + +# Must add this to COQIDE_OPAM{,_EDGE} when we update the opam +# packages "lablgtk3-gtksourceview3" # base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ - opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM + opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM # base+32bit switch RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install $BASE_OPAM camlp5.$CAMLP5_VER + opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.07.0" \ - CAMLP5_VER_EDGE="7.06" \ - COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="dune-release.0.3.0" - -RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE +ENV COMPILER_EDGE="4.07.1" \ + COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" \ + BASE_OPAM_EDGE="dune-release.1.1.0" # 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 camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + 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 index 918d289ae2..5f819f31f9 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -26,12 +26,12 @@ if %ARCH% == 64 ( SET CYGROOT=C:\ci\cygwin%ARCH%
SET DESTCOQ=C:\ci\coq%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
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
@@ -39,16 +39,19 @@ SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\ IF "%WINDOWS%" == "enabled_all_addons" (
SET EXTRA_ADDONS=^
+ -addon=bignums ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
-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 ^
+ -addon=coquelicot ^
+ -addon=vst ^
+ -addon=aactactics
) ELSE (
SET "EXTRA_ADDONS= "
)
@@ -56,10 +59,6 @@ IF "%WINDOWS%" == "enabled_all_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
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix new file mode 100644 index 0000000000..3fcf177aec --- /dev/null +++ b/dev/ci/nix/CoLoR.nix @@ -0,0 +1,5 @@ +{ bignums }: + +{ + coqBuildInputs = [ 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..0d22a6b91b --- /dev/null +++ b/dev/ci/nix/Corn.nix @@ -0,0 +1,5 @@ +{ bignums, math-classes }: + +{ + coqBuildInputs = [ 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..45d688285e --- /dev/null +++ b/dev/ci/nix/GeoCoq.nix @@ -0,0 +1,5 @@ +{ mathcomp }: +{ + coqBuildInputs = [ 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..6f32abef95 --- /dev/null +++ b/dev/ci/nix/README.md @@ -0,0 +1,26 @@ +# 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. + +## Variant: nocoq + +The dependencies of the third-party developments are split into `buildInputs` +and `coqBuildInputs`. The second list gathers the Coq libraries. In case you +only want the non-coq dependencies (because you want to use Coq from your `PATH`), +set the environment variable `NOCOQ` to some non-empty value. 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..b610790f61 --- /dev/null +++ b/dev/ci/nix/coq.nix @@ -0,0 +1,8 @@ +{ 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}"; +}) 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..17070e66ee --- /dev/null +++ b/dev/ci/nix/default.nix @@ -0,0 +1,115 @@ +{ pkgs ? import ../../nixpkgs.nix {} +, branch +, wd +, project ? "xyz" +, withCoq ? true +, bn ? "master" +}: + +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 ssreflect = coqPackages.ssreflect.overrideAttrs (o: { + inherit (mathcomp) src; + }); in + +let coq-ext-lib = coqPackages.coq-ext-lib.overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-ext-lib/coq-ext-lib/tarball/master"; + }); in + +let simple-io = + (coqPackages.simple-io.override { inherit coq-ext-lib; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/Lysxia/coq-simple-io/tarball/master"; + }); 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 corn = (coqPackages.corn.override { inherit coq bignums math-classes; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz"; + }); in + +let stdpp = coqPackages.stdpp.overrideAttrs (o: { + src = fetchTarball "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/master/stdpp-master.tar.bz2"; + }); in + +let iris = (coqPackages.iris.override { inherit coq stdpp; }) + .overrideAttrs (o: { + src = fetchTarball "https://gitlab.mpi-sws.org/iris/iris/-/archive/master/iris-master.tar.bz2"; + propagatedBuildInputs = [ stdpp ]; + }); in + +let unicoq = callPackage ./unicoq { inherit coq; }; in + +let callPackage = newScope { inherit coq + bignums coq-ext-lib coqprime corn iris math-classes + mathcomp simple-io ssreflect stdpp 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 {}; + formal-topology = callPackage ./formal-topology.nix {}; + GeoCoq = callPackage ./GeoCoq.nix {}; + HoTT = callPackage ./HoTT.nix {}; + iris = callPackage ./iris.nix {}; + lambda-rust = callPackage ./lambda-rust.nix {}; + math_classes = callPackage ./math_classes.nix {}; + mathcomp = {}; + mtac2 = callPackage ./mtac2.nix {}; + oddorder = callPackage ./oddorder.nix {}; + quickchick = callPackage ./quickchick.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 + +let inherit (stdenv.lib) optional optionals; in + +stdenv.mkDerivation { + name = "shell-for-${project}-in-${branch}"; + + buildInputs = + optional withCoq coq + ++ (prj.buildInputs or []) + ++ optionals withCoq (prj.coqBuildInputs 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..0f0ee91387 --- /dev/null +++ b/dev/ci/nix/fiat_crypto.nix @@ -0,0 +1,6 @@ +{ coqprime }: +{ + coqBuildInputs = [ 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/formal-topology.nix b/dev/ci/nix/formal-topology.nix new file mode 100644 index 0000000000..53b9b1182b --- /dev/null +++ b/dev/ci/nix/formal-topology.nix @@ -0,0 +1,4 @@ +{ corn }: +{ + coqBuildInputs = [ corn ]; +} diff --git a/dev/ci/nix/iris.nix b/dev/ci/nix/iris.nix new file mode 100644 index 0000000000..b55cccc7c6 --- /dev/null +++ b/dev/ci/nix/iris.nix @@ -0,0 +1,4 @@ +{ stdpp }: +{ + coqBuildInputs = [ stdpp ]; +} diff --git a/dev/ci/nix/lambda-rust.nix b/dev/ci/nix/lambda-rust.nix new file mode 100644 index 0000000000..0d07c3028a --- /dev/null +++ b/dev/ci/nix/lambda-rust.nix @@ -0,0 +1,4 @@ +{ iris }: +{ + coqBuildInputs = [ iris ]; +} diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix new file mode 100644 index 0000000000..8edc3c8358 --- /dev/null +++ b/dev/ci/nix/math_classes.nix @@ -0,0 +1,6 @@ +{ bignums }: + +{ + coqBuildInputs = [ bignums ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix new file mode 100644 index 0000000000..4acc326c02 --- /dev/null +++ b/dev/ci/nix/mtac2.nix @@ -0,0 +1,6 @@ +{ coq, unicoq }: +{ + buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ]; + coqBuildInputs = [ unicoq ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix new file mode 100644 index 0000000000..2341bb3173 --- /dev/null +++ b/dev/ci/nix/oddorder.nix @@ -0,0 +1,4 @@ +{ mathcomp }: +{ + coqBuildInputs = [ mathcomp ]; +} diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix new file mode 100644 index 0000000000..b90f1e4f88 --- /dev/null +++ b/dev/ci/nix/quickchick.nix @@ -0,0 +1,5 @@ +{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }: +{ + buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ]; + coqBuildInputs = [ ssreflect simple-io ]; +} diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell new file mode 100755 index 0000000000..a5f8ee8f54 --- /dev/null +++ b/dev/ci/nix/shell @@ -0,0 +1,26 @@ +#!/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 + +if [ "$NOCOQ" ]; then + NOCOQ="--arg withCoq false" +else + NOCOQ="" +fi + +nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN $NOCOQ diff --git a/dev/ci/nix/unicoq/default.nix b/dev/ci/nix/unicoq/default.nix new file mode 100644 index 0000000000..54c67ac0fd --- /dev/null +++ b/dev/ci/nix/unicoq/default.nix @@ -0,0 +1,26 @@ +{ stdenv, writeText, coq }: + +let META = writeText "META" '' + archive(native) = "unicoq.cmxa" + plugin(native) = "unicoq.cmxs" +''; in + + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-unicoq-0.0-git"; + src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz; + + patches = [ ./unicoq-num.patch ]; + + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); + + configurePhase = "coq_makefile -f Make -o Makefile"; + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + + postInstall = '' + cp ${META} META + install -d $OCAMLFIND_DESTDIR + ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/ + install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq + ''; +} diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch new file mode 100644 index 0000000000..6d96d94dfc --- /dev/null +++ b/dev/ci/nix/unicoq/unicoq-num.patch @@ -0,0 +1,44 @@ +commit f29bc64ee3d8b36758d17e1f5d50812e0c93063b +Author: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> +Date: Thu Nov 29 08:59:22 2018 +0000 + + Make explicit dependency to num + +diff --git a/Make b/Make +index 550dc6a..8aa1309 100644 +--- a/Make ++++ b/Make +@@ -9,7 +9,7 @@ src/logger.ml + src/munify.mli + src/munify.ml + src/unitactics.mlg +-src/unicoq.mllib ++src/unicoq.mlpack + theories/Unicoq.v + test-suite/munifytest.v + test-suite/microtests.v +diff --git a/Makefile.local b/Makefile.local +new file mode 100644 +index 0000000..88be365 +--- /dev/null ++++ b/Makefile.local +@@ -0,0 +1 @@ ++CAMLPKGS += -package num +diff --git a/src/unicoq.mllib b/src/unicoq.mllib +deleted file mode 100644 +index 2b84e2d..0000000 +--- a/src/unicoq.mllib ++++ /dev/null +@@ -1,3 +0,0 @@ +-Logger +-Munify +-Unitactics +diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack +new file mode 100644 +index 0000000..2b84e2d +--- /dev/null ++++ b/src/unicoq.mlpack +@@ -0,0 +1,3 @@ ++Logger ++Munify ++Unitactics 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 d812df3ec0..0000000000 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_REF=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp -fi diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh deleted file mode 100644 index 575df07425..0000000000 --- a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=pure-sharing-flag - -if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - mtac2_CI_BRANCH="$_OVERLAY_BRANCH" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - -fi diff --git a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh deleted file mode 100644 index 019cb8054d..0000000000 --- a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then - cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification - cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto -fi diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh deleted file mode 100644 index 3a6480a5a1..0000000000 --- a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then - - ltac2_CI_BRANCH=master+globenv-coq-pr7288 - ltac2_CI_GITURL=https://github.com/herbelin/ltac2 - -fi diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh new file mode 100644 index 0000000000..2b4c1489ad --- /dev/null +++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh @@ -0,0 +1,13 @@ +_OVERLAY_BRANCH=ho-matching-occ-sel + +if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="PR7819-overlay" + + mtac2_CI_REF="PR7819-overlay" + mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 + + equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + equations_CI_REF="PR7819-overlay" + +fi diff --git a/dev/ci/user-overlays/08456-fix-6764.sh b/dev/ci/user-overlays/08456-fix-6764.sh deleted file mode 100644 index 3b951d9c07..0000000000 --- a/dev/ci/user-overlays/08456-fix-6764.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8456" ] || [ "$CI_BRANCH" = "fix-6764" ]; then - Elpi_CI_REF=overlay/8456 -fi diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh deleted file mode 100644 index c08f44fc50..0000000000 --- a/dev/ci/user-overlays/08552-gares-elpi-11.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then - Elpi_CI_REF=coq-master-elpi-1.1 -fi diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh deleted file mode 100644 index 484ad8f9e6..0000000000 --- a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh +++ /dev/null @@ -1,11 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then - - ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env - ltac2_CI_REF=master+fix-pr8554-change-takes-env - ltac2_CI_GITURL=https://github.com/herbelin/ltac2 - - Equations_CI_BRANCH=master+fix-pr8554-change-takes-env - Equations_CI_REF=master+fix-pr8554-change-takes-env - Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh deleted file mode 100644 index 41c2ad6fef..0000000000 --- a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then - - ltac2_CI_REF=rm-section-path - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - Equations_CI_REF=rm-section-path - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh new file mode 100644 index 0000000000..81e18226ed --- /dev/null +++ b/dev/ci/user-overlays/08817-sprop.sh @@ -0,0 +1,34 @@ +if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then + aac_tactics_CI_REF=sprop + aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics + + coq_dpdgraph_CI_REF=sprop + coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph + + coqhammer_CI_REF=sprop + coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer + + elpi_CI_REF=sprop + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sprop + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + ltac2_CI_REF=sprop + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + unicoq_CI_REF=sprop + unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq + + mtac2_CI_REF=sprop + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sprop + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + + quickchick_CI_REF=sprop + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + + relation_algebra_CI_REF=sprop + relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra +fi diff --git a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh new file mode 100644 index 0000000000..c09d1b8929 --- /dev/null +++ b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh @@ -0,0 +1,30 @@ +if [ "$CI_PULL_REQUEST" = "9129" ] || [ "$CI_BRANCH" = "proof+no_global_partial" ]; then + + aac_tactics_CI_REF=proof+no_global_partial + aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics + + # coqhammer_CI_REF=proof+no_global_partial + # coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer + + elpi_CI_REF=proof+no_global_partial + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + equations_CI_REF=proof+no_global_partial + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + ltac2_CI_REF=proof+no_global_partial + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + # unicoq_CI_REF=proof+no_global_partial + # unicoq_CI_GITURL=https://github.com/ejgallego/unicoq + + mtac2_CI_REF=proof+no_global_partial + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=proof+no_global_partial + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + quickchick_CI_REF=proof+no_global_partial + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh new file mode 100644 index 0000000000..23eb24c304 --- /dev/null +++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then + + ltac2_CI_REF=proofview+proof_info + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + fiat_parsers_CI_REF=proofview+proof_info + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + +fi diff --git a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh new file mode 100644 index 0000000000..1110157069 --- /dev/null +++ b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9389" ] || [ "$CI_BRANCH" = "set-implicits" ]; then + + equations_CI_REF=set-implicits + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=set-implicits + mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 + +fi diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh new file mode 100644 index 0000000000..cca85a2f68 --- /dev/null +++ b/dev/ci/user-overlays/09439-sep-variance.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then + elpi_CI_REF=sep-variance + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=sep-variance + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + mtac2_CI_REF=sep-variance + mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 + + paramcoq_CI_REF=sep-variance + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh new file mode 100644 index 0000000000..1af8b5430d --- /dev/null +++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then + + quickchick_CI_REF=context-constructor + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + + equations_CI_REF=context-constructor + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh new file mode 100644 index 0000000000..27ce9aca16 --- /dev/null +++ b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then + + equations_CI_REF=hooks_unify + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=hooks_unify + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=hooks_unify + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + +fi diff --git a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh new file mode 100644 index 0000000000..18a295cdbb --- /dev/null +++ b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9602" ] || [ "$CI_BRANCH" = "more-delta-in-termination-checking" ]; then + + equations_CI_REF=more-delta-in-termination-checking + equations_CI_GITURL=https://github.com/gares/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh new file mode 100644 index 0000000000..ccb3498764 --- /dev/null +++ b/dev/ci/user-overlays/09678-printed-by-env.sh @@ -0,0 +1,14 @@ + +if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then + elpi_CI_REF=printed-by-env + elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi + + equations_CI_REF=printed-by-env + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + + ltac2_CI_REF=printed-by-env + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + quickchick_CI_REF=printed-by-env + quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 68afe7ee4a..7fb73e447d 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -33,3 +33,11 @@ fi ``` (`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`. diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh deleted file mode 100644 index 76aa37d380..0000000000 --- a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh +++ /dev/null @@ -1,5 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then - HoTT_CI_REF=fix-for-numeral-notations - HoTT_CI_GITURL=https://github.com/JasonGross/HoTT - HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive -fi |