[doc] [dune] Some tweaks from #13617

Tweaks to docs that are independent / unrelated to that PR.

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