Skip to content

Commit

Permalink
Fix dune-dbg inside emacs with dune >= 3
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer authored and ana-borges committed Nov 15, 2022
1 parent e435f3c commit c4f5055
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 26 deletions.
59 changes: 34 additions & 25 deletions dev/dune-dbg.in
Original file line number Diff line number Diff line change
@@ -1,29 +1,38 @@
#!/usr/bin/env bash

# Run in a proper install dune env.
case $1 in
coqchk)
shift
exe=_build/default/checker/coqchk.bc
;;
coqide)
shift
exe=_build/default/ide/coqide/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,coqchk,coqide}"
exit 1
;;
esac

emacs="${INSIDE_EMACS:+-emacs}"
opts=()
while [[ $# -gt 0 ]]; do
case $1 in
-emacs)
shift
opts+=("-emacs")
;;
coqchk)
shift
exe=_build/default/checker/coqchk.bc
break
;;
coqide)
shift
exe=_build/default/ide/coqide/coqide_main.bc
break
;;
coqc)
shift
exe=_build/default/topbin/coqc_bin.bc
break
;;
coqtop)
shift
exe=_build/default/topbin/coqtop_byte_bin.bc
break
;;
*)
echo "usage: dune exec -- dev/dune-dbg [-emacs] {coqchk|coqide|coqc|coqtop} coqargs"
exit 1
;;
esac
done

ocamldebug $emacs $(ocamlfind query -recursive -i-format coq-core.top_printers) -I +threads -I dev $exe "$@"
ocamldebug "${opts[@]}" $(ocamlfind query -recursive -i-format coq-core.top_printers) -I +threads -I dev $exe "$@"
2 changes: 1 addition & 1 deletion dev/tools/coqdev.el
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ Note that this function is executed before _Coqproject is read if it exists."
(setq-local coq-prog-name (concat dir "_build/default/dev/shim/coqtop-prelude")))))
(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)

(defvar coqdev-ocamldebug-command "dune exec -- dev/dune-dbg coqc /tmp/foo.v"
(defvar coqdev-ocamldebug-command "dune exec -- dev/dune-dbg -emacs coqc /tmp/foo.v"
"Command run by `coqdev-ocamldebug'")

(declare-function comint-check-proc "comint")
Expand Down

0 comments on commit c4f5055

Please sign in to comment.