[dune] [dbg] Add support for coqtop in dune-dbg

We also workaround problem #11405 , however, this should be reverted
once the problem is fixed in OCaml upstream.

6 files changed, 91 insertions, 11 deletions

diff --git a/coq.opam b/coq.opam
index 6aec0132be..50f746abec 100644
--- a/coq.opam
+++ b/coq.opam
@@ -29,7 +29,6 @@ depends: [
 
 build: [
   [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
-  [ "dune" "build" "@vodeps" ]
-  [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ]
+  [ "make" "-f" "Makefile.dune" "voboot" ]
   [ "dune" "build" "-p" name "-j" jobs ]
 ]
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 37c6e2f619..cd35064b18 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -108,24 +108,44 @@ automatically.
 You can use `ocamldebug` with Dune; after a build, do:
 
 ```
-dune exec -- dev/dune-dbg /path/to/foo.v
+dune exec -- dev/dune-dbg coqc foo.v
 (ocd) source dune_db
 ```
 
-or
+to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`:
 
 ```
-dune exec -- dev/dune-dbg checker Foo
+dune exec -- dev/dune-dbg checker foo.vo
 (ocd) source 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.
+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.
 
 For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`.
 
+**Note**: If you are using OCaml >= 4.08 you need to use
+
+```
+(ocd) source dune_db_408
+```
+
+or
+
+```
+(ocd) source dune_db_409
+```
+
+depending on your OCaml version. This is due to several factors:
+
+- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source`
+  is not re entrant and seems to doubly-load in the default setup, see
+  https://github.com/coq/coq/issues/8952
+- OCaml >= 4.09 comes with `dynlink` already linked in so we need to
+  modify the list of modules loaded.
+
 ## Dropping from coqtop:
 
 After doing `make -f Makefile.dune voboot`, the following commands should work:
diff --git a/dev/dune b/dev/dune
index 11e42f97f3..b312a55706 100644
--- a/dev/dune
+++ b/dev/dune
@@ -13,6 +13,8 @@
         ../checker/coqchk.bc
         ../topbin/coqc_bin.bc
         ../ide/coqide_main.bc
-        ; This is not enough as the call to `ocamlfind` will fail :/
+        %{lib:coq.plugins.ltac:ltac_plugin.cma}
+        ; This is not enough, the call to `ocamlfind` may fail if the
+        ; META file is not yet in place :/
         top_printers.cma)
   (action (copy dune-dbg.in dune-dbg)))
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 1382f4d1b6..498f167eb1 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -7,11 +7,21 @@ case $1 in
         exe=_build/default/checker/coqchk.bc
         ;;
     coqide)
+        shift
         exe=_build/default/ide/coqide_main.bc
         ;;
-    *)
+    coqc)
+        shift
         exe=_build/default/topbin/coqc_bin.bc
         ;;
+    coqtop)
+        shift
+        exe=_build/default/topbin/coqtop_byte_bin.bc
+        ;;
+    *)
+        echo "First argument must be one of {coqc,coqtop,checker,coqide}"
+        exit 1
+        ;;
 esac
 
 emacs="${INSIDE_EMACS:+-emacs}"
diff --git a/dev/dune_db_408 b/dev/dune_db_408
new file mode 100644
index 0000000000..3bf13da62d
--- /dev/null
+++ b/dev/dune_db_408
@@ -0,0 +1,25 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer config.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer gramlib.cma
+load_printer byterun.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer vernac.cma
+load_printer stm.cma
+load_printer toplevel.cma
+
+load_printer ltac_plugin.cma
+load_printer top_printers.cma
+
+source top_printers.dbg
diff --git a/dev/dune_db_409 b/dev/dune_db_409
new file mode 100644
index 0000000000..1267fd5393
--- /dev/null
+++ b/dev/dune_db_409
@@ -0,0 +1,24 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer config.cma
+load_printer clib.cma
+load_printer lib.cma
+load_printer gramlib.cma
+load_printer byterun.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer vernac.cma
+load_printer stm.cma
+load_printer toplevel.cma
+
+load_printer ltac_plugin.cma
+load_printer top_printers.cma
+
+source top_printers.dbg