diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 136 | ||||
| -rw-r--r-- | dev/doc/README.md | 77 | ||||
| -rw-r--r-- | dev/doc/changes.md | 227 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 6 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 262 | ||||
| -rw-r--r-- | dev/doc/proof-engine.md | 31 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 128 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 269 | ||||
| -rw-r--r-- | dev/doc/translate.txt | 495 | ||||
| -rw-r--r-- | dev/doc/versions-history.tex | 12 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 4 |
11 files changed, 846 insertions, 801 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md new file mode 100644 index 00000000..000f21c2 --- /dev/null +++ b/dev/doc/MERGING.md @@ -0,0 +1,136 @@ +# Merging changes in 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. + +When a PR is submitted, GitHub will automatically ask the principal +maintainer for a review. If the PR touches several parts, all the +corresponding principal maintainers 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. + +## Reviewing + +When maintainers receive a review request, they are expected to: + +* Put their name in the assignee field, if they are in charge of the component + that is the main target of the patch (or if they are the only maintainer asked + to review the PR). +* Review the PR, approve it or request changes. +* If they are the assignee, check if all reviewers approved the PR. If not, + regularly ping the author (if changes should be implemented) or the reviewers + (if reviews are missing). The assignee ensures that any requests for more + discussion have been granted. When the discussion has converged and ALL + 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. + +A maintainer is expected to be reasonably reactive, but no specific timeframe is +given for reviewing. + +(*) In case a component is touched in a trivial way (adding/removing one file in +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 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) 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 + +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](../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, 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 +- warn the author that they are going to rebase the branch, and push to the + branch directly + +In both cases, CI should be run again. + +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), 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 merge the PR proceed in the following way +``` +$ 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 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 00000000..223cf628 --- /dev/null +++ b/dev/doc/README.md @@ -0,0 +1,77 @@ +# 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 +$ 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 +``` + +## 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/changes.md b/dev/doc/changes.md index ab78b095..ca73cd63 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,205 @@ +## 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 + +Not handled yet. + +#### ARGUMENT EXTEND + +Not handled yet. + +#### 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,7 +218,7 @@ 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. @@ -44,8 +246,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 +265,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 +317,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/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e..764d4829 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 diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs new file mode 100644 index 00000000..8d78559c --- /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/proof-engine.md b/dev/doc/proof-engine.md index 8f96ac22..77455223 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 00000000..b33a1cbd --- /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 c48c2d5d..00000000 --- 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/translate.txt b/dev/doc/translate.txt deleted file mode 100644 index 5b372c96..00000000 --- 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/versions-history.tex b/dev/doc/versions-history.tex index 3867d4af..8f9c3171 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 b35571e9..48671c03 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) |