diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/INSTALL.make.md | 8 | ||||
| -rw-r--r-- | dev/doc/changes.md | 24 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 15 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 13 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 4 |
5 files changed, 55 insertions, 9 deletions
diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md index 3db5d0b14f..f81630c55d 100644 --- a/dev/doc/INSTALL.make.md +++ b/dev/doc/INSTALL.make.md @@ -102,6 +102,14 @@ Detailed Installation Procedure. it is recommended to compile in parallel, via make -jN where N is your number of cores. + If you wish to create timing logs for the standard library, you can + pass `TIMING=1` (for per-line timing files) or `TIMED=1` (for + per-file timing on stdout). Further variables and targets are + available for more detailed timing analysis; see the section of the + reference manual on `coq_makefile`. If there is any timing target + or variable supported by `coq_makefile`-made Makefiles which is not + supported by Coq's own Makefile, please report that as a bug. + 5. You can now install the Coq system. Executables, libraries, and manual pages are copied in some standard places of your system, defined at configuration time (step 3). Just do diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 04b20c6889..d5938713d6 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,25 @@ ### ML API +Types `precedence`, `parenRelation`, `tolerability` in +`notgram_ops.ml` have been reworked. See `entry_level` and +`entry_relative_level` in `constrexpr.ml`. + +### ML API + +Exception handling: + +- Coq's custom `Backtrace` module has been removed in favor of OCaml's + native backtrace implementation. Please use the functions in + `Exninfo.capture` and `iraise` when re-raising inside an exception + handler. + +- Registration of exception printers now follows more closely OCaml's + API, thus: + + + printers are of type `exn -> Pp.t option` [`None` == not handled] + + it is forbidden for exception printers to raise. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been @@ -10,6 +29,11 @@ Printers: Constrextern.extern_constr which were taking a boolean argument for the goal style now take instead a label. +Implicit arguments: + +- The type `Impargs.implicit_kind` was removed in favor of + `Glob_term.binding_kind`. + ## Changes between Coq 8.10 and Coq 8.11 ### ML API diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 2d187f7bae..3260040248 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -158,7 +158,7 @@ Universes component: universe polymorphism, asynchronous proofs summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one - impacted released: V8.5-V8.10 + impacted released versions: V8.5-V8.10 impacted development branches: none impacted coqchk versions: immune fixed in: PR#10664 @@ -167,6 +167,19 @@ Universes GH issue number: none risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + component: algebraic universes + summary: Set+2 was incorrectly simplified to Set+1 + introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a) + impacted released versions: V8.10.0 V8.10.1 V8.10.2 + impacted coqchk versions: same + fixed in: PR#11422 + found by: Gilbert + exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration) + GH issue number: see PR + risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic + universes such that +2 increments do not appear), mild risk from plugins which manipulate + algebraic universes. + Primitive projections component: primitive projections, guard condition diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index ba68501e04..58c2fcc68a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -127,11 +127,11 @@ in time. - [ ] Send an e-mail on Coqdev announcing that the tag has been put so that package managers can start preparing package updates (including a `coq-bignums` compatible version). -- [ ] Ping **@erikmd** to update the Docker images in `coqorg/coq` - (requires `coq-bignums` in `extra-dev` for a beta / in `released` - for a final release). +- [ ] When opening the corresponding PR for `coq` in the opam repository ([`coq/opam-coq-archive`](https://github.com/coq/opam-coq-archive) or [`ocaml/opam-repository`](https://github.com/ocaml/opam-repository)), + the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq) + (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built). - [ ] Draft a release on GitHub. -- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and +- [ ] 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)). @@ -139,8 +139,6 @@ in time. *TODO: setup some continuous deployment for this.* - [ ] Merge the website update, publish the release and send announcement e-mails. -- [ ] Ping **@Zimmi48** to publish a new version on Zenodo. - *TODO: automate this.* - [ ] Close the milestone ## At the final release time ## @@ -160,7 +158,10 @@ in time. Repeat the generic process documented above for all releases. +Ping `@Zimmi48` to: + - [ ] Switch the default version of the reference manual on the website. +- [ ] Publish a new version on Zenodo. ## At the patch-level release time ## diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index f0b8d6630f..fca7b77fc2 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -1,11 +1,11 @@ # Coq XML Protocol This document is based on documentation originally written by CJ Bell -for his [vscoq](https://github.com/siegebell/vscoq/) project. +for his [vscoq](https://github.com/coq-community/vscoq/) project. Here, the aim is to provide a "hands on" description of the XML protocol that coqtop and IDEs use to communicate. The protocol first appeared -with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/siegebell/vscoq/), and other user interfaces. +with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md). |