diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 15 | ||||
| -rw-r--r-- | dev/doc/changes.md | 20 |
2 files changed, 30 insertions, 5 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 3609171b82..01c32041d2 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,9 +10,9 @@ 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. +Usually, using the latest version of Dune 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 @@ -63,11 +63,16 @@ ml files in quick mode. Dune also provides targets for documentation, testing, and release builds, please see below. -## Documentation and test targets +## Documentation and testing targets Coq's test-suite can be run with `dune runtest`. -The documentation target is not implemented in Dune yet. +There is preliminary support to build the API documentation and +reference manual in HTML format, use `dune build {@doc,@refman-html}` +to generate them. + +So far these targets will build the documentation artifacts, however +no install rules are generated yet. ## Developer shell diff --git a/dev/doc/changes.md b/dev/doc/changes.md index c0f15f02a5..e7d4b605c7 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -52,6 +52,26 @@ Macros: where `atts : Vernacexpr.vernac_flags` was bound in the expression and had to be manually parsed. +Libobject + +- A Higher-level API for objects with fixed scope was introduced. It supports the following kinds of objects: + + * Local objects, meaning that objects cannot be imported from outside. + * Global objects, meaning that they can be imported (by importing the module that contains the object). + * Superglobal objects, meaning that objects survive to closing a module, and + are imported when the file which contains them is Required (even without + Import). + * Objects that survive section closing or don't (see `nodischarge` variants, + however we discourage defining such objects) + + This API is made of the following functions: + * `Libobject.local_object` + * `Libobject.local_object_nodischarge` + * `Libobject.global_object` + * `Libobject.global_object_nodischarge` + * `Libobject.superglobal_object` + * `Libobject.superglobal_object_nodischarge` + ## Changes between Coq 8.8 and Coq 8.9 ### ML API |