diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/README.md | 24 | ||||
| -rw-r--r-- | dev/doc/changes.md | 20 |
2 files changed, 22 insertions, 22 deletions
diff --git a/dev/doc/README.md b/dev/doc/README.md index c764455aed..bc281e0d94 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -2,27 +2,9 @@ ## 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 -``` +See the first section of [`INSTALL`](../../INSTALL). Developers are +recommended to use a recent OCaml version, which they can get through +opam or Nix, in particular. ## Building `coqtop` The general workflow is to first setup a development environment with diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 51d90df89f..ab9df12766 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -13,13 +13,31 @@ Proof state: Proofs that are attached to a top-level constant (such as lemmas) are represented by `Lemmas.t`, as they do contain additional - information related to the constant declaration. + information related to the constant declaration. Some functions have + been renamed from `start_proof` to `start_lemma` + Plugins that require access to the information about currently opened lemmas can add one of the `![proof]` attributes to their `mlg` entry, which will refine the type accordingly. See documentation in `vernacentries` for more information. + Proof `terminators` have been removed in favor of a principled + proof-saving path. This should not affect the regular API user, but + if plugin writes need special handling of the proof term they should + now work with Coq upstream to unsure the provided API does work and + is principled. Closing `hooks` are still available for simple + registration on constant save path, and essentially they do provide + the same power as terminators, but don't encourage their use other + than for simple tasks [such as adding a constant to a database] + + Additionally, the API for proof/lemma handling has been refactored, + triples have been split into named arguments, and a few bits of + duplicated information among layers has been cleaned up. Most proof + information is now represented in a direct-style, as opposed to it + living inside closures in previous Coq versions; thus, proof + manipulation possibilities have been improved. + ## Changes between Coq 8.9 and Coq 8.10 ### ML4 Pre Processing |