diff options
| author | Emilio Jesus Gallego Arias | 2018-11-08 14:50:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-08 16:56:13 +0100 |
| commit | 9fe7007d1d071c3cc878822b27cdaf5d33defd7c (patch) | |
| tree | 9ddc8bb29b53f81f138b06fe447a677ffd2722b2 /dev/doc | |
| parent | 108c15b51a7d5f647c8681fe7a37c86f0c5a8b9c (diff) | |
[dune] Some tweaks to docs.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0aeb30c4e8..cdb6f9d6c0 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 |