diff options
Diffstat (limited to 'dev')
56 files changed, 521 insertions, 445 deletions
diff --git a/dev/base_include b/dev/base_include index 0e12b57b36..48feeec147 100644 --- a/dev/base_include +++ b/dev/base_include @@ -8,6 +8,7 @@ #directory "toplevel";; #directory "library";; #directory "kernel";; +#directory "gramlib";; #directory "engine";; #directory "pretyping";; #directory "lib";; @@ -18,8 +19,6 @@ #directory "stm";; #directory "vernac";; -#directory "+camlp5";; (* Gramext is found in top_printers.ml *) - #use "top_printers.ml";; #use "vm_printers.ml";; @@ -135,7 +134,6 @@ open Pfedit open Proof open Proof_using open Proof_global -open Proof_type open Redexpr open Refiner open Tacmach diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 71207bb040..d0b5f4be47 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1076,7 +1076,7 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_camlp5 + # make_camlp5 } ##### OCAML EXTRA LIBRARIES ##### @@ -1386,7 +1386,7 @@ function make_coq { make_ocaml make_num make_findlib - make_camlp5 + # make_camlp5 make_lablgtk if case $COQ_VERSION in @@ -1645,7 +1645,7 @@ function make_addon_bignums { function make_addon_equations { installer_addon_dependency equations - if build_prep_overlay Equations; then + if build_prep_overlay equations; then installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" "" # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH 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 4709247549..afbfab3ac6 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -6,213 +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'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. - -- 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. - -### 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. - -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.sh b/dev/ci/appveyor.sh index 84fec71f7a..abeb039c0e 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -10,6 +10,6 @@ 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 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 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 3137576207..96bc5be7ff 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -113,16 +113,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 @@ -153,7 +153,7 @@ : "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## -# coq-dpdgraph +# coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" @@ -162,9 +162,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 @@ -196,16 +196,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 @@ -215,13 +215,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}" @@ -257,11 +250,11 @@ : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## -# aac-tactics +# aac_tactics ######################################################################## -: "${aactactics_CI_REF:=master}" -: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" -: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}" +: "${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 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..a5aa54144c 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; 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-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-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 index 6c26a71a21..6c26a71a21 100755 --- a/dev/ci/ci-plugin-tutorial.sh +++ b/dev/ci/ci-plugin_tutorial.sh 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/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 4ddb582414..3fc6dce4e5 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-30-V1" +# CACHEKEY: "bionic_coq-V2018-11-08-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -41,29 +41,27 @@ 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 CAMLP5_VER="7.03" \ - COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" +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 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.1" \ - CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \ 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 camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE + 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 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/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/unicoq.nix b/dev/ci/nix/unicoq.nix index f10afd5680..093c262cde 100644 --- a/dev/ci/nix/unicoq.nix +++ b/dev/ci/nix/unicoq.nix @@ -1,11 +1,8 @@ -{ stdenv, fetchzip, coq }: +{ stdenv, coq }: stdenv.mkDerivation { name = "coq${coq.coq-version}-unicoq-0.0-git"; - src = fetchzip { - url = "https://github.com/vbgl/unicoq/archive/8b33e37700e92bfd404bf8bf9fe03f1be8928d97.tar.gz"; - sha256 = "0s4z0wjxlp56ccgzxgk04z7skw90rdnz39v730ffkgrjl38rr9il"; - }; + src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz; buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); 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/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/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/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh deleted file mode 100755 index 4605255d5e..0000000000 --- a/dev/ci/user-overlays/08515-command-atts.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then - ltac2_CI_REF=command-atts - ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 - - Equations_CI_REF=command-atts - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - plugin_tutorial_CI_REF=command-atts - plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials -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/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh deleted file mode 100644 index 9d723dc7f2..0000000000 --- a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh +++ /dev/null @@ -1,11 +0,0 @@ -_OVERLAY_BRANCH=name-abstract-univ-context - -if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - Elpi_CI_REF="$_OVERLAY_BRANCH" - Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - Equations_CI_REF="$_OVERLAY_BRANCH" - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh deleted file mode 100644 index bd3e1bf7ff..0000000000 --- a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then - plugin_tutorial_CI_REF=pr8671-fix - plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials - -fi diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh deleted file mode 100644 index 98530c825a..0000000000 --- a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then - - Elpi_CI_REF=kernel-entries-cleanup - Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - Equations_CI_REF=kernel-entries-cleanup - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh deleted file mode 100644 index 81ed91f52b..0000000000 --- a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then - - Elpi_CI_REF=master+generalized-evar-printers-pr8688 - Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh deleted file mode 100644 index b3a9f67e00..0000000000 --- a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then - - # ltac2_CI_REF=rm-section-path - # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - plugin_tutorial_CI_REF=vernac+monify_hook - plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials - - Elpi_CI_REF=vernac+monify_hook - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - Equations_CI_REF=vernac+monify_hook - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh deleted file mode 100644 index 8ad8cba243..0000000000 --- a/dev/ci/user-overlays/08844-split-tactics.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then - Equations_CI_REF=split-tactics - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - ltac2_CI_REF=split-tactics - ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 - - fiat_parsers_CI_REF=split-tactics - fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat -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/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 diff --git a/dev/doc/README.md b/dev/doc/README.md index 223cf6286e..c764455aed 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -16,7 +16,6 @@ $ opam init --comp <latest-ocaml-version> ~/.bashrc and ~/.ocamlinit files. $ source ~/.bashrc -$ opam install camlp5 # needed if you want to build "coqide" target diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index c5ea88aaf6..3609171b82 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,7 +10,8 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +Dune >= 1.5.0 is recommended, see `dune-project` for the minimum +required version; type `dune build` to build the base Coq libraries. No call to `./configure` is needed. Dune will get confused if it finds leftovers of in-tree compilation, @@ -49,14 +50,25 @@ The default dune target is `dune build` (or `dune build @install`), which will scan all sources in the Coq tree and then build the whole project, creating an "install" overlay in `_build/install/default`. -You can build some other target by doing `dune build $TARGET`. +You can build some other target by doing `dune build $TARGET`, where +`$TARGET` can be a `.cmxa`, a binary, a file that Dune considers a +target, an alias, etc... In order to build a single package, you can do `dune build $PACKAGE.install`. +A very useful target is `dune build @check`, that will compile all the +ml files in quick mode. + Dune also provides targets for documentation, testing, and release builds, please see below. +## Documentation and test targets + +Coq's test-suite can be run with `dune runtest`. + +The documentation target is not implemented in Dune yet. + ## Developer shell You can create a developer shell with `dune utop $library`, where @@ -139,11 +151,6 @@ Note that due to https://github.com/ocaml/dune/issues/1401 , we must perform a full rebuild each time as otherwise Dune will remove the files. We hope to solve this in the future. -## Documentation and test targets - -The documentation and test suite targets for Coq are still not -implemented in Dune. - ## Planned and Advanced features Dune supports or will support extra functionality that may result very diff --git a/dev/doc/changes.md b/dev/doc/changes.md index b1fdfafd3a..acb0d80c18 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,5 +1,15 @@ ## Changes between Coq 8.9 and Coq 8.10 +### ML4 Pre Processing + +- Support for `.ml4` files, processed by camlp5 has been removed in + favor of `.mlg` files processed by `coqpp`. + + Porting is usually straightforward, and involves renaming the + `file.ml4` file to `file.mlg` and adding a few brackets. + + See "Transitioning away from Camlp5" below for update instructions. + ### ML API General deprecation @@ -19,6 +29,10 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 +- `Names.transparent_state` has been moved to its own module `TransparentState`. + This module gathers utility functions that used to be defined in several + places. + Coqlib: - Most functions from the `Coqlib` module have been deprecated in favor of diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 764d482957..e5e4f740bd 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -94,7 +94,7 @@ Tacexpr.glob_tactic_expr | | Tacinterp.eval_tactic (?) V -Proof_type.tactic +Proofview.V82.tac TODO: check with Hugo @@ -4,12 +4,13 @@ (synopsis "Coq's Debug Printers") (wrapped false) (modules :standard) + (optional) (libraries coq.toplevel coq.plugins.ltac)) (rule (targets dune-dbg) (deps dune-dbg.in - ../checker/main.bc + ../checker/coqchk.bc ../topbin/coqtop_byte_bin.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 3f3df23fe1..80ad0500e0 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,7 +3,7 @@ # Run in a proper install dune env. case $1 in checker) - exe=_build/default/checker/main.bc + exe=_build/default/checker/coqchk.bc ;; *) exe=_build/default/topbin/coqtop_byte_bin.bc diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index d330f517be..c1dcabb743 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -8,16 +8,16 @@ # here are some reasonable default values [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug -[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ - -I $CAMLP5LIB -I +threads \ + -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ + -I $COQTOP/gramlib__pack \ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh new file mode 100755 index 0000000000..41392be5d7 --- /dev/null +++ b/dev/tools/create_overlays.sh @@ -0,0 +1,78 @@ +#!/usr/bin/env bash + +# TODO: +# +# - Check if the branch already exists in the remote => checkout +# - Better error handling +# - Just checkout, don't build +# - Rebase functionality +# + +set -x +set -e +set -o pipefail + +# setup_contrib_git("_build_ci/fiat", "https://github.com/ejgallego/fiat-core.git") +setup_contrib_git() { + + local _DIR=$1 + local _GITURL=$2 + + ( cd $_DIR + git checkout -b $OVERLAY_BRANCH || true # allow the branch to exist already + git remote add $DEVELOPER_NAME $_GITURL || true # allow the remote to exist already + ) + +} + +if [ $# -lt 3 ]; then + echo "usage: $0 github_username pr_number contrib1 ... contribN" + exit 1 +fi + +set +x +. dev/ci/ci-basic-overlay.sh +set -x + +DEVELOPER_NAME=$1 +shift +PR_NUMBER=$1 +shift +OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD) +OVERLAY_FILE=$(mktemp overlay-XXXX) + +# Create the overlay file +printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then \n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" + +# We first try to build the contribs +while test $# -gt 0 +do + _CONTRIB_NAME=$1 + _CONTRIB_GITURL=${_CONTRIB_NAME}_CI_GITURL + _CONTRIB_GITURL=${!_CONTRIB_GITURL} + echo "Processing Contrib $_CONTRIB_NAME" + + # check _CONTRIB_GIT exists and it is of the from github... + + _CONTRIB_DIR=_build_ci/$_CONTRIB_NAME + + # extract the relevant part of the repository + _CONTRIB_GITSUFFIX=${_CONTRIB_GITURL#https://github.com/*/} + _CONTRIB_GITURL="https://github.com/$DEVELOPER_NAME/$_CONTRIB_GITSUFFIX" + _CONTRIB_GITPUSHURL="git@github.com:$DEVELOPER_NAME/${_CONTRIB_GITSUFFIX}.git" + + # This should work better: for example we should be able not to + # build but just to checkout. + make ci-$_CONTRIB_NAME || true + setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL + + echo " ${_CONTRIB_NAME}_CI_REF=$OVERLAY_BRANCH" >> $OVERLAY_FILE + echo " ${_CONTRIB_NAME}_CI_GITURL=$_CONTRIB_GITURL" >> $OVERLAY_FILE + echo "" >> $OVERLAY_FILE + shift +done + +# End the file; copy to overlays folder. +echo "fi" >> $OVERLAY_FILE +PR_NUMBER=$(printf '%05d' "$PR_NUMBER") +mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-${OVERLAY_BRANCH///}.sh diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 320ef6ed07..5fd8a3b7d9 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -202,9 +202,8 @@ info "merging" git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e # TODO: improve this check -if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then - warning "this PR may have overlays (sorry the check is not perfect)" - warning "if it has overlays please check the following:" +if ! git diff --quiet --diff-filter=A "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then + warning "this PR has overlays, please check the following:" warning "- each overlay has a corresponding open PR on the upstream repo" warning "- after merging please notify the upstream they can merge the PR" fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f94e9acb72..4287702b3a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -514,18 +514,18 @@ let _ = let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in - let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd_class _ = VtQuery,VtNow in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in - Vernacextend.vernac_extend ~command:"PrintConstr" [cmd] + vernac_extend ~command:"PrintConstr" [cmd] let _ = let open Vernacextend in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in - let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd_class _ = VtQuery,VtNow in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in - Vernacextend.vernac_extend ~command:"PrintPureConstr" [cmd] + vernac_extend ~command:"PrintPureConstr" [cmd] (* Setting printer of unbound global reference *) open Names diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 63d7d58053..5eac3e2b9c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -101,7 +101,7 @@ val ppdelta : Mod_subst.delta_resolver -> unit val pp_idpred : Names.Id.Pred.t -> unit val pp_cpred : Names.Cpred.t -> unit -val pp_transparent_state : Names.transparent_state -> unit +val pp_transparent_state : TransparentState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit @@ -120,9 +120,9 @@ val ppclenv : Clenv.clausenv -> unit val ppgoalgoal : Goal.goal -> unit -val ppgoal : Proof_type.goal Evd.sigma -> unit +val ppgoal : Goal.goal Evd.sigma -> unit (* also print evar map *) -val ppgoalsigma : Proof_type.goal Evd.sigma -> unit +val ppgoalsigma : Goal.goal Evd.sigma -> unit val pphintdb : Hints.Hint_db.t -> unit val ppproofview : Proofview.proofview -> unit |