From 56b5d6792962a857f116a2fd62022fe7ae37ae19 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 22 May 2019 17:27:00 +0200
Subject: Better dune ocamldebug integration

- use coqc instead of coqtop (since -compile doesn't work anymore this
  is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users

The dune-dbg dependencies are still broken ;_;
---
 dev/doc/build-system.dune.md |  6 ++++--
 dev/dune                     |  4 ++--
 dev/dune-dbg.in              |  7 +++++--
 dev/tools/coqdev.el          | 29 +++++++++++++++++++++++++++++
 4 files changed, 40 insertions(+), 6 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 49251d61a1..372e40a0b7 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -108,14 +108,14 @@ automatically.
 You can use `ocamldebug` with Dune; after a build, do:
 
 ```
-dune exec dev/dune-dbg
+dune exec dev/dune-dbg /path/to/foo.v
 (ocd) source dune_db
 ```
 
 or
 
 ```
-dune exec dev/dune-dbg checker
+dune exec dev/dune-dbg checker Foo
 (ocd) source dune_db
 ```
 
@@ -124,6 +124,8 @@ 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`.
+
 ## Dropping from coqtop:
 
 After doing `make -f Makefile.dune voboot`, the following commands should work:
diff --git a/dev/dune b/dev/dune
index 792da6254a..ffa885a008 100644
--- a/dev/dune
+++ b/dev/dune
@@ -3,7 +3,7 @@
  (public_name coq.top_printers)
  (synopsis "Coq's Debug Printers")
  (wrapped false)
- (modules :standard)
+ (modules top_printers)
  (optional)
  (libraries coq.toplevel coq.plugins.ltac))
 
@@ -11,7 +11,7 @@
   (targets dune-dbg)
   (deps dune-dbg.in
         ../checker/coqchk.bc
-        ../topbin/coqtop_byte_bin.bc
+        ../topbin/coqc_bin.bc
         ; This is not enough as the call to `ocamlfind` will fail :/
         top_printers.cma)
   (action (copy dune-dbg.in dune-dbg)))
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 80ad0500e0..bd0a837938 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -3,11 +3,14 @@
 # Run in a proper install dune env.
 case $1 in
     checker)
+        shift
         exe=_build/default/checker/coqchk.bc
         ;;
     *)
-        exe=_build/default/topbin/coqtop_byte_bin.bc
+        exe=_build/default/topbin/coqc_bin.bc
         ;;
 esac
 
-ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe
+emacs="${INSIDE_EMACS:+-emacs}"
+
+ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@"
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index c6687b9731..b89ae67a82 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -85,6 +85,35 @@ Note that this function is executed before _Coqproject is read if it exists."
       (setq-local coq-prog-name (concat dir "bin/coqtop")))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)
 
+(defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg"
+  "Command run by `coqdev-ocamldebug'")
+
+(defun coqdev-ocamldebug ()
+  "Runs a command in an ocamldebug buffer."
+  (interactive)
+  (let* ((dir (read-directory-name "Run from directory: "
+                                   (coqdev-default-directory)))
+         (name "ocamldebug-coq")
+         (buffer-name (concat "*" name "*")))
+    (pop-to-buffer buffer-name)
+    (unless (comint-check-proc buffer-name)
+      (setq default-directory dir)
+      (setq coqdev-ocamldebug-command
+            (read-from-minibuffer "Command to run: "
+                                  coqdev-ocamldebug-command))
+      (let* ((cmdlist (tuareg--split-args coqdev-ocamldebug-command))
+             (cmdlist (mapcar #'substitute-in-file-name cmdlist)))
+        (apply #'make-comint name
+               (car cmdlist)
+               nil
+               (cdr cmdlist))
+        (set-process-filter (get-buffer-process (current-buffer))
+                            #'ocamldebug-filter)
+        (set-process-sentinel (get-buffer-process (current-buffer))
+                              #'ocamldebug-sentinel)
+        (ocamldebug-mode)))
+  (ocamldebug-set-buffer)))
+
 ;; This Elisp snippet adds a regexp parser for the format of Anomaly
 ;; backtraces (coqc -bt ...), to the error parser of the Compilation
 ;; mode (C-c C-c: "Compile command: ..."). File locations in traces
-- 
cgit v1.2.3