diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/README.md | 1 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 21 | ||||
| -rw-r--r-- | dev/doc/changes.md | 14 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 2 |
4 files changed, 29 insertions, 9 deletions
diff --git a/dev/doc/README.md b/dev/doc/README.md index 223cf6286e..c764455aed 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -16,7 +16,6 @@ $ opam init --comp <latest-ocaml-version> ~/.bashrc and ~/.ocamlinit files. $ source ~/.bashrc -$ opam install camlp5 # needed if you want to build "coqide" target diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index c5ea88aaf6..3609171b82 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,7 +10,8 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +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. Dune will get confused if it finds leftovers of in-tree compilation, @@ -49,14 +50,25 @@ The default dune target is `dune build` (or `dune build @install`), which will scan all sources in the Coq tree and then build the whole project, creating an "install" overlay in `_build/install/default`. -You can build some other target by doing `dune build $TARGET`. +You can build some other target by doing `dune build $TARGET`, where +`$TARGET` can be a `.cmxa`, a binary, a file that Dune considers a +target, an alias, etc... In order to build a single package, you can do `dune build $PACKAGE.install`. +A very useful target is `dune build @check`, that will compile all the +ml files in quick mode. + Dune also provides targets for documentation, testing, and release builds, please see below. +## Documentation and test targets + +Coq's test-suite can be run with `dune runtest`. + +The documentation target is not implemented in Dune yet. + ## Developer shell You can create a developer shell with `dune utop $library`, where @@ -139,11 +151,6 @@ Note that due to https://github.com/ocaml/dune/issues/1401 , we must perform a full rebuild each time as otherwise Dune will remove the files. We hope to solve this in the future. -## Documentation and test targets - -The documentation and test suite targets for Coq are still not -implemented in Dune. - ## Planned and Advanced features Dune supports or will support extra functionality that may result very diff --git a/dev/doc/changes.md b/dev/doc/changes.md index b1fdfafd3a..acb0d80c18 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,5 +1,15 @@ ## Changes between Coq 8.9 and Coq 8.10 +### ML4 Pre Processing + +- Support for `.ml4` files, processed by camlp5 has been removed in + favor of `.mlg` files processed by `coqpp`. + + Porting is usually straightforward, and involves renaming the + `file.ml4` file to `file.mlg` and adding a few brackets. + + See "Transitioning away from Camlp5" below for update instructions. + ### ML API General deprecation @@ -19,6 +29,10 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 +- `Names.transparent_state` has been moved to its own module `TransparentState`. + This module gathers utility functions that used to be defined in several + places. + Coqlib: - Most functions from the `Coqlib` module have been deprecated in favor of diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 764d482957..e5e4f740bd 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -94,7 +94,7 @@ Tacexpr.glob_tactic_expr | | Tacinterp.eval_tactic (?) V -Proof_type.tactic +Proofview.V82.tac TODO: check with Hugo |