diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 3 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 18 |
2 files changed, 21 insertions, 0 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 5705857d76..3f1b470878 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -37,6 +37,9 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. +To know what files you are a code owner of in a large PR, you can run +`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect. + When a PR received lots of comments or if the PR has not been opened for long and the assignee thinks that some other developers might want to comment, it is recommended that they announce their intention to merge and wait a full diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index da91c85856..a31ab1c511 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -44,6 +44,24 @@ Dune will read the file `~/.config/dune/config`; see `man dune-config`. Among others, you can set in this file the custom number of build threads `(jobs N)` and display options `(display _mode_)`. +## Running binaries [coqtop / coqide] + +There are two special targets `states` and `quickide` that will +generate "shims" for running `coqtop` and `coqide` in a fast build. In +order to use them, do: + +``` +$ make -f Makefile.dune voboot # Only once per session +$ dune exec dev/shim/coqtop-prelude +``` + +or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets +enjoy quick incremental compilation thanks to `-opaque` so they tend +to be very fast while developing. + +Note that for a fast developer build of ML files, the `check` target +will be faster. + ## Targets The default dune target is `dune build` (or `dune build @install`), |