diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 34 | ||||
| -rw-r--r-- | dev/doc/changes.md | 7 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 15 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 3 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 5 |
5 files changed, 52 insertions, 12 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 37c6e2f619..cd35064b18 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -108,24 +108,44 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec -- dev/dune-dbg /path/to/foo.v +dune exec -- dev/dune-dbg coqc foo.v (ocd) source dune_db ``` -or +to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`: ``` -dune exec -- dev/dune-dbg checker Foo +dune exec -- dev/dune-dbg checker foo.vo (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. +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. For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. +**Note**: If you are using OCaml >= 4.08 you need to use + +``` +(ocd) source dune_db_408 +``` + +or + +``` +(ocd) source dune_db_409 +``` + +depending on your OCaml version. This is due to several factors: + +- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source` + is not re entrant and seems to doubly-load in the default setup, see + https://github.com/coq/coq/issues/8952 +- OCaml >= 4.09 comes with `dynlink` already linked in so we need to + modify the list of modules loaded. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 04b20c6889..3bc92e6aee 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,13 @@ ### 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. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been 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 1c486b024d..ba68501e04 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -75,7 +75,8 @@ in time. - [ ] Pin the versions of libraries and plugins in `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it exists, a branch dedicated to compatibility with the corresponding - Coq branch). + Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this + semi-automatically. - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The project should have a "Request X.X+beta1 inclusion" column for the PRs that were diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 0fc0a413ba..fca7b77fc2 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -1,12 +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. It will also be used in upcoming -versions of Proof General. +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). |