aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/MERGING.md120
-rw-r--r--dev/doc/README.md76
-rw-r--r--dev/doc/about-hints454
-rw-r--r--dev/doc/build-system.dev.txt40
-rw-r--r--dev/doc/build-system.dune.md161
-rw-r--r--dev/doc/build-system.txt8
-rw-r--r--dev/doc/changes.md345
-rw-r--r--dev/doc/cic.dtd231
-rw-r--r--dev/doc/coq-src-description.txt8
-rw-r--r--dev/doc/critical-bugs262
-rw-r--r--dev/doc/debugging.md2
-rw-r--r--dev/doc/minicoq.tex98
-rw-r--r--dev/doc/ocamlbuild.txt30
-rw-r--r--dev/doc/primproj.md41
-rw-r--r--dev/doc/profiling.txt54
-rw-r--r--dev/doc/proof-engine.md31
-rw-r--r--dev/doc/release-process.md128
-rw-r--r--dev/doc/setup.txt269
-rw-r--r--dev/doc/transition-V5.10-V65
-rw-r--r--dev/doc/transition-V6-V78
-rw-r--r--dev/doc/translate.txt495
-rw-r--r--dev/doc/universes.md (renamed from dev/doc/univpoly.txt)191
-rw-r--r--dev/doc/universes.txt26
-rw-r--r--dev/doc/versions-history.tex12
-rw-r--r--dev/doc/xml-protocol.md4
25 files changed, 1285 insertions, 1814 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 71fc396088..318562338d 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -1,23 +1,26 @@
# Merging changes in Coq
-This document describes how patches (submitted as Pull Requests) should be
-merged into the main repository (https://github.com/coq/coq).
+This document describes how patches, submitted as pull requests (PRs) on the
+`master` branch, should be merged into the main repository
+(https://github.com/coq/coq).
## Code owners
-The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
-system, two owners. One is the principal maintainer of the component, the other
-is the secondary maintainer.
+The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of
+the code. Sometime there is one principal maintainer and one or several
+secondary maintainer(s). Sometimes, it is a team of code owners and all of its
+members act as principal maintainers for the component.
-When a pull request is submitted, GitHub will automatically ask the principal
-maintainer for a review. If the pull request touches several parts, all the
-corresponding principal maintainers will be asked for a review.
+When a PR is submitted, GitHub will automatically ask the principal
+maintainer (or the code owner team) for a review. If the PR touches several
+parts, all the corresponding owners will be asked for a review.
Maintainers are never assigned as reviewer on their own PRs.
-If a principal maintainer submits a PR that changes the component they own, they
-must assign the secondary maintainer as reviewer. They should also do it if they
-know they are not available to do the review.
+If a principal maintainer submits a PR or is a co-author of a PR that is
+submitted and this PR changes the component they own, they must request a
+review from a secondary maintainer. They can also delegate the review if they
+know they are not available to do it.
## Reviewing
@@ -34,17 +37,51 @@ When maintainers receive a review request, they are expected to:
REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
process described below.
-In all cases, maintainers can delegate reviews to the other maintainer of the
-same component, except if it would lead to a maintainer reviewing their own
-patch.
+When a PR received lots of comments or if the PR has not been opened for long
+and the assignee thinks that some other developers might want to comment,
+it is recommended that they announce their intention to merge and wait a full
+working day (or more if deemed useful) before the actual merge, as a sort of
+last call for comments.
+
+In all cases, maintainers can delegate reviews to the other maintainers,
+except if it would lead to a maintainer reviewing their own patch.
A maintainer is expected to be reasonably reactive, but no specific timeframe is
given for reviewing.
+When none of the maintainers have commented nor self-assigned a PR in a delay
+of five working days, any maintainer of another component who feels comfortable
+reviewing the PR can assign it to themselves. To prevent misunderstandings,
+maintainers should not hesitate to announce in advance when they shall be
+unavailable for more than five working days.
+
(*) In case a component is touched in a trivial way (adding/removing one file in
-a `Makefile`, etc), or by applying a systematic process (global renaming,
-deprecationg propagation, etc) that has been reviewed globally, the assignee can
-say in a comment they think a review is not required and proceed with the merge.
+a `Makefile`, etc), or by applying a systematic refactoring process (global
+renaming for instance) that has been reviewed globally, the assignee can
+say in a comment they think a review is not required from every code owner and
+proceed with the merge.
+
+### Breaking changes
+
+If the PR breaks compatibility of some external projects in CI, then fixes to
+those external projects should have been prepared (cf. the relevant sub-section
+in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
+with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
+
+Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or
+the [`dev/doc/changes.md`](changes.md) file.
+
+If overlays are missing, ask the author to prepare them and label the PR with
+the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
+
+When fixes are ready, there are two cases to consider:
+
+- For patches that are backward compatible (best scenario), you should get the
+ external project maintainers to integrate them before merging the PR.
+- For patches that are not backward compatible (which is often the case when
+ patching plugins after an update to the Coq API), you can proceed to merge
+ the PR and then notify the external project maintainers they can merge the
+ patch.
## Merging
@@ -52,7 +89,17 @@ Once all reviewers approved the PR, the assignee is expected to check that CI
completed without relevant failures, and that the PR comes with appropriate
documentation and test cases. If not, they should leave a comment on the PR and
put the approriate label. Otherwise, they are expected to merge the PR using the
-[merge script](/dev/tools/merge-pr.sh).
+[merge script](../tools/merge-pr.sh).
+
+When CI has a few failures which look spurious, restarting the corresponding
+jobs is a good way of ensuring this was indeed the case.
+To restart a job on Travis or on AppVeyor, you should connect using your GitHub
+account; being part of the Coq organization on GitHub should give you the
+permission to do so.
+To restart a job on GitLab CI, you should sign into GitLab (this can be done
+using a GitHub account); if you are part of the
+[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry"
+button; otherwise, send a request to join the organization.
When the PR has conflicts, the assignee can either:
- ask the author to rebase the branch, fixing the conflicts
@@ -61,18 +108,45 @@ When the PR has conflicts, the assignee can either:
In both cases, CI should be run again.
-In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR
+is not a candidate for backporting), it is ok to fix
the conflicts in the merge commit (following the same steps as below), and push
-to `master` directly. Don't use the GitHub interface to fix these conflicts.
+to `master` directly. DON'T USE the GitHub interface to fix these conflicts.
-The command to be used is:
+To merge the PR proceed in the following way
```
-$ dev/tools/merge-pr XXXX
+$ git checkout master
+$ git pull
+$ dev/tools/merge-pr.sh XXXX
+$ git push upstream
```
-where `XXXX` is the number of the PR to be merged. This operation should be followed by a push.
+where `XXXX` is the number of the PR to be merged and `upstream` is the name
+of your remote pointing to `git@github.com:coq/coq.git`.
+Note that you are only supposed to merge PRs into `master`. PRs should rarely
+target the stable branch, but when it is the case they are the responsibility
+of the release manager.
+
+This script conducts various checks before proceeding to merge. Don't bypass them
+without a good reason to, and in that case, write a comment in the PR thread to
+explain the reason.
Maintainers MUST NOT merge their own patches.
DON'T USE the GitHub interface for merging, since it will prevent the automated
backport script from operating properly, generates bad commit messages, and a
messy history when there are conflicts.
+
+### Merge script dependencies
+
+The merge script passes option `-S` to `git merge` to ensure merge commits
+are signed. Consequently, it depends on the GnuPG command utility being
+installed and a GPG key being available. Here is a short documentation on
+how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/.
+
+The script depends on a few other utilities. If you are a Nix user, the
+simplest way of getting them is to run `nix-shell` first.
+
+**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG
+is not out of the box. Installing explicitly "pinentry-mac" seems important for
+typing of passphrase to work correctly (see also this
+[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)).
diff --git a/dev/doc/README.md b/dev/doc/README.md
new file mode 100644
index 0000000000..c764455aed
--- /dev/null
+++ b/dev/doc/README.md
@@ -0,0 +1,76 @@
+# Beginner's guide to hacking Coq
+
+## Getting dependencies
+
+Assuming one is running Ubuntu (if not, replace `apt` with the package manager of choice)
+
+```
+$ sudo apt-get install make opam git
+
+# At the time of writing, <latest-ocaml-version> is 4.07.0.
+# The latest version number is available at: https://ocaml.org/releases/
+
+$ opam init --comp <latest-ocaml-version>
+
+# Then follow the advice displayed at the end as how to update your
+ ~/.bashrc and ~/.ocamlinit files.
+
+$ source ~/.bashrc
+
+# needed if you want to build "coqide" target
+
+$ sudo apt-get install liblablgtksourceview2-ocaml-dev \
+ libgtk2.0-dev libgtksourceview2.0-dev
+$ opam install lablgtk
+```
+
+## Building `coqtop`
+The general workflow is to first setup a development environment with
+the correct `configure` settings, then hacking on Coq, make-ing, and testing.
+
+
+This document will use `$JOBS` to refer to the number of parallel jobs one
+is willing to have with `make`.
+
+
+```
+$ git clone git clone https://github.com/coq/coq.git
+$ cd coq
+$ ./configure -profile devel
+$ make -j $JOBS # Make once for `merlin`(autocompletion tool)
+
+<hack>
+
+$ make -j $JOBS states # builds just enough to run coqtop
+$ bin/coqtop -compile <test_file_name.v>
+<goto hack until stuff works>
+
+<run test-suite>
+```
+
+To learn how to run the test suite, you can read
+[`test-suite/README.md`](../../test-suite/README.md).
+
+## Coq functions of interest
+- `Coqtop.start`: This function is the main entry point of coqtop.
+- `Coqtop.parse_args `: This function is responsible for parsing command-line arguments.
+- `Coqloop.loop`: This function implements the read-eval-print loop.
+- `Vernacentries.interp`: This function is called to execute the Vernacular command user have typed.
+ It dispatches the control to specific functions handling different Vernacular command.
+- `Vernacentries.vernac_check_may_eval`: This function handles the `Check ...` command.
+
+
+## Development environment + tooling
+- [`Merlin`](https://github.com/ocaml/merlin) for autocomplete.
+- [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup)
+
+## A note about rlwrap
+
+When using `rlwrap coqtop` make sure the version of `rlwrap` is at least
+`0.42`, otherwise you will get
+
+```
+rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory
+```
+
+If this happens either update or use an alternate readline wrapper like `ledit`.
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/build-system.dev.txt b/dev/doc/build-system.dev.txt
index abba13428f..b0a2b04121 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -1,5 +1,3 @@
-
-
HISTORY:
-------
@@ -35,13 +33,41 @@ HISTORY:
grammar.cma (and q_constr.cmo) directly, no need for a separate
subcall to make nor awkward include-failed-and-retry.
-
----------------------------------------------------------------------------
+* February - September 2018 (Emilio Jesús Gallego Arias)
+
+ Dune support added.
+
+ The build setup is mostly vanilla for the OCaml part, however the
+ `.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper
+ that will generate the necessary `dune` files.
+
+ As a developer, you should not have to deal with Dune configuration
+ files on a regular basis unless adding a new library or plugin.
+ The vanilla setup declares all the Coq libraries and binaries [we
+ must respect proper containment/module implementation rules as to
+ allow packing], and we build custom preprocessors (based on `camlp5`
+ and `coqpp`) that will process the `ml4`/`mlg` files.
+
+ This suffices to build `coqtop` and `coqide`, all that remains to
+ handle is `.vo` compilation.
+
+ To teach Dune about the `.vo`, we use a small utility `coq_dune`,
+ that will generate a `dune` file for each directory in `plugins` and
+ `theories`. The code is pretty straightforward and declares build
+ and install rules for each `.v` straight out of `coqdep`. Thus, our
+ build strategy looks like this:
+
+ 1. Use `dune` to build `coqdep` and `coq_dune`.
+ 2. Use `coq_dune` to generate `dune` files for each directory with `.v` files.
+ 3. ?
+ 4. Profit! [Seriously, at this point Dune has all the information to build Coq]
+
+---------------------------------------------------------------------------
-This file documents internals of the implementation of the build
-system. For what a Coq developer needs to know about the build system,
-see build-system.txt .
+This file documents internals of the implementation of the make-based
+build system. For what a Coq developer needs to know about the build
+system, see build-system.txt and build-system.dune.md .
.ml4 files
----------
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
new file mode 100644
index 0000000000..3609171b82
--- /dev/null
+++ b/dev/doc/build-system.dune.md
@@ -0,0 +1,161 @@
+This file documents what a Coq developer needs to know about the
+Dune-based build system. If you want to enhance the build system
+itself (or are curious about its implementation details), see
+build-system.dev.txt, and in particular its initial HISTORY section.
+
+About Dune
+==========
+
+Coq can now be built using [Dune](https://github.com/ocaml/dune).
+
+## Quick Start
+
+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,
+so please be sure your tree is clean from objects files generated by
+the make-based system.
+
+If you want to build the standard libraries and plugins you should
+call `make -f Makefile.dune voboot`. It is usually enough to do that
+once per-session.
+
+More helper targets are availabe in `Makefile.dune`, `make -f
+Makefile.dune` will display some help.
+
+Dune places build artifacts in a separate directory `_build`; it will
+also generate an `.install` file so files can be properly installed by
+package managers.
+
+Contrary to other systems, Dune doesn't use a global `Makefile` but
+local build files named `dune` that are later composed to form a
+global build.
+
+As a developer, Dune should take care of all OCaml-related build tasks
+including library management, merlin files, and linking order. You are
+are not supposed to modify the `dune` files unless you are adding a
+new binary, library, or plugin.
+
+## Per-User Custom Settings
+
+Dune will read the file `~/.config/dune/config`; see `man
+dune-config`. Among others, you can set in this file the custom number
+of build threads `(jobs N)` and display options `(display _mode_)`.
+
+## Targets
+
+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`, 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
+`$library` can be any directory in the current workspace. For example,
+`dune utop engine` or `dune utop plugins/ltac` will launch `utop` with
+the right libraries already loaded.
+
+Note that you must invoke the `#rectypes;;` toplevel flag in order to
+use Coq libraries. The provided `.ocamlinit` file does this
+automatically.
+
+## ocamldebug
+
+You can use `ocamldebug` with Dune; after a build, do:
+
+```
+dune exec dev/dune-dbg
+(ocd) source dune_db
+```
+
+or
+
+```
+dune exec dev/dune-dbg checker
+(ocd) source dune_db
+```
+
+for the checker. Unfortunately, dependency handling here is not fully
+refined, so you need to build enough of Coq once to use this target
+[it will then correctly compute the deps and rebuild if you call the
+script again] This will be fixed in the future.
+
+## Compositionality, developer and release modes.
+
+By default [in "developer mode"], Dune will compose all the packages
+present in the tree and perform a global build. That means that for
+example you could drop the `ltac2` folder under `plugins` and get a
+build using `ltac2`, that will use the current Coq version.
+
+This is very useful to develop plugins and Coq libraries as your
+plugin will correctly track dependencies and rebuild incrementally as
+needed.
+
+However, it is not always desirable to go this way. For example, the
+current Coq source tree contains two packages [Coq and CoqIDE], and in
+the OPAM CoqIDE package we don't want to build CoqIDE against the
+local copy of Coq. For this purpose, Dune supports the `-p` option, so
+`dune build -p coqide` will build CoqIDE against the system-installed
+version of Coq libs, and use a "release" profile that for example
+enables stronger compiler optimizations.
+
+## Stanzas
+
+`dune` files contain the so-called "stanzas", that may declare:
+
+- libraries,
+- executables,
+- documentation, arbitrary blobs.
+
+The concrete options for each stanza can be seen in the Dune manual,
+but usually the default setup will work well with the current Coq
+sources. Note that declaring a library or an executable won't make it
+installed by default, for that, you need to provide a "public name".
+
+## Workspaces and Profiles
+
+Dune provides support for tree workspaces so the developer can set
+global options --- such as flags --- on all packages, or build Coq
+with different OPAM switches simultaneously [for example to test
+compatibility]; for more information, please refer to the Dune manual.
+
+## Inlining reports
+
+The `ireport` profile will produce standard OCaml [inlining
+reports](https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html#sec488). These
+are to be found under `_build/default/$lib/$lib.objs/$module.$round.inlining.org`
+and are in Emacs `org-mode` format.
+
+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.
+
+## Planned and Advanced features
+
+Dune supports or will support extra functionality that may result very
+useful to Coq, some examples are:
+
+- Cross-compilation.
+- Automatic Generation of OPAM files.
+- Multi-directory libraries.
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index fd3101613a..8cefe699cc 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -140,11 +140,9 @@ New files
For a new file, in most cases, you just have to add it to the proper
file list(s):
- For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib)
- These files are also used by the experimental ocamlbuild plugin,
- which is quite touchy about them : be careful with order,
- duplicated entries, whitespace errors, and do not mention .mli there.
- If module B depends on module A, then B should be after A in the .mllib
- file.
+ Be careful with order, duplicated entries, whitespace errors, and
+ do not mention .mli there. If module B depends on module A, then B
+ should be after A in the .mllib file.
- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
- The definitions in Makefile.common might have to be adapted too.
- If your file needs a specific rule, add it to Makefile.build
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ab78b0956f..acb0d80c18 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,321 @@
+## 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
+
+- All functions marked [@@ocaml.deprecated] in 8.8 have been
+ removed. Please, make sure your plugin is warning-free in 8.8 before
+ trying to port it over 8.9.
+
+Names
+
+- Kernel names no longer contain a section path. They now have only two
+ components (module path and label), which led to some changes in the API:
+
+ KerName.make takes only 2 components
+ KerName.repr returns only 2 components
+ KerName.make2 is now KerName.make
+ 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
+ `register_ref` and `lib_ref`. The first one is available through the
+ vernacular `Register` command; it binds a name to a constant. The second
+ command then enables to locate the registered constant through its name. The
+ name resolution is dynamic.
+
+Macros:
+
+- The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
+ deprecated. Use TYPED AS instead.
+
+- coqpp (.mlg) based VERNAC EXTEND accesses attributes through a `#[ x
+ = att ]` syntax, where `att : 'a Attributes.attribute` and `x` will
+ be bound with type `'a` in the expression, unlike the old system
+ where `atts : Vernacexpr.vernac_flags` was bound in the expression
+ and had to be manually parsed.
+
+## Changes between Coq 8.8 and Coq 8.9
+
+### ML API
+
+Names
+
+- In `Libnames`, the type `reference` and its two constructors `Qualid` and
+ `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
+ `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
+ replaced by a test using `qualid_is_ident`. Extracting the `ident` part of a
+ `qualid` can be done using `qualid_basename`.
+
+Misctypes
+
+- Syntax for universe sorts and kinds has been moved from `Misctypes`
+ to `Glob_term`, as these are turned into kernel terms by
+ `Pretyping`.
+
+Proof engine
+
+- More functions have been changed to use `EConstr`, notably the
+ functions in `Evd`, and in particular `Evd.define`.
+
+ Note that the core function `EConstr.to_constr` now _enforces_ by
+ default that the resulting term is ground, that is to say, free of
+ Evars. This is usually what you want, as open terms should be of
+ type `EConstr.t` to benefit from the invariants the `EConstr` API is
+ meant to guarantee.
+
+ In case you'd like to violate this API invariant, you can use the
+ `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
+ that setting this flag to false is deprecated so it is only meant to
+ be used as to help port pre-EConstr code.
+
+- A few type alias have been deprecated, in all cases the message
+ should indicate what the canonical form is. An important change is
+ the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+
+- Unification API returns `evar_map option` instead of `bool * evar_map`
+ with the guarantee that the `evar_map` was unchanged if the boolean
+ was false.
+
+ML Libraries used by Coq
+
+- Introduction of a `Smart` module for collecting `smart*` functions, e.g.
+ `Array.Smart.map`.
+- Uniformization of some names, e.g. `Array.Smart.fold_left_map` instead
+ of `Array.smartfoldmap`.
+
+Printer.ml API
+
+- The mechanism in `Printer` that allowed dynamically overriding `pr_subgoals`,
+ `pr_subgoal` and `pr_goal` was removed to simplify the code. It was
+ earlier used by PCoq.
+
+Kernel
+
+- The following renamings happened:
+ - `Context.Rel.t` into `Constr.rel_context`
+ - `Context.Named.t` into `Constr.named_context`
+ - `Context.Compacted.t` into `Constr.compacted_context`
+ - `Context.Rel.Declaration.t` into `Constr.rel_declaration`
+ - `Context.Named.Declaration.t` into `Constr.named_declaration`
+ - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration`
+
+Source code organization
+
+- We have eliminated / fused some redundant modules and relocated a
+ few interfaces files. The `intf` folder is gone, and now for example
+ `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and
+ so on. Changes should be compatible, but in a few cases stricter
+ layering requirements may mean that functions have moved. In all
+ cases adapting is a matter of changing the module name.
+
+Vernacular commands
+
+- The implementation of vernacular commands has been refactored so it
+ is self-contained now, including the parsing and extension
+ mechanisms. This involves a couple of non-backward compatible
+ changes due to layering issues, where some functions have been moved
+ from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in
+ `tactics/`. In all cases adapting is a matter of changing the module
+ name.
+
+Primitive number parsers
+
+- For better modularity, the primitive parsers for `positive`, `N` and `Z`
+ have been split over three files (`plugins/syntax/positive_syntax.ml`,
+ `plugins/syntax/n_syntax.ml`, `plugins/syntax/z_syntax.ml`).
+
+Parsing
+
+- Manual uses of the `Pcoq.Gram` module have been deprecated. Wrapper modules
+ `Pcoq.Entry` and `Pcoq.Parsable` were introduced to replace it.
+
+Termops
+
+- Internal printing functions have been placed under the
+ `Termops.Internal` namespace.
+
+### Unit testing
+
+The test suite now allows writing unit tests against OCaml code in the Coq
+code base. Those unit tests create a dependency on the OUnit test framework.
+
+### Transitioning away from Camlp5
+
+In an effort to reduce dependency on camlp5, the use of several grammar macros
+is discouraged. Coq is now shipped with its own preprocessor, called coqpp,
+which serves the same purpose as camlp5.
+
+To perform the transition to coqpp macros, one first needs to change the
+extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are
+handled yet.
+
+Due to parsing constraints, the syntax of the macros is slightly different, but
+updating the source code is mostly a matter of straightforward
+search-and-replace. The main differences are summarized below.
+
+#### OCaml code
+
+Every piece of toplevel OCaml code needs to be wrapped into braces.
+
+For instance, code of the form
+```
+let myval = 0
+```
+should be turned into
+```
+{
+let myval = 0
+}
+```
+
+#### TACTIC EXTEND
+
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions with braces
+- if not there yet, add a leading `|` to the first rule
+
+For instance, code of the form:
+```
+TACTIC EXTEND my_tac
+ [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ]
+| [ "tac2" tactic(t) ] -> [ mytac2 t ]
+END
+```
+should be turned into
+```
+TACTIC EXTEND my_tac
+| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t }
+| [ "tac2" tactic(t) ] -> { mytac2 t }
+END
+```
+
+#### VERNAC EXTEND
+
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions and rule classifiers with
+ braces
+- if not there yet, add a leading `|̀ to the first rule
+
+Handwritten classifiers declared through the `CLASSIFIED BY` statement are
+considered OCaml code, so they also need to be wrapped in braces.
+
+For instance, code of the form:
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY classifier
+ [ "foo" int(i) ] => [ classif' ] -> [ cmd1 i ]
+| [ "bar" ] -> [ cmd2 ]
+END
+```
+should be turned into
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY { classifier }
+| [ "foo" int(i) ] => { classif' } -> { cmd1 i }
+| [ "bar" ] -> { cmd2 }
+END
+```
+
+#### ARGUMENT EXTEND
+
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions with braces
+- if not there yet, add a leading `|` to the first rule
+- syntax of `TYPED AS` has been restricted not to accept compound generic
+ arguments as a literal, e.g. `foo_opt` should be rewritten into `foo option`
+ and similarly `foo_list` into `foo list`.
+- parenthesis around pair types in `TYPED AS` are now mandatory
+- `RAW_TYPED AS` and `GLOB_TYPED AS` clauses need to be removed
+
+`BY` clauses are considered OCaml code, and thus need to be wrapped in braces,
+but not the `TYPED AS` clauses.
+
+For instance, code of the form:
+```
+ARGUMENT EXTEND my_arg
+ TYPED AS int_opt
+ PRINTED BY printer
+ INTERPRETED BY interp_f
+ GLOBALIZED BY glob_f
+ SUBSTITUTED BY subst_f
+ RAW_TYPED AS int_opt
+ RAW_PRINTED BY raw_printer
+ GLOB_TYPED AS int_opt
+ GLOB_PRINTED BY glob_printer
+ [ "foo" int(i) ] -> [ my_arg1 i ]
+| [ "bar" ] -> [ my_arg2 ]
+END
+```
+should be turned into
+```
+ARGUMENT EXTEND my_arg
+ TYPED AS { int_opt }
+ PRINTED BY { printer }
+ INTERPRETED BY { interp_f }
+ GLOBALIZED BY { glob_f }
+ SUBSTITUTED BY { subst_f }
+ RAW_PRINTED BY { raw_printer }
+ GLOB_PRINTED BY { glob_printer }
+| [ "foo" int(i) ] -> { my_arg1 i }
+| [ "bar" ] -> { my_arg2 }
+END
+```
+
+#### GEXTEND
+
+Most plugin writers do not need this low-level interface, but for the sake of
+completeness we document it.
+
+Steps to perform are:
+- replace `GEXTEND` with `GRAMMAR EXTEND`
+- wrap every occurrence of OCaml code in actions into braces `{ }`
+
+For instance, code of the form
+```
+GEXTEND Gram
+ GLOBAL: my_entry;
+
+my_entry:
+[ [ x = bar; y = qux -> do_something x y
+ | "("; z = LIST0 my_entry; ")" -> do_other_thing z
+] ];
+END
+```
+should be turned into
+```
+GRAMMAR EXTEND Gram
+ GLOBAL: my_entry;
+
+my_entry:
+[ [ x = bar; y = qux -> { do_something x y }
+ | "("; z = LIST0 my_entry; ")" -> { do_other_thing z }
+] ];
+END
+```
+
+Caveats:
+- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases
+ this as a shorthand for all global entries. Solution: always define a `GLOBAL`
+ section.
+- No complex patterns allowed in token naming. Solution: match on it inside the
+ OCaml quotation.
+
## Changes between Coq 8.7 and Coq 8.8
### Bug tracker
@@ -16,13 +334,13 @@ All the other bugs kept their number.
General deprecation
-- All functions marked [@@ocaml.deprecated] in 8.7 have been
+- All functions marked `[@@ocaml.deprecated]` in 8.7 have been
removed. Please, make sure your plugin is warning-free in 8.7 before
trying to port it over 8.8.
Proof engine
- Due to the introduction of `EConstr` in 8.7, it is not necessary to
+- Due to the introduction of `EConstr` in 8.7, it is not necessary to
track "goal evar normal form status" anymore, thus the type `'a
Proofview.Goal.t` loses its ghost argument. This may introduce some
minor incompatibilities at the typing level. Code-wise, things
@@ -44,8 +362,8 @@ We changed the type of the following functions:
- `Global.body_of_constant`: same as above.
-- `Constrinterp.*` generally, many functions that used to take an
- `evar_map ref` have been now switched to functions that will work in
+- `Constrinterp.*`: generally, many functions that used to take an
+ `evar_map ref` have now been switched to functions that will work in
a functional way. The old style of passing `evar_map`s as references
is not supported anymore.
@@ -63,16 +381,21 @@ We have changed the representation of the following types:
Some tactics and related functions now support static configurability, e.g.:
-- injectable, dEq, etc. takes an argument ~keep_proofs which,
- - if None, tells to behave as told with the flag Keep Proof Equalities
- - if Some b, tells to keep proof equalities iff b is true
+- `injectable`, `dEq`, etc. take an argument `~keep_proofs` which,
+ - if `None`, tells to behave as told with the flag `Keep Proof Equalities`
+ - if `Some b`, tells to keep proof equalities iff `b` is true
Declaration of printers for arguments used only in vernac command
-- It should now use "declare_extra_vernac_genarg_pprule" rather than
- "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+- It should now use `declare_extra_vernac_genarg_pprule` rather than
+ `declare_extra_genarg_pprule`, otherwise, a failure at runtime might
happen. An alternative is to register the corresponding argument as
- a value, using "Geninterp.register_val0 wit None".
+ a value, using `Geninterp.register_val0 wit None`.
+
+Types Alias deprecation and type relocation.
+
+- A few type alias have been deprecated, in all cases the message
+ should indicate what the canonical form is.
### STM API
@@ -110,7 +433,7 @@ functions when some given constants are traversed:
* `declare_reduction_effect`: to declare a hook to be applied when some
constant are visited during the execution of some reduction functions
- (primarily cbv).
+ (primarily `cbv`).
* `set_reduction_effect`: to declare a constant on which a given effect
hook should be called.
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/coq-src-description.txt b/dev/doc/coq-src-description.txt
index b3d49b7e56..e5e4f740bd 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -17,12 +17,6 @@ toplevel
Special components
------------------
-intf :
-
- Contains mli-only interfaces, many of them providing a.s.t.
- used for dialog bewteen coq components. Ex: Constrexpr.constr_expr
- produced by parsing and transformed by interp.
-
grammar :
Camlp5 syntax extensions. The file grammar/grammar.cma is used
@@ -100,7 +94,7 @@ Tacexpr.glob_tactic_expr
|
| Tacinterp.eval_tactic (?)
V
-Proof_type.tactic
+Proofview.V82.tac
TODO: check with Hugo
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
new file mode 100644
index 0000000000..8d78559c0d
--- /dev/null
+++ b/dev/doc/critical-bugs
@@ -0,0 +1,262 @@
+Preliminary compilation of critical bugs in stable releases of Coq
+==================================================================
+ WORK IN PROGRESS WITH SEVERAL OPEN QUESTIONS
+
+
+To add: #7723 (vm_compute universe polymorphism), #7695 (modules and algebraic universes), #7615 (lost functor substitutions)
+
+Typing constructions
+
+ component: "match"
+ summary: substitution missing in the body of a let
+ introduced: ?
+ impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl4
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: master/trunk/v8.5 (e583a79b5, 22 Nov 2015, Herbelin), v8.4 (525056f1, 22 Nov 2015, Herbelin), v8.3 (4bed0289, 22 Nov 2015, Herbelin)
+ found by: Herbelin
+ exploit: test-suite/success/Case22.v
+ GH issue number: ?
+ risk: ?
+
+ component: fixpoint, guard
+ summary: missing lift in checking guard
+ introduced: probably from V5.10
+ impacted released versions: probably V5-V7, V8.0-V8.0pl4, V8.1-V8.1pl4
+ impacted development branches: v8.0 ?
+ impacted coqchk versions: ?
+ fixed in: master/trunk/v8.2 (ff45afa8, r11646, 2 Dec 2008, Barras), v8.1 (f8e7f273, r11648, 2 Dec 2008, Barras)
+ found by: Barras
+ exploit: test-suite/failure/guard.v
+ GH issue number: none
+ risk: unprobable by chance
+
+ component: cofixpoint, guard
+ summary: de Bruijn indice bug in checking guard of nested cofixpoints
+ introduced: after V6.3.1, before V7.0
+ impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: master (9f81e2c36, 10 Apr 2014, Dénès), v8.4 (f50ec9e7d, 11 Apr 2014, Dénès), v8.3 (40c0fe7f4, 11 Apr 2014, Dénès), v8.2 (06d66df8c, 11 Apr 2014, Dénès), v8.1 (977afae90, 11 Apr 2014, Dénès), v8.0 (f1d632992, 29 Nov 2015, Herbelin, backport)
+ found by: Dénès
+ exploit: ?
+ GH issue number: none ?
+ risk: ?
+
+ component: inductive types, elimination principle
+ summary: de Bruijn indice bug in computing allowed elimination principle
+ introduced: 23 May 2006, 9c2d70b, r8845, Herbelin (part of universe polymorphism)
+ impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: master (8a01c3685, 24 Jan 2014, Dénès), v8.4 (8a01c3685, 25 Feb 2014, Dénès), v8.3 (2b3cc4f85, 25 Feb 2014, Dénès), v8.2 (459888488, 25 Feb 2014, Dénès), v8.1 (79aa20872, 25 Feb 2014, Dénès)
+ found by: Dénès
+ exploit: see GH#3211
+ GH issue number: #3211
+ risk: ?
+
+ component: universe subtyping
+ summary: bug in Prop<=Set conversion which made Set identifiable with Prop, preventing a proof-irrelevant interpretation of Prop
+ introduced: V8.2 (bba897d5f, 12 May 2008, Herbelin)
+ impacted released versions: V8.2-V8.2pl2
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport)
+ found by: Georgi Guninski
+ exploit: test-suite/bugs/closed/4294.v
+ GH issue number: #4294
+ risk: ?
+
+Module system
+
+ component: modules, universes
+ summary: missing universe constraints in typing "with" clause of a module type
+ introduced: ?
+ impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl6; unclear for V8.2 and previous versions
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau)
+ found by: Dénès
+ exploit: test-suite/bugs/closed/4294.v
+ GH issue number: #4294
+ risk: ?
+
+Module system
+
+ component: modules, universes
+ summary: universe constraints for module subtyping not stored in vo files
+ introduced: presumably 8.2 (b3d3b56)
+ impacted released versions: 8.2, 8.3, 8.4
+ impacted development branches: v8.5
+ impacted coqchk versions: none
+ fixed in: v8.2 (c1d9889), v8.3 (8056d02), v8.4 (a07deb4), trunk (0cd0a3e) Mar 5, 2014, Tassi
+ found by: Tassi by running coqchk on the mathematical components library
+ exploit: requires multiple files, no test provided
+ GH issue number: #3243
+ risk: could be exploited by mistake
+
+Universes
+
+ component: template polymorphism
+ summary: issue with two parameters in the same universe level
+ introduced: 23 May 2006, 9c2d70b, r8845, Herbelin
+ impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin),
+ found by: Barras
+ exploit: test-suite/failure/inductive4.v
+ GH issue number: none
+ risk: unlikely to be activated by chance
+
+ component: universe polymorphism
+ summary: universe polymorphism can capture global universes
+ impacted released versions: V8.5 to V8.8
+ impacted coqchk versions: V8.5 to current (NOT FIXED)
+ fixed in: 2385b5c1ef
+ found by: Gaëtan Gilbert
+ exploit: test-suite/misc/poly-capture-global-univs
+ GH issue number: #8341
+ risk: unlikely to be activated by chance (requires a plugin)
+
+Primitive projections
+
+ component: primitive projections, guard condition
+ summary: check of guardedness of extra arguments of primitive projections missing
+ introduced: 6 May 2014, a4043608f, Sozeau
+ impacted released versions: V8.5-V8.5pl2,
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: trunk/master/v8.5 (ba00867d5, 25 Jul 2016, Sozeau)
+ found by: Sozeau, by analyzing bug report #4876
+ exploit: to be done (?)
+ GH issue number: #4876
+ risk: consequence of bug found by chance, unlikely to be exploited by chance (MS?)
+
+ component: primitive projections, guard condition
+ summary: records based on primitive projections became possibly recursive without the guard condition being updated
+ introduced: 10 Sep 2014, 6624459e4, Sozeau (?)
+ impacted released versions: V8.5
+ impacted development branches: none
+ impacted coqchk versions: ?
+ fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès)
+ found by: Dénès exploiting bug #4588
+ exploit: test-suite/bugs/closed/4588.v
+ GH issue number: #4588
+ risk: ?
+
+Conversion machines
+
+ component: "lazy machine" (lazy krivine abstract machine)
+ summary: the invariant justifying some optimization was wrong for some combination of sharing side effects
+ introduced: prior to V7.0
+ impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl3
+ impacted development branches: none
+ impacted coqchk versions: (eefe63d52, Barras, 20 May 2008), was in beta-development for 8.2 at this time
+ fixed in: master/trunk/8.2 (f13aaec57/a8b034513, 15 May 2008, Barras), v8.1 (e7611477a, 15 May 2008, Barras), v8.0 (6ed40a8bc, 29 Nov 2016, Herbelin, backport)
+ found by: Gonthier
+ exploit: by Gonthier
+ GH issue number: none
+ risk: unrealistic to be exploited by chance
+
+ component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+ summary: collision between constructors when more than 256 constructors in a type
+ introduced: V8.1
+ impacted released versions: V8.1-V8.5pl3, V8.2-V8.2pl2, V8.3-V8.3pl3, V8.4-V8.4pl5
+ impacted development branches: none
+ impacted coqchk versions: none (no virtual machine in coqchk)
+ fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport)
+ found by: Dénès, Pédrot
+ exploit: test-suite/failure/vm-bug4157.v
+ GH issue number: #4157
+ risk:
+
+ component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+ summary: wrong universe constraints
+ introduced: possibly exploitable from V8.1; exploitable at least from V8.5
+ impacted released versions: V8.1-V8.4pl5 unknown, V8.5-V8.5pl3, V8.6-V8.6.1, V8.7.0-V8.7.1
+ impacted development branches: unknown for v8.1-v8.4, none from v8.5
+ impacted coqchk versions: none (no virtual machine in coqchk)
+ fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport)
+ found by: Dénès
+ exploit: test-suite/bugs/closed/6677.v
+ GH issue number: #6677
+ risk:
+
+ component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+ summary: missing pops in executing 31bit arithmetic
+ introduced: V8.5
+ impacted released versions: V8.1-V8.4pl5
+ impacted development branches: v8.1 (probably)
+ impacted coqchk versions: none (no virtual machine in coqchk)
+ fixed in: master/trunk/v8.5 (a5e04d9dd, 6 Sep 2015, Dénès), v8.4 (d5aa3bf6, 9 Sep 2015, Dénès), v8.3 (5da5d751, 9 Sep 2015, Dénès), v8.2 (369e82d2, 9 Sep 2015, Dénès),
+ found by: Catalin Hritcu
+ exploit: lost?
+ GH issue number: ?
+ risk:
+
+ component: "native" conversion machine (translation to OCaml which compiles to native code)
+ summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
+ introduced: V8.5
+ impacted released versions: V8.5-V8.5pl1
+ impacted development branches: none
+ impacted coqchk versions: none (no native computation in coqchk)
+ fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey),
+ found by: Letouzey, Dénès
+ exploit: lost?
+ GH issue number: ?
+ risk:
+
+Conflicts with axioms in library
+
+ component: library of real numbers
+ summary: axiom of description and decidability of equality on real numbers in library Reals was inconsistent with impredicative Set
+ introduced: 67c75fa01, 20 Jun 2002
+ impacted released versions: 7.3.1, 7.4
+ impacted coqchk versions:
+ fixed by deciding to drop impredicativity of Set: bac707973, 28 Oct 2004
+ found by: Herbelin & Werner
+ exploit: need to find the example again
+ GH issue number: no
+ risk: unlikely to be exploited by chance
+
+ component: library of extensional sets, guard condition
+ summary: guard condition was unknown to be inconsistent with propositional extensionality in library Sets
+ introduced: not a bug per se but an incompatibility discovered late
+ impacted released versions: technically speaking from V6.1 with the introduction of the Sets library which was then inconsistent from the very beginning without we knew it
+ impacted coqchk versions: ?
+ fixed by constraining the guard condition: (9b272a8, ccd7546c 28 Oct 2014, Barras, Dénès)
+ found by: Schepler, Dénès, Azevedo de Amorim
+ exploit: ?
+ GH issue number: none
+ risk: unlikely to be exploited by chance (?)
+
+ component: library for axiom of choice and excluded-middle
+ summary: incompatibility axiom of choice and excluded-middle with elimination of large singletons to Set
+ introduced: not a bug but a change of intended "model"
+ impacted released versions: strictly before 8.1
+ impacted coqchk versions: ?
+ fixed by constraining singleton elimination: b19397ed8, r9633, 9 Feb 2007, Herbelin
+ found by: Benjamin Werner
+ exploit:
+ GH issue number: none
+ risk:
+
+There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1).
+
+There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical.
+
+Another non exploitable bug?
+
+ component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+ summary: bug in 31bit arithmetic
+ introduced: V8.1
+ impacted released versions: none
+ impacted development branches:
+ impacted coqchk versions: none (no virtual machine in coqchk)
+ fixed in: master/trunk/v8.5 (0f8d1b92c, 6 Sep 2015, Dénès)
+ found by: Dénès, from a bug report by Tahina Ramananandro
+ exploit: ?
+ GH issue number: ?
+ risk:
+
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index fd3cbd1bc3..14a1cc693c 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs
7. some hints:
- To debug a failure/error/anomaly, add a breakpoint in
- Vernac.vernac_com at the with clause of the "try ... interp com
+ `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com
with ..." block, then go "back" a few steps to find where the
failure/error/anomaly has been raised
- Alternatively, for an error or an anomaly, add breakpoints in the middle
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/ocamlbuild.txt b/dev/doc/ocamlbuild.txt
deleted file mode 100644
index efedbc506e..0000000000
--- a/dev/doc/ocamlbuild.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-Ocamlbuild & Coq
-----------------
-
-A quick note in case someone else gets interested someday in compiling
-Coq via ocamlbuild : such an experimental build system has existed
-in the past (more or less maintained from 2009 to 2013), in addition
-to the official build system via gnu make. But this build via
-ocamlbuild has been severly broken since early 2014 (and don't work
-in 8.5, for instance). This experiment has attracted very limited
-interest from other developers over the years, and has been quite
-cumbersome to maintain, so it is now officially discontinued.
-If you want to have a look at the files of this build system
-(especially myocamlbuild.ml), you can fetch :
- - my last effort at repairing this build system (up to coqtop.native) :
- https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair
- - coq official v8.5 branch (recent but broken)
- - coq v8.4 branch(less up-to-date, but works).
-
-For the record, the three main drawbacks of this experiments were:
- - recurrent issues with circularities reported by ocamlbuild
- (even though make was happy) during the evolution of Coq sources
- - no proper support of parallel build
- - quite slow re-traversal of already built things
-See the two corresponding bug reports on Mantis, or
-https://github.com/ocaml/ocamlbuild/issues/52
-
-As an interesting feature, I successfully used this to cross-compile
-Coq 8.4 from linux to win32 via mingw.
-
-Pierre Letouzey, june 2016
diff --git a/dev/doc/primproj.md b/dev/doc/primproj.md
new file mode 100644
index 0000000000..ea76aeeab5
--- /dev/null
+++ b/dev/doc/primproj.md
@@ -0,0 +1,41 @@
+Primitive Projections
+---------------------
+
+ | Proj of Projection.t * constr
+
+Projections are always applied to a term, which must be of a record
+type (i.e. reducible to an inductive type `I params`). Type-checking,
+reduction and conversion are fast (not as fast as they could be yet)
+because we don't keep parameters around. As you can see, it's
+currently a `constant` that is used here to refer to the projection,
+that will change to an abstract `projection` type in the future.
+Basically a projection constant records which inductive it is a
+projection for, the number of params and the actual position in the
+constructor that must be projected. For compatibility reason, we also
+define an eta-expanded form (accessible from user syntax `@f`). The
+constant_entry of a projection has both informations. Declaring a
+record (under `Set Primitive Projections`) will generate such
+definitions. The API to declare them is not stable at the moment, but
+the inductive type declaration also knows about the projections, i.e.
+a record inductive type decl contains an array of terms representing
+the projections. This is used to implement eta-conversion for record
+types (with at least one field and having all projections definable).
+The canonical value being `Build_R (pn x) ... (pn x)`. Unification and
+conversion work up to this eta rule. The records can also be universe
+polymorphic of course, and we don't need to keep track of the universe
+instance for the projections either. Projections are reduced _eagerly_
+everywhere, and introduce a new `Zproj` constructor in the abstract
+machines that obeys both the delta (for the constant opacity) and iota
+laws (for the actual reduction). Refolding works as well (afaict), but
+there is a slight hack there related to universes (not projections).
+
+For the ML programmer, the biggest change is that pattern-matchings on
+kind_of_term require an additional case, that is handled usually
+exactly like an `App (Const p) arg`.
+
+There are slight hacks related to hints is well, to use the primitive
+projection form of f when one does `Hint Resolve f`. Usually hint
+resolve will typecheck the term, resulting in a partially applied
+projection (disallowed), so we allow it to take
+`constr_or_global_reference` arguments instead and special-case on
+projections. Other tactic extensions might need similar treatment.
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 9d2ebf0d4c..29e87df6b8 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux.
In Coq source folder:
-opam switch 4.02.1+fp
+opam switch 4.05.0+trunk+fp
./configure -local -debug
make
perf record -g bin/coqtop -compile file.v
@@ -21,6 +21,58 @@ and plug into the process
perf record -g -p PID
+### Per-component [flame graphs](https://github.com/brendangregg/FlameGraph)
+
+I (Andres Erbsen) have found it useful to look at library-wide flame graphs of
+coq time consumption. As the Ltac interpreter stack is reflected in the OCaml
+stack, calls to the same primitive can appear on top of multiple essentially
+equivalent stacks. To make the profiles more readable, one could either try to
+edit the stack trace to merge "equivalent" frames, or simply look at the
+aggregate profile on a component-by-component basis. Here is how to do the
+second for the standard library ([example output](https://cdn.rawgit.com/andres-erbsen/b29b29cb6480dfc6a662062e4fcd0ae3/raw/304fc3fea9630c8e453929aa7920ca8a2a570d0b/stdlib_categorized_outermost.svg)).
+
+~~~~~
+#!/bin/bash
+make -f Makefile.dune clean
+make -f Makefile.dune states
+perf record -F99 `# ~1GB of data` --call-graph=dwarf -- make -f Makefile.dune world
+perf script --time '0%-100%' |
+ stackcollapse-perf.pl |
+ grep Coqtop__compile |
+ sed -rf <(cat <<'EOF'
+ s/;caml/;/g
+ s/_[0-9]*;/;/g
+ s/Logic_monad__fun;//g
+ s/_apply[0-9];//g
+ s/;System/@&@/
+ s/;Hashcons/@&@/
+ s/;Grammar/@&@/
+ s/;Declaremods/@&@/
+ s/;Tactics/@&@/
+ s/;Pretyping/@&@/
+ s/;Typeops/@&@/
+ s/;Reduction/@&@/
+ s/;Unification/@&@/
+ s/;Evarutil/@&@/
+ s/;Evd/@&@/
+ s/;EConstr/@&@/
+ s/;Constr/@&@/
+ s/;Univ/@&@/
+ s/;Ugraph/@&@/
+ s/;UState/@&@/
+ s/;Micromega/@&@/
+ s/;Omega/@&@/
+ s/;Auto/@&@/
+ s/;Ltac_plugin__Tacinterp/@&@/
+ s/;Ltac_plugin__Rewrite/@&@/
+ s/[^@]*@;([^@]*)@/\1;\1/
+ s/@//g
+ :a; s/;([^;]+);\1;/;\1;/g;ta
+EOF
+ ) |
+ flamegraph.pl
+~~~~~
+
## Memory
You first need a few commits atop trunk for this to work.
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index 8f96ac223f..774552237a 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the
`Refine.refine` primitive.
```ocaml
-val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine typecheck t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
[evar_map] context. The term [t] is used as a partial solution
for the current goal (refine is a goal-dependent tactic), the
new holes created by [t] become the new subgoals. Exceptions
@@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
```
-In a first approximation, we can think of `'a Sigma.run` as
-`evar_map -> 'a * evar_map`. What the function does is first evaluate the
-`Constr.t Sigma.run` argument in the current proof state, and then use the
-resulting term as a filler for the proof under focus. All evars that have been
-created by the invocation of this thunk are then turned into new goals added in
-the order of their creation.
+What the function does is first evaluate the `t` argument in the
+current proof state, and then use the resulting term as a filler for
+the proof under focus. All evars that have been created by the
+invocation of this thunk are then turned into new goals added in the
+order of their creation.
To see how we can use it, let us have a look at an idealized example, the `cut`
tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]`
@@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order.
```ocaml
let cut c =
- let open Sigma in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
(** In this block, we focus on one goal at a time indicated by gl *)
let env = Proofview.Goal.env gl in
(** Get the context of the goal, essentially [Γ] *)
@@ -80,25 +78,22 @@ let cut c =
let t = mkArrow c (Vars.lift 1 concl) in
(** Build [X -> A]. Note the lifting of [A] due to being on the right hand
side of the arrow. *)
- Refine.refine { run = begin fun sigma ->
+ Refine.refine begin fun sigma ->
(** All evars generated by this block will be added as goals *)
- let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in
+ let sigma, f = Evarutil.new_evar env sigma t in
(** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the
term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity
substitution for [Γ] is extracted from the [env] argument, so that
one must be careful to pass the correct context here in order for the
resulting term to be well-typed. The [p] return value is a proof term
used to enforce sigma monotonicity. *)
- let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in
+ let sigma, x = Evarutil.new_evar env sigma c in
(** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return
[x := Γ ⊢ ?e2{Γ} : X]. *)
let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in
(** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *)
- Sigma (r, sigma, p +> q)
- (** Fills the current hole with [r]. The [p +> q] thingy ensures
- monotonicity of sigma. *)
- end }
- end }
+ end
+ end
```
The `Evarutil.new_evar` function is the preferred way to generate evars in
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
new file mode 100644
index 0000000000..b33a1cbd73
--- /dev/null
+++ b/dev/doc/release-process.md
@@ -0,0 +1,128 @@
+# Release process #
+
+## As soon as the previous version branched off master ##
+
+- [ ] Create a new issue to track the release process where you can copy-paste
+ the present checklist.
+- [ ] Change the version name to the next major version and the magic numbers
+ (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+- [ ] Update the compatibility infrastructure, which consists of doing
+ the following steps. Note that all but the final step can be
+ performed automatically by
+ [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so
+ long as you have already updated `coq_version` in
+ [`configure.ml`](/configure.ml).
+ + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header
+ from [`dev/header.ml`](/dev/header.ml)
+ + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of
+ `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X.
+ + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions
+ prior to X.X.
+ + [ ] Update
+ [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
+ with the deleted/added files.
+ + [ ] Remove any notations in the standard library which have `compat "W.W"`.
+ + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
+ bumping all the version numbers by one, and update the interpretations
+ of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
+ [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+ + [ ] Update the files
+ [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
+ [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
+ and
+ [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v)
+ by bumping all version numbers by 1.
+ + [ ] Decide what to do about all test-suite files which mention `-compat
+ W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only
+ keep compatibility against the two previous versions)
+- [ ] Put the corresponding alpha tag using `git tag -s`.
+ The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
+ branch of the previous version.
+- [ ] Create the `X.X+beta1` milestone if it did not already exist.
+- [ ] Decide the release calendar with the team (freeze date, beta date, final
+ release date) and put this information in the milestone (using the
+ description and due date fields).
+
+## About one month before the beta ##
+
+- [ ] Create the `X.X.0` milestone and set its due date.
+- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to
+ remove from the beta milestone what they already know won't be ready on time
+ (possibly postponing to the `X.X.0` milestone for minor bug fixes,
+ infrastructure and documentation updates).
+- [ ] Determine which issues should / must be fixed before the beta, add them
+ to the beta milestone, possibly with a
+ ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker)
+ label. Make sure that all these issues are assigned (and that the assignee
+ provides an ETA).
+- [ ] Ping the development coordinator (**@mattam82**) to get him started on
+ the update to the Credits chapter of the reference manual.
+ See also [#7058](https://github.com/coq/coq/issues/7058).
+ The command to get the list of contributors for this version is
+ `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2`
+ (the ordering is approximative as it will misplace people with middle names).
+
+## 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).
+- [ ] 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
+ "Request X.X inclusion" column for the PRs that were merged in `master` that
+ are to be considered for backporting, a "Waiting for CI" column to put the
+ PRs in the process of being backported, and "Shipped in ..." columns to put
+ what was backported. (The release manager is the person responsible for
+ merging PRs that target the version branch and backporting appropriate PRs
+ that are merged into `master`).
+ A message to **@coqbot** in the milestone description tells it to
+ automatically add merged PRs to the "Request X.X inclusion" column.
+- [ ] Delay non-blocking issues to the appropriate milestone and ensure
+ blocking issues are solved. If required to solve some blocking issues,
+ it is possible to revert some feature PRs in the version branch only.
+
+## Before the beta release date ##
+
+- [ ] Ensure the Credits chapter has been updated.
+- [ ] Ensure that an appropriate version of the plugins we will distribute with
+ Coq has been tagged.
+- [ ] Have some people test the recently auto-generated Windows and MacOS
+ packages.
+- [ ] Change the version name from alpha to beta1 (see
+ [#7009](https://github.com/coq/coq/pull/7009/files)).
+ We generally do not update the magic numbers at this point.
+- [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+
+### These steps are the same for all releases (beta, final, patch-level) ###
+
+- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
+ package managers can start preparing package updates.
+- [ ] Draft a release on GitHub.
+- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and
+ upload them on GitHub.
+- [ ] Prepare a page of news on the website with the link to the GitHub release
+ (see [coq/www#63](https://github.com/coq/www/pull/63)).
+- [ ] Upload the new version of the reference manual to the website.
+ *TODO: setup some continuous deployment for this.*
+- [ ] Merge the website update, publish the release
+ and send annoucement e-mails.
+- [ ] Ping **@Zimmi48** to publish a new version on Zenodo.
+ *TODO: automate this.*
+- [ ] Close the milestone
+
+## At the final release time ##
+
+- [ ] Change the version name to X.X.0 and the magic numbers (see
+ [#7271](https://github.com/coq/coq/pull/7271/files)).
+- [ ] Put the `VX.X.0` tag.
+
+Repeat the generic process documented above for all releases.
+
+- [ ] Switch the default version of the reference manual on the website.
+
+## At the patch-level release time ##
+
+We generally do not update the magic numbers at this point (see
+[`2881a18`](https://github.com/coq/coq/commit/2881a18)).
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
deleted file mode 100644
index c48c2d5d16..0000000000
--- a/dev/doc/setup.txt
+++ /dev/null
@@ -1,269 +0,0 @@
-This document provides detailed guidance on how to:
-- compile Coq
-- take advantage of Merlin in Emacs
-- enable auto-completion for Ocaml source-code
-- use ocamldebug in Emacs for debugging coqtop
-The instructions were tested with Debian 8.3 (Jessie).
-
-The procedure is somewhat tedious, but the final results are (still) worth the effort.
-
-How to compile Coq
-------------------
-
-Getting build dependencies:
-
- sudo apt-get install make opam git
- opam init --comp 4.02.3
- # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files.
-
- source ~/.bashrc
-
- # needed if you want to build "coqtop" target
- opam install camlp5
-
- # needed if you want to build "coqide" target
- sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev
- opam install lablgtk
-
- # needed if you want to build "doc" target
- sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \
- hevea texlive-latex-extra latex-xcolor
-
-Cloning Coq:
-
- # Go to the directory where you want to clone Coq's source-code. E.g.:
- cd ~/git
-
- git clone https://github.com/coq/coq.git
-
-Building coqtop:
-
- cd ~/git/coq
- git checkout trunk
- make distclean
- ./configure -profile devel
- make clean
- make -j4 coqide printers
-
-The "-profile devel" enables all options recommended for developers (like
-warnings, support for Merlin, etc). Moreover Coq is configured so that
-it can be run without installing it (i.e. from the current directory).
-
-Once the compilation is over check if
-- bin/coqtop
-- bin/coqide
-behave as expected.
-
-
-A note about rlwrap
--------------------
-
-When using "rlwrap coqtop" make sure the version of rlwrap is at least
-0.42, otherwise you will get
-
- rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory
-
-If this happens either update or use an alternate readline wrapper like "ledit".
-
-
-How to install and configure Merlin (for Emacs)
------------------------------------------------
-
- sudo apt-get install emacs
-
- opam install tuareg
- # Follow the advice displayed at the end as how to update your ~/.emacs file.
-
- opam install merlin
- # Follow the advice displayed at the end as how to update your ~/.emacs file.
-
-Then add this:
-
- (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path) ; directory containing merlin.el
- (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin") ; needed only if ocamlmerlin not already in your PATH
- (autoload 'merlin-mode "merlin" "Merlin mode" t)
- (add-hook 'tuareg-mode-hook 'merlin-mode)
- (add-hook 'caml-mode-hook 'merlin-mode)
- (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file")
-
- ;; Do not use TABs. These confuse Merlin.
- (setq-default indent-tabs-mode nil)
-
-to your ~/.emacs file.
-
-Further Emacs configuration when we start it for the first time.
-
-Try to open some *.ml file in Emacs, e.g.:
-
- cd ~/git/coq
- emacs toplevel/coqtop.ml &
-
-Emacs display the following strange message:
-
- The local variables list in ~/git/coq
- contains values that may be safe (*).
-
- Do you want to apply it?
-
-Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe."
-
-Emacs then shows two windows:
-- one window that shows the contents of the "toplevel/coqtop.ml" file
-- and the other window that shows greetings for new Emacs users.
-
-If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen."
-
-The default key-bindings are described here:
-
- https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch
-
-If you want, you can customize them by replacing the following lines:
-
- (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next)
- (define-key merlin-map (kbd "C-c C-l") 'merlin-locate)
- (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack)
- (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing)
-
-in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want.
-In the text below we assume that you changed the origin key-bindings in the following way:
-
- (define-key merlin-map (kbd "C-n") 'merlin-error-next)
- (define-key merlin-map (kbd "C-l") 'merlin-locate)
- (define-key merlin-map (kbd "C-b") 'merlin-pop-stack)
- (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing)
-
-Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window.
-If you prefer to jump to the definition within the same window, do this:
-
- <Alt+X> customize-group <ENTER> merlin <ENTER>
-
- Merlin Locate In New Window
-
- Value Menu
-
- Never Open In New Window
-
- State
-
- Set For Future Sessions
-
-Testing (Merlin):
-
- cd ~/git/coq
- emacs toplevel/coqtop.ml &
-
-Go to the end of the file where you will see the "start" function.
-
-Go to a line where "init_toplevel" function is called.
-
-If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>.
-
-If you want to jump back, type: <Ctrl+B>
-
-If you want to learn the type of the value at current cursor's position, type: <Ctrl+T>
-
-
-Enabling auto-completion in emacs
----------------------------------
-
-In Emacs, type: <Alt+M> list-packages <ENTER>
-
-In the list that is displayed, click on "company".
-
-A new window appears where just click on "Install" and then answer "Yes".
-
-These lines:
-
- (package-initialize)
- (require 'company)
- ; Make company aware of merlin
- (add-to-list 'company-backends 'merlin-company-backend)
- ; Enable company on merlin managed buffers
- (add-hook 'merlin-mode-hook 'company-mode)
- (global-set-key [C-tab] 'company-complete)
-
-then need to be added to your "~/.emacs" file.
-
-Next time when you start emacs and partially type some identifier,
-emacs will offer the corresponding completions.
-Auto-completion can also be manually invoked by typing <Ctrl+TAB>.
-Description of various other shortcuts is here.
-
- http://company-mode.github.io/
-
-
-Getting along with ocamldebug
------------------------------
-
-The default ocamldebug key-bindings are described here.
-
- http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369
-
-If you want, you can customize them by putting the following commands:
-
- (global-set-key (kbd "<f5>") 'ocamldebug-break)
- (global-set-key (kbd "<f6>") 'ocamldebug-run)
- (global-set-key (kbd "<f7>") 'ocamldebug-next)
- (global-set-key (kbd "<f8>") 'ocamldebug-step)
- (global-set-key (kbd "<f9>") 'ocamldebug-finish)
- (global-set-key (kbd "<f10>") 'ocamldebug-print)
- (global-set-key (kbd "<f12>") 'camldebug)
-
-to your "~/.emacs" file.
-
-Let us try whether ocamldebug in Emacs works for us.
-(If necessary, re-)compile coqtop:
-
- cd ~/git/coq
- make -j4 coqide printers
-
-open Emacs:
-
- emacs toplevel/coqtop.ml &
-
-and type:
-
- <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER>
-
-As a result, a new window is open at the bottom where you should see:
-
- (ocd)
-
-i.e. an ocamldebug shell.
-
- 1. Switch to the window that contains the "coqtop.ml" file.
- 2. Go to the end of the file.
- 3. Find the definition of the "start" function.
- 4. Go to the "let" keyword that is at the beginning of the first line.
- 5. By pressing <F5> you set a breakpoint to the cursor's position.
- 6. By pressing <F6> you start the bin/coqtop process.
- 7. Then you can:
- - step over function calls: <F7>
- - step into function calls: <F8>
- - or finish execution of the current function until it returns: <F9>.
-
-Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell.
-
-The points at which the execution of Ocaml program can stop are defined here:
-
- http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350
-
-
-Installing printers to ocamldebug
----------------------------------
-
-There is a pretty comprehensive set of printers defined for many common data types.
-You can load them by switching to the window holding the "ocamldebug" shell and typing:
-
- (ocd) source "../dev/db"
-
-
-Some of the functions were you might want to set a breakpoint and see what happens next
----------------------------------------------------------------------------------------
-
-- Coqtop.start : This function is the main entry point of coqtop.
-- Coqtop.parse_args : This function is responsible for parsing command-line arguments.
-- Coqloop.loop : This function implements the read-eval-print loop.
-- Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\
- It dispatches the control to specific functions handling different Vernacular command.
-- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command.
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/doc/translate.txt b/dev/doc/translate.txt
deleted file mode 100644
index 5b372c96c3..0000000000
--- a/dev/doc/translate.txt
+++ /dev/null
@@ -1,495 +0,0 @@
-
- How to use the translator
- =========================
-
- (temporary version to be included in the official
- TeX document describing the translator)
-
-The translator is a smart, robust and powerful tool to improve the
-readibility of your script. The current document describes the
-possibilities of the translator.
-
-In case of problem recompiling the translated files, don't waste time
-to modify the translated file by hand, read first the following
-document telling on how to modify the original files to get a smooth
-uniform safe translation. All 60000 lines of Coq lines on our
-user-contributions server have been translated without any change
-afterwards, and 0,5 % of the lines of the original files (mainly
-notations) had to be modified beforehand to get this result.
-
-Table of contents
------------------
-
-I) Implicit Arguments
- 1) Strict Implicit Arguments
- 2) Implicit Arguments in standard library
-
-II) Notations
- 1) Translating a V7 notation as it was
- 2) Translating a V7 notation which conflicts with the new syntax
- a) Associativity conflicts
- b) Conflicts with other notations
- b1) A notation hides another notation
- b2) A notation conflicts with the V8 grammar
- b3) My notation is already defined at another level
- c) How to use V8only with Distfix ?
- d) Can I overload a notation in V8, e.g. use "*" and "+" ?
- 3) Using the translator to have simplest notations
- 4) Setting the translator to automatically use new notations that
- wasn't used in old syntax
- 5) Defining a construction and its notation simultaneously
-
-III) Various pitfalls
- 1) New keywords
- 2) Old "Case" and "Match"
- 3) Change of definition or theorem names
- 4) Change of tactic names
-
----------------------------------------------------------------------
-
-I) Implicit Arguments
- ------------------
-
-1) Strict Implicit Arguments
-
- "Set Implicit Arguments" changes its meaning in V8: the default is
-to turn implicit only the arguments that are _strictly_ implicit (or
-rigid), i.e. that remains inferable whatever the other arguments
-are. E.g "x" inferable from "P x" is not strictly inferable since it
-can disappears if "P" is instanciated by a term which erase "x".
-
- To respect the old semantics, the default behaviour of the
-translator is to replace each occurrence "Set Implicit Arguments" by
-
- Set Implicit Arguments.
- Unset Strict Implicits.
-
- However, you may wish to adopt the new semantics of "Set Implicit
-Arguments" (for instance because you think that the choice of
-arguments it setsimplicit is more "natural" for you). In this case,
-add the option -strict-implicit to the translator.
-
- Warning: Changing the number of implicit arguments can break the
-notations. Then use the V8only modifier of Notations.
-
-2) Implicit Arguments in standard library
-
- Main definitions of standard library have now implicit
-arguments. These arguments are dropped in the translated files. This
-can exceptionally be a source of incompatibilities which has to be
-solved by hand (it typically happens for polymorphic functions applied
-to "nil" or "None").
-
-II) Notations
- ---------
-
- Grammar (on constr) and Syntax are no longer supported. Replace them by
-Notation before translation.
-
- Precedence levels are now from 0 to 200. In V8, the precedence and
-associativity of an operator cannot be redefined. Typical level are
-(refer to the chapter on notations in the Reference Manual for the
-full list):
-
- <-> : 95 (no associativity)
- -> : 90 (right associativity)
- \/ : 85 (right associativity)
- /\ : 80 (right associativity)
- ~ : 75 (right associativity)
- =, <, >, <=, >=, <> : 70 (no associativity)
- +, - : 50 (left associativity)
- *, / : 40 (left associativity)
- ^ : 30 (right associativity)
-
-1) Translating a V7 notation as it was
-
- By default, the translator keeps the associativity given in V7 while
-the levels are mapped according to the following table:
-
- the V7 levels [ 0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10]
- are resp. mapped in V8 to [ 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100]
- with predefined assoc [ No; L; R; L; L; No; R; R; R; No; L]
-
- If this is OK for you, just simply apply the translator.
-
-2) Translating a V7 notation which conflicts with the new syntax
-
-a) Associativity conflict
-
- Since the associativity of the levels obtained by translating a V7
-level (as shown on table above) cannot be changed, you have to choose
-another level with a compatible associativity.
-
- You can choose any level between 0 and 200, knowing that the
-standard operators are already set at the levels shown on the list
-above.
-
-Example 1: Assume you have a notation
-
-Infix NONA 2 "=_S" my_setoid_eq.
-
-By default, the translator moves it to level 30 which is right
-associative, hence a conflict with the expected no associativity.
-
-To solve the problem, just add the "V8only" modifier to reset the
-level and enforce the associativity as follows:
-
-Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
-
-The translator now knows that it has to translate "=_S" at level 70
-with no associativity.
-
-Rem: 70 is the "natural" level for relations, hence the choice of 70
-here, but any other level accepting a no-associativity would have been
-OK.
-
-Example 2: Assume you have a notation
-
-Infix RIGHTA 1 "o" my_comp.
-
-By default, the translator moves it to level 20 which is left
-associative, hence a conflict with the expected right associativity.
-
-To solve the problem, just add the "V8only" modifier to reset the
-level and enforce the associativity as follows:
-
-Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
-
-The translator now knows that it has to translate "o" at level 20
-which has the correct "right associativity".
-
-Rem: We assumed here that the user wants a strong precedence for
-composition, in such a way, say, that "f o g + h" is parsed as
-"(f o g) + h". To get "o" binding less than the arithmetical operators,
-an appropriated level would have been close of 70, and below, e.g. 65.
-
-b) Conflicts with other notations
-
-Since the new syntax comes with new keywords and new predefined
-symbols, new conflicts can occur. Again, you can use the option V8only
-to inform the translator of the new syntax to use.
-
-b1) A notation hides another notation
-
-Rem: use Print Grammar constr in V8 to diagnose the overlap and see the
-section on factorization in the chapter on notations of the Reference
-Manual for hints on how to factorize.
-
-Example:
-
-Notation "{ x }" := (my_embedding x) (at level 1).
-
-overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at
-level 99. The conflicts can be solved by left-factorizing the notation
-as follows:
-
-Notation "{ x }" := (my_embedding x) (at level 1)
- V8only (at level 0, x at level 99).
-
-b2) A notation conflicts with the V8 grammar.
-
-Again, use the V8only modifier to tell the translator to automatically
-take in charge the new syntax.
-
-Example:
-
-Infix 3 "@" app.
-
-Since "@" is used in the new syntax for deactivating the implicit
-arguments, another symbol has to be used, e.g. "@@". This is done via
-the V8only option as follows:
-
-Infix 3 "@" app V8only "@@" (at level 40, left associativity).
-
-or, alternatively by
-
-Notation "x @ y" := (app x y) (at level 3, left associativity)
- V8only "x @@ y" (at level 40, left associativity).
-
-b3) My notation is already defined at another level (or with another
-associativity)
-
-In V8, the level and associativity of a given notation can no longer
-be changed. Then, either you adopt the standard reserved levels and
-associativity for this notation (as given on the list above) or you
-change your notation.
-
-- To change the notation, follow the directions in section b2.
-
-- To adopt the standard level, just use V8only without any argument.
-
-Example.
-
-Infix 6 "*" my_mult.
-
-is not accepted as such in V8. Write
-
-Infix 6 "*" my_mult V8only.
-
-to tell the translator to use "*" at the reserved level (i.e. 40 with
-left associativity). Even better, use interpretation scopes (look at
-the Reference Manual).
-
-c) How to use V8only with Distfix ?
-
-You can't, use Notation instead of Distfix.
-
-d) Can I overload a notation in V8, e.g. use "*" and "+" for my own
-algebraic operations ?
-
-Yes, using interpretation scopes (see the corresponding chapter in the
-Reference Manual).
-
-3) Using the translator to have simplest notations
-
-Thanks to the new syntax, * has now the expected left associativity,
-and the symbols <, >, <= and >= are now available.
-
-Thanks to the interpretation scopes, you can overload the
-interpretation of these operators with the default interpretation
-provided in Coq.
-
-This may be a motivation to use the translator to automatically change
-the notations while switching to the new syntax.
-
-See sections b) and d) above for examples.
-
-4) Setting the translator to automatically use new notations that
-wasn't used in old syntax
-
-Thanks to the "Notation" mechanism, defining symbolic notations is
-simpler than in the previous versions of Coq.
-
-Thanks to the new syntax and interpretation scopes, new symbols and
-overloading is available.
-
-This may be a motivation for using the translator to automatically change
-the notations while switching to the new syntax.
-
-Use for that the commands V8Notation and V8Infix.
-
-Examples:
-
-V8Infix "==>" my_relation (at level 65, right associativity).
-
-tells the translator to write an infix "==>" instead of my_relation in
-the translated files.
-
-V8Infix ">=" my_ge.
-
-tells the translator to write an infix ">=" instead of my_ge in the
-translated files and that the level and associativity are the standard
-one (as defined in the chart above).
-
-V8Infix ">=" my_ge : my_scope.
-
-tells the translator to write an infix ">=" instead of my_ge in the
-translated files, that the level and associativity are the standard
-one (as defined in the chart above), but only if scope my_scope is
-open or if a delimiting key is available for "my_scope" (see the
-Reference Manual).
-
-5) Defining a construction and its notation simultaneously
-
-This is permitted by the new syntax. Look at the Reference Manual for
-explanation. The translator is not fully able to take this in charge...
-
-III) Various pitfalls
- ----------------
-
-1) New keywords
-
- The following identifiers are new keywords
-
- "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
- "else"; "return"; "mod"; "at"; "let"; "_"; ".("
-
- The translator automatically add a "_" to names clashing with a
-keyword, except for files. Hence users may need to rename the files
-whose name clashes with a keyword.
-
- Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type"
- were already keywords
-
-2) Old "Case" and "Match"
-
- "Case" and "Match" are normally automatically translated into
- "match" or "match" and "fix", but sometimes it fails to do so. It
- typically fails when the Case or Match is argument of a tactic whose
- typing context is unknown because of a preceding Intro/Intros, as e.g. in
-
- Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
-
- The solution is then to replace the invocation of the sequence of
- tactics into several invocation of the elementary tactics as follows
-
- Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
- ^^^
-
-3) Change of definition or theorem names
-
- Type "entier" from fast_integer.v is renamed into "N" by the
-translator. As a consequence, user-defined objects of same name "N"
-are systematically qualified even tough it may not be necessary. The
-same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
-TO GIVE].
-
-4) Change of tactics names
-
- Since tactics names are now lowercase, this can clash with
-user-defined tactic definitions. To pally this, clashing names are
-renamed by adding an extra "_" to their name.
-
-======================================================================
-Main examples for new syntax
-----------------------------
-
-1) Constructions
-
- Applicative terms don't any longer require to be surrounded by parentheses as
-e.g in
-
- "x = f y -> S x = S (f y)"
-
-
- Product is written
-
- "forall x y : T, U"
- "forall x y, U"
- "forall (x y : T) z (v w : V), U"
- etc.
-
- Abstraction is written
-
- "fun x y : T, U"
- "fun x y, U"
- "fun (x y : T) z (v w : V), U"
- etc.
-
- Pattern-matching is written
-
- "match x with c1 x1 x2 => t | c2 y as z => u end"
- "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end"
- "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with
- c1 x1 x2, _ => t | c2 y, d z => u end"
-
- The last example is the new form of what was written
-
- "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of
- (c1 x1 x2) _ => t | (c2 y) (d z) => u end"
-
- Pattern-matching of type with one constructors and no dependencies
-of the arguments in the resulting type can be written
-
- "let (x,y,z) as u return P u := t in v"
-
- Local fixpoints are written
-
- "fix f (n m:nat) z (x : X) {struct m} : nat := ...
- with ..."
-
- and "struct" tells which argument is structurally decreasing.
-
- Explicitation of implicit arguments is written
-
- "f @1:=u v @3:=w t"
- "@f u v w t"
-
-2) Tactics
-
- The main change is that tactics names are now lowercase. Besides
-this, the following renaming are applied:
-
- "NewDestruct" -> "destruct"
- "NewInduction" -> "induction"
- "Induction" -> "simple induction"
- "Destruct" -> "simple destruct"
-
- For tactics with occurrences, the occurrences now comes after and
- repeated use is separated by comma as in
-
- "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4"
- "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4"
- "Simpl 1 3 e" -> "simpl e at 1 3"
-
-3) Tactic language
-
- Definitions are now introduced with keyword "Ltac" (instead of
-"Tactic"/"Meta" "Definition") and are implicitly recursive
-("Recursive" is no longer used).
-
- The new rule for distinguishing terms from ltac expressions is:
-
- Write "ltac:" in front of any tactic in argument position and
- "constr:" in front of any construction in head position
-
-4) Vernacular language
-
-a) Assumptions
-
- The syntax for commands is mainly unchanged. Declaration of
-assumptions is now done as follows
-
- Variable m : t.
- Variables m n p : t.
- Variables (m n : t) (u v : s) (w : r).
-
-b) Definitions
-
- Definitions are done as follows
-
- Definition f m n : t := ... .
- Definition f m n := ... .
- Definition f m n := ... : t.
- Definition f (m n : u) : t := ... .
- Definition f (m n : u) := ... : t.
- Definition f (m n : u) := ... .
- Definition f a b (p q : v) r s (m n : t) : t := ... .
- Definition f a b (p q : v) r s (m n : t) := ... .
- Definition f a b (p q : v) r s (m n : t) := ... : t.
-
-c) Fixpoints
-
- Fixpoints are done this way
-
- Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... .
- Fixpoint f x : v := ... .
- Fixpoint f (x : t) : v := ... .
-
- It is possible to give a concrete notation to a fixpoint as follows
-
- Fixpoint plus (n m:nat) {struct n} : nat as "n + m" :=
- match n with
- | O => m
- | S p => S (p + m)
- end.
-
-d) Inductive types
-
- The syntax for inductive types is as follows
-
- Inductive t (a b : u) (d : e) : v :=
- c1 : w1 | c2 : w2 | ... .
-
- Inductive t (a b : u) (d : e) : v :=
- c1 : w1 | c2 : w2 | ... .
-
- Inductive t (a b : u) (d : e) : v :=
- c1 (x y : t) : w1 | c2 (z : r) : w2 | ... .
-
- As seen in the last example, arguments of the constructors can be
-given before the colon. If the type itself is omitted (allowed only in
-case the inductive type has no real arguments), this yields an
-ML-style notation as follows
-
- Inductive nat : Set := O | S (n:nat).
- Inductive bool : Set := true | false.
-
- It is even possible to define a syntax at the same time, as follows:
-
- Inductive or (A B:Prop) : Prop as "A \/ B":=
- | or_introl (a:A) : A \/ B
- | or_intror (b:B) : A \/ B.
-
- Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).
-
diff --git a/dev/doc/univpoly.txt b/dev/doc/universes.md
index ca3d520c70..c276603ed2 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/universes.md
@@ -1,11 +1,11 @@
-Notes on universe polymorphism and primitive projections, M. Sozeau
-===================================================================
+Notes on universe polymorphism
+------------------------------
-The new implementation of universe polymorphism and primitive
-projections introduces a few changes to the API of Coq. First and
-foremost, the term language changes, as global references now carry a
-universe level substitution:
+The implementation of universe polymorphism introduces a few changes
+to the API of Coq. First and foremost, the term language changes, as
+global references now carry a universe level substitution:
+~~~ocaml
type 'a puniverses = 'a * Univ.Instance.t
type pconstant = constant puniverses
type pinductive = inductive puniverses
@@ -15,30 +15,31 @@ type constr = ...
| Const of puniverses
| Ind of pinductive
| Constr of pconstructor
- | Proj of constant * constr
-
+~~~
Universes
-=========
+---------
- Universe instances (an array of levels) gets substituted when
+Universe instances (an array of levels) gets substituted when
unfolding definitions, are used to typecheck and are unified according
-to the rules in the ITP'14 paper on universe polymorphism in Coq.
+to the rules in the ITP'14 paper on universe polymorphism in Coq.
+~~~ocaml
type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *)
type Instance.t = Level.t array
type Universe.t = Level.t list (* hashconsed *)
+~~~
The universe module defines modules and abstract types for levels,
universes etc.. Structures are hashconsed (with a hack to take care
-of the fact that deserialization breaks sharing).
+of the fact that deserialization breaks sharing).
- Definitions (constants, inductives) now carry around not only
+ Definitions (constants, inductives) now carry around not only
constraints but also the universes they introduced (a Univ.UContext.t).
-There is another kind of contexts [Univ.ContextSet.t], the latter has
+There is another kind of contexts `Univ.ContextSet.t`, the latter has
a set of universes, while the former has serialized the levels in an
-array, and is used for polymorphic objects. Both have "reified"
-constraints depending on global and local universes.
+array, and is used for polymorphic objects. Both have "reified"
+constraints depending on global and local universes.
A polymorphic definition is abstract w.r.t. the variables in this
context, while a monomorphic one (or template polymorphic) just adds the
@@ -46,18 +47,18 @@ universes and constraints to the global universe context when it is put
in the environment. No other universes than the global ones and the
declared local ones are needed to check a declaration, hence the kernel
does not produce any constraints anymore, apart from module
-subtyping.... There are hence two conversion functions now: [check_conv]
-and [infer_conv]: the former just checks the definition in the current env
+subtyping.... There are hence two conversion functions now: `check_conv`
+and `infer_conv`: the former just checks the definition in the current env
(in which we usually push_universe_context of the associated context),
-and [infer_conv] which produces constraints that were not implied by the
+and `infer_conv` which produces constraints that were not implied by the
ambient constraints. Ideally, that one could be put out of the kernel,
-but currently module subtyping needs it.
+but currently module subtyping needs it.
Inference of universes is now done during refinement, and the evar_map
carries the incrementally built universe context, starting from the
-global universe constraints (see [Evd.from_env]). [Evd.conversion] is a
-wrapper around [infer_conv] that will do the bookkeeping for you, it
-uses [evar_conv_x]. There is a universe substitution being built
+global universe constraints (see `Evd.from_env`). `Evd.conversion` is a
+wrapper around `infer_conv` that will do the bookkeeping for you, it
+uses `evar_conv_x`. There is a universe substitution being built
incrementally according to the constraints, so one should normalize at
the end of a proof (or during a proof) with that substitution just like
we normalize evars. There are some nf_* functions in
@@ -67,16 +68,16 @@ the universe constraints used in the term. It is heuristic but
validity-preserving. No user-introduced universe (i.e. coming from a
user-written anonymous Type) gets touched by this, only the fresh
universes generated for each global application. Using
-
+~~~ocaml
val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
-
+~~~
Is the way to make a constr out of a global reference in the new API.
If they constr is polymorphic, it will add the necessary constraints to
the evar_map. Even if a constr is not polymorphic, we have to take care
of keeping track of its universes. Typically, using:
-
- mkApp (coq_id_function, [| A; a |])
-
+~~~ocaml
+ mkApp (coq_id_function, [| A; a |])
+~~~
and putting it in a proof term is not enough now. One has to somehow
show that A's type is in cumululativity relation with id's type
argument, incurring a universe constraint. To do this, one can simply
@@ -84,19 +85,19 @@ call Typing.resolve_evars env evdref c which will do some infer_conv to
produce the right constraints and put them in the evar_map. Of course in
some cases you might know from an invariant that no new constraint would
be produced and get rid of it. Anyway the kernel will tell you if you
-forgot some. As a temporary way out, [Universes.constr_of_global] allows
+forgot some. As a temporary way out, `Universes.constr_of_global` allows
you to make a constr from any non-polymorphic constant, but it will fail
on polymorphic ones.
Other than that, unification (w_unify and evarconv) now take account of universes and
produce only well-typed evar_maps.
-Some syntactic comparisons like the one used in [change] have to be
-adapted to allow identification up-to-universes (when dealing with
-polymorphic references), [make_eq_univs_test] is there to help.
+Some syntactic comparisons like the one used in `change` have to be
+adapted to allow identification up-to-universes (when dealing with
+polymorphic references), `make_eq_univs_test` is there to help.
In constr, there are actually many new comparison functions to deal with
that:
-
+~~~ocaml
(** [equal a b] is true if [a] equals [b] modulo alpha, casts,
and application grouping *)
val equal : constr -> constr -> bool
@@ -105,7 +106,7 @@ val equal : constr -> constr -> bool
application grouping and the universe equalities in [u]. *)
val eq_constr_univs : constr Univ.check_function
-(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
alpha, casts, application grouping and the universe inequalities in [u]. *)
val leq_constr_univs : constr Univ.check_function
@@ -120,47 +121,47 @@ val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained
(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and ignoring universe instances. *)
val eq_constr_nounivs : constr -> constr -> bool
-
-The [_univs] versions are doing checking of universe constraints
-according to a graph, while the [_universes] are producing (non-atomic)
+~~~
+The `_univs` versions are doing checking of universe constraints
+according to a graph, while the `_universes` are producing (non-atomic)
universe constraints. The non-atomic universe constraints include the
-[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2'
-*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are
-treated specially: as unfolding [f] might not result in these
+`ULub` constructor: when comparing `f (* u1 u2 *) c` and `f (* u1' u2'
+*) c` we add ULub constraints on `u1, u1'` and `u2, u2'`. These are
+treated specially: as unfolding `f` might not result in these
unifications, we need to keep track of the fact that failure to satisfy
them does not mean that the term are actually equal. This is used in
-unification but probably not necessary to the average programmer.
+unification but probably not necessary to the average programmer.
Another issue for ML programmers is that tables of constrs now usually
-need to take a [constr Univ.in_universe_context_set] instead, and
-properly refresh the universes context when using the constr, e.g. using
-Clenv.refresh_undefined_univs clenv or:
-
+need to take a `constr Univ.in_universe_context_set` instead, and
+properly refresh the universes context when using the constr, e.g. using
+Clenv.refresh_undefined_univs clenv or:
+~~~ocaml
(** Get fresh variables for the universe context.
Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set ->
+val fresh_universe_context_set_instance : universe_context_set ->
universe_level_subst * universe_context_set
-
-The substitution should be applied to the constr(s) under consideration,
+~~~
+The substitution should be applied to the constr(s) under consideration,
and the context_set merged with the current evar_map with:
-
+~~~ocaml
val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
-
-The [rigid] flag here should be [Evd.univ_flexible] most of the
+~~~
+The `rigid` flag here should be `Evd.univ_flexible` most of the
time. This means the universe levels of polymorphic objects in the
-constr might get instantiated instead of generating equality constraints
+constr might get instantiated instead of generating equality constraints
(Evd.univ_rigid does that).
-On this issue, I recommend forcing commands to take [global_reference]s
+On this issue, I recommend forcing commands to take `global_reference`s
only, the user can declare his specialized terms used as hints as
constants and this is cleaner. Alas, backward-compatibility-wise,
this is the only solution I found. In the case of global_references
-only, it's just a matter of using [Evd.fresh_global] /
-[pf_constr_of_global] to let the system take care of universes.
+only, it's just a matter of using `Evd.fresh_global` /
+`pf_constr_of_global` to let the system take care of universes.
The universe graph
-==================
+------------------
To accomodate universe polymorphic definitions, the graph structure in
kernel/univ.ml was modified. The new API forces every universe to be
@@ -176,68 +177,14 @@ no universe i can be set lower than Set, so the chain of universes
always bottoms down at Prop < Set.
Modules
-=======
+-------
One has to think of universes in modules as being globally declared, so
when including a module (type) which declares a type i (e.g. through a
parameter), we get back a copy of i and not some fresh universe.
-Projections
-===========
-
- | Proj of constant * constr
-
-Projections are always applied to a term, which must be of a record type
-(i.e. reducible to an inductive type [I params]). Type-checking,
-reduction and conversion are fast (not as fast as they could be yet)
-because we don't keep parameters around. As you can see, it's currently
-a [constant] that is used here to refer to the projection, that will
-change to an abstract [projection] type in the future. Basically a
-projection constant records which inductive it is a projection for, the
-number of params and the actual position in the constructor that must be
-projected. For compatibility reason, we also define an eta-expanded form
-(accessible from user syntax @f). The constant_entry of a projection has
-both informations. Declaring a record (under [Set Primitive
-Projections]) will generate such definitions. The API to declare them is
-not stable at the moment, but the inductive type declaration also knows
-about the projections, i.e. a record inductive type decl contains an
-array of terms representing the projections. This is used to implement
-eta-conversion for record types (with at least one field and having all
-projections definable). The canonical value being [Build_R (pn x)
-... (pn x)]. Unification and conversion work up to this eta rule. The
-records can also be universe polymorphic of course, and we don't need to
-keep track of the universe instance for the projections either.
-Projections are reduced _eagerly_ everywhere, and introduce a new Zproj
-constructor in the abstract machines that obeys both the delta (for the
-constant opacity) and iota laws (for the actual reduction). Refolding
-works as well (afaict), but there is a slight hack there related to
-universes (not projections).
-
-For the ML programmer, the biggest change is that pattern-matchings on
-kind_of_term require an additional case, that is handled usually exactly
-like an [App (Const p) arg].
-
-There are slight hacks related to hints is well, to use the primitive
-projection form of f when one does [Hint Resolve f]. Usually hint
-resolve will typecheck the term, resulting in a partially applied
-projection (disallowed), so we allow it to take
-[constr_or_global_reference] arguments instead and special-case on
-projections. Other tactic extensions might need similar treatment.
-
-WIP
-===
-
-- [vm_compute] does not deal with universes and projections correctly,
-except when it goes to a normal form with no projections or polymorphic
-constants left (the most common case). E.g. Ring with Set Universe
-Polymorphism and Set Primitive Projections work (at least it did at some
-point, I didn't recheck yet).
-
-- [native_compute] works with universes and projections.
-
-
Incompatibilities
-=================
+-----------------
Old-style universe polymorphic definitions were implemented by taking
advantage of the fact that elaboration (i.e., pretyping and unification)
@@ -247,33 +194,33 @@ possible, as unification ensures that the substitution is built is
entirely well-typed, even w.r.t universes. This means that some terms
that type-checked before no longer do, especially projections of the
pair:
-
+~~~coq
@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)).
-
+~~~
The "template universe polymorphic" variables i and j appear during
typing without being refreshed, meaning that they can be lowered (have
upper constraints) with user-introduced universes. In most cases this
won't work, so ?x and ?y have to be instantiated earlier, either from
the type of the actual projected pair term (some t : prod A B) or the
-typing constraint. Adding the correct type annotations will always fix
+typing constraint. Adding the correct type annotations will always fix
this.
Unification semantics
-=====================
+---------------------
In Ltac, matching with:
-- a universe polymorphic constant [c] matches any instance of the
+- a universe polymorphic constant `c` matches any instance of the
constant.
-- a variable ?x already bound to a term [t] (non-linear pattern) uses
+- a variable ?x already bound to a term `t` (non-linear pattern) uses
strict equality of universes (e.g., Type@{i} and Type@{j} are not
equal).
In tactics:
-- [change foo with bar], [pattern foo] will unify all instances of [foo]
- (and convert them with [bar]). This might incur unifications of
- universes. [change] uses conversion while [pattern] only does
+- `change foo with bar`, `pattern foo` will unify all instances of `foo`
+ (and convert them with `bar`). This might incur unifications of
+ universes. `change` uses conversion while `pattern` only does
syntactic matching up-to unification of universes.
-- [apply], [refine] use unification up to universes.
+- `apply`, `refine` use unification up to universes.
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt
deleted file mode 100644
index a40706e996..0000000000
--- a/dev/doc/universes.txt
+++ /dev/null
@@ -1,26 +0,0 @@
-How to debug universes?
-
-1. There is a command Print Universes in Coq toplevel
-
- Print Universes.
- prints the graph of universes in the form of constraints
-
- Print Universes "file".
- produces the "file" containing universe constraints in the form
- univ1 # univ2 ;
- where # can be either > >= or =
-
- If "file" ends with .gv or .dot, the resulting file will be in
- dot format.
-
-
- *) for dot see http://www.research.att.com/sw/tools/graphviz/
-
-
-2. There is a printing option
-
- {Set,Unset} Printing Universes.
-
- which, when set, makes all pretty-printed Type's annotated with the
- name of the universe.
-
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 3867d4af90..8f9c3171da 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -395,7 +395,17 @@ Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect pl
Coq V8.7 beta 2 & released 6 October 2017 & \\
-Coq V8.7 & released 18 October 2016 & \\
+Coq V8.7.0 & released 18 October 2017 & \\
+
+Coq V8.7.1 & released 15 December 2017 & \\
+
+Coq V8.7.2 & released 17 February 2018 & \\
+
+Coq V8.8 beta1 & released 19 March 2018 & \\
+
+Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\
+&& \feature{effort towards better documented, better structured ML API}\\
+&& \feature{miscellaneous changes/improvements of existing features}\\
\end{tabular}
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index b35571e9ca..48671c03b6 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -10,9 +10,9 @@ versions of Proof General.
A somewhat out-of-date description of the async state machine is
[documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md).
-OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli).
+OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml).
-Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt).
+Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md).
* [Commands](#commands)
- [About](#command-about)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 15:04:43 +0000