diff options
| author | Gaëtan Gilbert | 2018-10-26 13:30:01 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-26 13:30:01 +0200 |
| commit | e2096b9e6048bbab5c6da279bab3c3a719dc237f (patch) | |
| tree | 6e7fdcbd3b90334bdf0f6723dcee5eb65b5ba729 /dev/doc | |
| parent | 3b14b406807af5503471d4936dea4d5ed0e0c789 (diff) | |
| parent | f8881bcc694644700e20f475b0a36ec740b2547d (diff) | |
Merge PR #8744: [dune] Compile debug and checker printers.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 91ab57f1e9..0aeb30c4e8 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -68,6 +68,27 @@ Note that you must invoke the `#rectypes;;` toplevel flag in order to use Coq libraries. The provided `.ocamlinit` file does this automatically. +## ocamldebug + +You can use `ocamldebug` with Dune; after a build, do: + +``` +dune exec dev/dune-dbg +(ocd) source dune_db +``` + +or + +``` +dune exec dev/dune-dbg checker +(ocd) source checker_dune_db +``` + +for the checker. Unfortunately, dependency handling here is not fully +refined, so you need to build enough of Coq once to use this target +[it will then correctly compute the deps and rebuild if you call the +script again] This will be fixed in the future. + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages |