diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 3 | ||||
| -rw-r--r-- | dev/ci/README-developers.md | 165 | ||||
| -rw-r--r-- | dev/ci/README-users.md | 85 | ||||
| -rw-r--r-- | dev/ci/README.md | 216 | ||||
| -rw-r--r-- | dev/ci/appveyor.sh | 9 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 19 | ||||
| -rwxr-xr-x | dev/ci/gitlab.bat | 8 | ||||
| -rw-r--r-- | dev/ci/nix/README.md | 19 | ||||
| -rw-r--r-- | dev/ci/nix/unicoq.nix | 7 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08850-poly-local-univs.sh | 9 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh | 9 | ||||
| -rw-r--r-- | dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh | 6 | ||||
| -rw-r--r-- | dev/doc/about-hints | 454 | ||||
| -rw-r--r-- | dev/doc/cic.dtd | 231 | ||||
| -rw-r--r-- | dev/doc/minicoq.tex | 98 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 6 | ||||
| -rw-r--r-- | dev/doc/transition-V5.10-V6 | 5 | ||||
| -rw-r--r-- | dev/doc/transition-V6-V7 | 8 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 1 | ||||
| -rwxr-xr-x | dev/tools/create_overlays.sh | 2 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 5 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 |
24 files changed, 329 insertions, 1052 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d0b5f4be47..b202635714 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1905,6 +1905,9 @@ function make_addon_quickchick { function make_addons { # Note: ':' is the empty command, which does not produce any output : > "/build/filelists/addon_dependencies.nsh" + : > "/build/filelists/addon_strings.nsh" + : > "/build/filelists/addon_descriptions.nsh" + : > "/build/filelists/addon_sections.nsh" for addon in $COQ_ADDONS; do "make_addon_$addon" 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 bc49e3e76b..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 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=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). +*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 abeb039c0e..cda369fb1b 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -2,14 +2,15 @@ set -e -x -APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c +APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c -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 init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing +eval "$(opam env)" opam install -y num ocamlfind ounit +# Full regular Coq Build cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4d5834eeb6..96bc5be7ff 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -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}" 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/gitlab.bat b/dev/ci/gitlab.bat index 918d289ae2..386a3de204 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -39,6 +39,10 @@ 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 ^
@@ -56,10 +60,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/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/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh new file mode 100644 index 0000000000..482792d7cd --- /dev/null +++ b/dev/ci/user-overlays/08850-poly-local-univs.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then + formal_topology_CI_REF=poly-local-univs + formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology + + paramcoq_CI_REF=poly-local-univs + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/ci/user-overlays/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/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/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh new file mode 100644 index 0000000000..2df8affd14 --- /dev/null +++ b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then + + elpi_CI_REF=ltac+remove_aliases + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/doc/about-hints b/dev/doc/about-hints deleted file mode 100644 index 95712c3cf9..0000000000 --- a/dev/doc/about-hints +++ /dev/null @@ -1,454 +0,0 @@ -An investigation of how ZArith lemmas could be classified in different -automation classes - -- Reversible lemmas relating operators (to be declared as hints but - needing precedences) -- Equivalent notions (one has to be considered as primitive and the - other rewritten into the canonical one) -- Isomorphisms between structure (one structure has to be considered - as more primitive than the other for a give operator) -- Irreversible simplifications (to be declared with precedences) -- Reversible bottom-up simplifications (to be used in hypotheses) -- Irreversible bottom-up simplifications (to be used in hypotheses - with precedences) -- Rewriting rules (relevant for autorewrite, or for an improved auto) - -Note: this analysis, made in 2001, was previously stored in -theories/ZArith/Zhints.v. It has been moved here to avoid obfuscating -the standard library. - -(**********************************************************************) -(** * Reversible lemmas relating operators *) -(** Probably to be declared as hints but need to define precedences *) - -(** ** Conversion between comparisons/predicates and arithmetic operators *) - -(** Lemmas ending by eq *) -(** -<< -Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` -Zabs_eq: (x:Z)`0 <= x`->`|x| = x` -Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)` -Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y` -Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y` -Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)` -Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)` -Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y` -Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)` -Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)` -Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)` ->> -*) - -(** ** Conversion between nat comparisons and Z comparisons *) - -(** Lemmas ending by eq *) -(** -<< -inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)` ->> -*) - -(** Lemmas ending by Zge *) -(** -<< -inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)` ->> -*) - -(** ** Conversion between comparisons *) - -(** Lemmas ending by Zge *) -(** -<< -not_Zlt: (x,y:Z)~`x < y`->`x >= y` -Zle_ge: (m,n:Z)`m <= n`->`n >= m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` -not_Zle: (x,y:Z)~`x <= y`->`x > y` -Zlt_gt: (m,n:Z)`m < n`->`n > m` -Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -not_Zge: (x,y:Z)~`x >= y`->`x < y` -Zgt_lt: (m,n:Z)`m > n`->`n < m` -Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)` -not_Zgt: (x,y:Z)~`x > y`->`x <= y` -Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p` -Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p` -Zge_le: (m,n:Z)`m >= n`->`n <= m` -Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p` -Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m` -Zlt_le_weak: (n,m:Z)`n < m`->`n <= m` -Zle_refl: (n,m:Z)`n = m`->`n <= m` ->> -*) - -(** ** Irreversible simplification involving several comparaisons *) -(** useful with clear precedences *) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d` -Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d` ->> -*) - -(** ** What is decreasing here ? *) - -(** Lemmas ending by eq *) -(** -<< -Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)` ->> -*) - -(**********************************************************************) -(** * Useful Bottom-up lemmas *) - -(** ** Bottom-up simplification: should be used *) - -(** Lemmas ending by eq *) -(** -<< -Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` -Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p` -Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m` -Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m` -Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m` -Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m` -Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m` -Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m` ->> -*) - -(** Lemmas ending by Zle *) -(** << Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m` -Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m` -Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *) - -(** ** Bottom-up irreversible (syntactic) simplification *) - -(** Lemmas ending by Zle *) -(** -<< -Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` ->> -*) - -(** ** Other unclearly simplifying lemmas *) - -(** Lemmas ending by Zeq *) -(** -<< -Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0` ->> -*) - -(* Lemmas ending by Zgt *) -(** -<< -Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` ->> -*) - -(* Lemmas ending by Zlt *) -(** -<< -pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` ->> -*) - -(* Lemmas ending by Zle *) -(** -<< -Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y` -OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y` ->> -*) - - -(**********************************************************************) -(** * Irreversible lemmas with meta-variables *) -(** To be used by EAuto *) - -(* Hints Immediate *) -(** Lemmas ending by eq *) -(** -<< -Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m` ->> -*) - -(** Lemmas ending by Zge *) -(** -<< -Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p` -Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p` -Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p` -Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p` ->> -*) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p` -Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p` -Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p` ->> -*) - - -(**********************************************************************) -(** * Unclear or too specific lemmas *) -(** Not to be used ? *) - -(** ** Irreversible and too specific (not enough regular) *) - -(** Lemmas ending by Zle *) -(** -<< -Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` -Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z` -OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z` -OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t` ->> -*) - -(** ** Expansion and too specific ? *) - -(** Lemmas ending by Zge *) -(** -<< -Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b` ->> -*) - -(** Lemmas ending by Zgt *) -(** -<< -Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b` -Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y` ->> -*) - -(** Lemmas ending by Zle *) -(** -<< -Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b` -Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y` ->> -*) - -(** ** Reversible but too specific ? *) - -(** Lemmas ending by Zlt *) -(** -<< -Zlt_minus: (n,m:Z)`0 < m`->`n-m < n` ->> -*) - -(**********************************************************************) -(** * Lemmas to be used as rewrite rules *) -(** but can also be used as hints *) - -(** Left-to-right simplification lemmas (a symbol disappears) *) - -(** -<< -Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m) -Zmin_n_n: (n:Z)`(Zmin n n) = n` -Zmult_1_n: (n:Z)`1*n = n` -Zmult_n_1: (n:Z)`n*1 = n` -Zminus_plus: (n,m:Z)`n+m-n = m` -Zle_plus_minus: (n,m:Z)`n+(m-n) = m` -Zopp_Zopp: (x:Z)`(-(-x)) = x` -Zero_left: (x:Z)`0+x = x` -Zero_right: (x:Z)`x+0 = x` -Zplus_inverse_r: (x:Z)`x+(-x) = 0` -Zplus_inverse_l: (x:Z)`(-x)+x = 0` -Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y` -Zmult_one: (x:Z)`1*x = x` -Zero_mult_left: (x:Z)`0*x = 0` -Zero_mult_right: (x:Z)`x*0 = 0` -Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y` ->> -*) - -(** Right-to-left simplification lemmas (a symbol disappears) *) - -(** -<< -Zpred_Sn: (m:Z)`m = (Zpred (Zs m))` -Zs_pred: (n:Z)`n = (Zs (Zpred n))` -Zplus_n_O: (n:Z)`n = n+0` -Zmult_n_O: (n:Z)`0 = n*0` -Zminus_n_O: (n:Z)`n = n-0` -Zminus_n_n: (n:Z)`0 = n-n` -Zred_factor6: (x:Z)`x = x+0` -Zred_factor0: (x:Z)`x = x*1` ->> -*) - -(** Unclear orientation (no symbol disappears) *) - -(** -<< -Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)` -Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)` -Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))` -Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p` -Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)` -Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)` -Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)` -Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)` -Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m` -Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p` -Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p` -Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)` -Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p` -Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)` -Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m` -Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z` -Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p` -Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)` -Zplus_sym: (x,y:Z)`x+y = y+x` -Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z` -Zmult_sym: (x,y:Z)`x*y = y*x` -Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z` -Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))` -Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))` -Zopp_one: (x:Z)`(-x) = x*(-1)` -Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)` -Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)` -Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y` -Zred_factor1: (x:Z)`x+x = x*2` -Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)` -Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)` -Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)` -Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y` -Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n` ->> -*) - -(** nat <-> Z *) -(** -<< -inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))` -inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)` -inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)` -inj_minus1: - (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)` -inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0` ->> -*) - -(** Too specific ? *) -(** -<< -Zred_factor5: (x,y:Z)`x*0+y = y` ->> -*) diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd deleted file mode 100644 index cc33efd483..0000000000 --- a/dev/doc/cic.dtd +++ /dev/null @@ -1,231 +0,0 @@ -<?xml encoding="ISO-8859-1"?> - -<!-- DTD FOR CIC OBJECTS: --> - -<!-- CIC term declaration --> - -<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST| - LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'> - -<!-- CIC sorts --> - -<!ENTITY % sort '(Prop|Set|Type)'> - -<!-- CIC sequents --> - -<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'> - -<!-- CIC objects: --> - -<!ELEMENT ConstantType %term;> -<!ATTLIST ConstantType - name CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT ConstantBody %term;> -<!ATTLIST ConstantBody - for CDATA #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT CurrentProof (Conjecture*,body)> -<!ATTLIST CurrentProof - of CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT InductiveDefinition (InductiveType+)> -<!ATTLIST InductiveDefinition - noParams NMTOKEN #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Variable (body?,type)> -<!ATTLIST Variable - name CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Sequent %sequent;> -<!ATTLIST Sequent - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!-- Elements used in CIC objects, which are not terms: --> - -<!ELEMENT InductiveType (arity,Constructor*)> -<!ATTLIST InductiveType - name CDATA #REQUIRED - inductive (true|false) #REQUIRED> - -<!ELEMENT Conjecture %sequent;> -<!ATTLIST Conjecture - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Constructor %term;> -<!ATTLIST Constructor - name CDATA #REQUIRED> - -<!ELEMENT Decl %term;> -<!ATTLIST Decl - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Def %term;> -<!ATTLIST Def - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Hidden EMPTY> -<!ATTLIST Hidden - id ID #REQUIRED> - -<!ELEMENT Goal %term;> - -<!-- CIC terms: --> - -<!ELEMENT LAMBDA (decl*,target)> -<!ATTLIST LAMBDA - sort %sort; #REQUIRED> - -<!ELEMENT LETIN (def*,target)> -<!ATTLIST LETIN - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT PROD (decl*,target)> -<!ATTLIST PROD - type %sort; #REQUIRED> - -<!ELEMENT CAST (term,type)> -<!ATTLIST CAST - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT REL EMPTY> -<!ATTLIST REL - value NMTOKEN #REQUIRED - binder CDATA #REQUIRED - id ID #REQUIRED - idref IDREF #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT SORT EMPTY> -<!ATTLIST SORT - value CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT APPLY (%term;)+> -<!ATTLIST APPLY - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT VAR EMPTY> -<!ATTLIST VAR - relUri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- The substitutions are ordered by increasing de Bruijn --> -<!-- index. An empty substitution means that that index is --> -<!-- not accessible. --> -<!ELEMENT META (substitution*)> -<!ATTLIST META - no NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT IMPLICIT EMPTY> -<!ATTLIST IMPLICIT - id ID #REQUIRED> - -<!ELEMENT CONST EMPTY> -<!ATTLIST CONST - uri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTIND EMPTY> -<!ATTLIST MUTIND - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT MUTCONSTRUCT EMPTY> -<!ATTLIST MUTCONSTRUCT - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - noConstr NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)> -<!ATTLIST MUTCASE - uriType CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT FIX (FixFunction+)> -<!ATTLIST FIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT COFIX (CofixFunction+)> -<!ATTLIST COFIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- Elements used in CIC terms: --> - -<!ELEMENT FixFunction (type,body)> -<!ATTLIST FixFunction - name CDATA #REQUIRED - recIndex NMTOKEN #REQUIRED> - -<!ELEMENT CofixFunction (type,body)> -<!ATTLIST CofixFunction - name CDATA #REQUIRED> - -<!ELEMENT substitution ((%term;)?)> - -<!-- Explicit named substitutions: --> - -<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)> -<!ATTLIST instantiate - id ID #IMPLIED> - -<!-- Sintactic sugar for CIC terms and for CIC objects: --> - -<!ELEMENT arg %term;> -<!ATTLIST arg - relUri CDATA #REQUIRED> - -<!ELEMENT decl %term;> -<!ATTLIST decl - id ID #REQUIRED - type %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT def %term;> -<!ATTLIST def - id ID #REQUIRED - sort %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT target %term;> - -<!ELEMENT term %term;> - -<!ELEMENT type %term;> - -<!ELEMENT arity %term;> - -<!ELEMENT patternsType %term;> - -<!ELEMENT inductiveTerm %term;> - -<!ELEMENT pattern %term;> - -<!ELEMENT body %term;> diff --git a/dev/doc/minicoq.tex b/dev/doc/minicoq.tex deleted file mode 100644 index a34b03a491..0000000000 --- a/dev/doc/minicoq.tex +++ /dev/null @@ -1,98 +0,0 @@ -\documentclass{article} - -\usepackage{fullpage} -\input{./macros.tex} -\newcommand{\minicoq}{\textsf{minicoq}} -\newcommand{\nonterm}[1]{\textit{#1}} -\newcommand{\terminal}[1]{\textsf{#1}} -\newcommand{\listzero}{\textit{LIST$_0$}} -\newcommand{\listun}{\textit{LIST$_1$}} -\newcommand{\sep}{\textit{SEP}} - -\title{Minicoq: a type-checker for the pure \\ - Calculus of Inductive Constructions} - - -\begin{document} - -\maketitle - -\section{Introduction} - -\minicoq\ is a minimal toplevel for the \Coq\ kernel. - - -\section{Grammar of terms} - -The grammar of \minicoq's terms is given in Figure~\ref{fig:terms}. - -\begin{figure}[htbp] - \hrulefill - \begin{center} - \begin{tabular}{lrl} - term & ::= & identifier \\ - & $|$ & \terminal{Rel} integer \\ - & $|$ & \terminal{Set} \\ - & $|$ & \terminal{Prop} \\ - & $|$ & \terminal{Type} \\ - & $|$ & \terminal{Const} identifier \\ - & $|$ & \terminal{Ind} identifier integer \\ - & $|$ & \terminal{Construct} identifier integer integer \\ - & $|$ & \terminal{[} name \terminal{:} term - \terminal{]} term \\ - & $|$ & \terminal{(} name \terminal{:} term - \terminal{)} term \\ - & $|$ & term \verb!->! term \\ - & $|$ & \terminal{(} \listun\ term \terminal{)} \\ - & $|$ & \terminal{(} term \terminal{::} term \terminal{)} \\ - & $|$ & \verb!<! term \verb!>! \terminal{Case} - term \terminal{of} \listzero\ term \terminal{end} - \\[1em] - name & ::= & \verb!_! \\ - & $|$ & identifier - \end{tabular} - \end{center} - \hrulefill - \caption{Grammar of terms} - \label{fig:terms} -\end{figure} - -\section{Commands} -The grammar of \minicoq's commands are given in -Figure~\ref{fig:commands}. All commands end with a dot. - -\begin{figure}[htbp] - \hrulefill - \begin{center} - \begin{tabular}{lrl} - command & ::= & \terminal{Definition} identifier \terminal{:=} term. \\ - & $|$ & \terminal{Definition} identifier \terminal{:} term - \terminal{:=} term. \\ - & $|$ & \terminal{Parameter} identifier \terminal{:} term. \\ - & $|$ & \terminal{Variable} identifier \terminal{:} term. \\ - & $|$ & \terminal{Inductive} \terminal{[} \listzero\ param - \terminal{]} \listun\ inductive \sep\ - \terminal{with}. \\ - & $|$ & \terminal{Check} term. - \\[1em] - param & ::= & identifier - \\[1em] - inductive & ::= & identifier \terminal{:} term \terminal{:=} - \listzero\ constructor \sep\ \terminal{$|$} - \\[1em] - constructor & ::= & identifier \terminal{:} term - \end{tabular} - \end{center} - \hrulefill - \caption{Commands} - \label{fig:commands} -\end{figure} - - -\end{document} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index b33a1cbd73..b1c111685b 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -64,10 +64,8 @@ ## On the date of the feature freeze ## -- [ ] Create the new version branch `vX.X` and - [protect it](https://github.com/coq/coq/settings/branches) - (activate the "Protect this branch", "Require pull request reviews before - merging" and "Restrict who can push to this branch" guards). +- [ ] Create the new version branch `vX.X` (using this name will ensure that + the branch will be automatically protected). - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The proposed model is to have a "X.X-only PRs" column for the rare PRs on the stable branch, a diff --git a/dev/doc/transition-V5.10-V6 b/dev/doc/transition-V5.10-V6 deleted file mode 100644 index df7b65dd8b..0000000000 --- a/dev/doc/transition-V5.10-V6 +++ /dev/null @@ -1,5 +0,0 @@ -The V5.10 archive has been created with cvs in February 1995 by -Jean-Christophe Filliâtre. It was moved to archive V6 in March 1996. -At this occasion, the contrib directory (user-contributions) were -moved to a separate directory and some theories (like ALGEBRA) moved -to the user-contributions directory too. diff --git a/dev/doc/transition-V6-V7 b/dev/doc/transition-V6-V7 deleted file mode 100644 index e477c9ff9d..0000000000 --- a/dev/doc/transition-V6-V7 +++ /dev/null @@ -1,8 +0,0 @@ -The V6 archive has been created in March 1996 with files from the -former V5.10 archive and has been abandoned in 2000. - -A new archive named V7 has been created in August 1999 by -Jean-Christophe Filliâtre with a new architecture placing the -type-checking at the kernel of Coq. This new architecture came with a -"cleaner" organization of files, a uniform indentation style, uniform -headers, etc. diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 707c7f07ce..c1dcabb743 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -17,6 +17,7 @@ exec $OCAMLDEBUG \ -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 index 314ac07e68..41392be5d7 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -75,4 +75,4 @@ 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 +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 4287702b3a..b90a53220d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -20,13 +20,12 @@ open Univ open Environ open Printer open Constr -open Goptions open Genarg open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true -let _ = set_bool_option_value ["Printing";"Matching"] false +let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) |