diff options
Diffstat (limited to 'dev/doc/build-system.dune.md')
| -rw-r--r-- | dev/doc/build-system.dune.md | 38 |
1 files changed, 31 insertions, 7 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index de3d5a3d15..8ebd6b5073 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,17 +10,23 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -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. +Usually, using the latest version of Dune is recommended, see the +first line of the `dune-project` file for the minimum required +version. + +It is strongly recommended that you use the helper targets available +in `Makefile.dune`, `make -f Makefile.dune` will display help. Note +that dune will call configure for you if needed, so no need to call +`./configure` in the regular development workflow. + +`dune build @install` will build all the public Coq artifacts; `dune +build` will build all the targets in the workspace, including tests +and documentations. 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 the make-based system. -More helper targets are available in `Makefile.dune`, `make -f -Makefile.dune` will display some help. - Dune places build artifacts in a separate directory `_build`; it will also generate an `.install` file so files can be properly installed by package managers. @@ -84,7 +90,11 @@ builds, please see below. ## Documentation and testing targets -Coq's test-suite can be run with `dune runtest`. +Coq's test-suite can be run with `dune runtest`; given that `dune` +still invokes the test-suite makefile, the environment variable +`NJOBS` will control the value of the `-j` option that is passed to +make; common call `NJOBS=8 dune runtest`. This will be resolved in the +future once the test suite is ported to Dune rules. There is preliminary support to build the API documentation and reference manual in HTML format, use `dune build {@doc,@refman-html}` @@ -229,3 +239,17 @@ useful to Coq, some examples are: implicitly loaded plugins / vo files. See the "Running binaries [coqtop / coqide]" section above as to how to correctly call Coq's binaries. + +## Dune cheat sheet + +- `dune build` build all targets in the current workspace +- `dune build @check` build all ML targets as fast as possible, setup merlin +- `dune utop $dir` open a shell for libraries in `$dir` +- `dune exec -- $file` build and execute binary `$file`, can be in path or be an specific name +- `dune build _build/$context/$foo` build target `$foo$` in `$context`, with build dir layout +- `dune build _build/install/$context/foo` build target `$foo$` in `$context`, with install dir layout + +### packaging: + +- `dune subst` generate metadata for a package to be installed / distributed, necessary for opam +- `dune build -p $pkg` build a package in release mode |