diff options
| -rw-r--r-- | dev/doc/build-system.dune.md | 6 | ||||
| -rw-r--r-- | dev/dune | 4 | ||||
| -rwxr-xr-x | dev/dune-dbg.in | 7 | ||||
| -rw-r--r-- | dev/tools/coqdev.el | 29 |
4 files changed, 40 insertions, 6 deletions
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: @@ -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 |