From f8881bcc694644700e20f475b0a36ec740b2547d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 16 Oct 2018 15:17:31 +0200
Subject: [dune] Compile debug and checker printers.

As noted by Gäetan, we didn't compile these. We also provide a recipe
to run `ocamldebug`. Try (after a build):

```
dune exec dev/dune-dbg
(ocd) source dune_db
```

or

```
dune exec dev/dune-dbg checker
(ocd) source checker_dune_db
```

for the checker.
---
 dev/doc/build-system.dune.md | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'dev/doc')

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
-- 
cgit v1.2.3