diff options
| author | Théo Zimmermann | 2018-11-20 19:51:02 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-11-20 19:51:02 +0100 |
| commit | 968be14b3788e112425eedf696f2e5e35d35ba17 (patch) | |
| tree | 81858592af623284fe47dba7816f1e2439e6d241 | |
| parent | 4449c990dee9980bb748988aa053f5462914cb3c (diff) | |
| parent | 9fe7007d1d071c3cc878822b27cdaf5d33defd7c (diff) | |
Merge PR #8948: [dune] Some tweaks to docs.
| -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 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 |