• OCaml version: 4.10 to 4.13 are useless

  • https://github.com/ocaml/ocaml/issues/9606 ocamldebug very slow (4.10 to 4.12)
  • https://github.com/ocaml/ocaml/issues/10517 ocamldebug bails if threads linked (4.12 and 4.13)
  • 4.14 alpha seems ok

• ocamldebug doc: https://ocaml.org/manual/debugger.html important commands: print, break, run/reverse, next/previous, step/backstep also useful: up/down finish/start

• compile Rocq: dune build rocq-runtime.install rocq-core.install.

Either

• run dune exec -- dev/dune-dbg coqc /tmp/foo.v (or other arguments instead of /tmp/foo.v) Alternatives to coqc are checker coqide and coqtop (see dev/dune-dbg.in, NB dune-dbg still uses "coq" instead of "rocq")

or

• run in emacs using coqdev-ocamldebug from dev/tools/coqdev.el (needed because Tuareg's ocamldebug adds -emacs -cd $PWD in the command so we would run dune -emacs -cd $PWD exec -- dev/dune-dbg coqc /tmp/foo.v, which doesn't work)

Then import printers using source dune_db (or dune_db_408 or dune_db_409 depending on OCaml version).

With the example of Elpi compiled with make ci-elpi:

• dune build dev/dune-dbg
• make ci-elpi
• dune exec --no-build -- dev/dune-dbg -I $PWD/_build_ci/elpi coqc test.v (in emacs, coqdev-ocamldebug prompts for the command so you can modify it accordingly) (-I goes between dune-dbg and coqc) where test.v contains eg

From elpi.apps Require Import NES.

NES.Begin This.Is.A.Long.Namespace.

• usual ocamldebug commands (setting breakpoints in elpi code won't work until it has been dynlinked)

Notes:

• if you forget --no-build or run any dune build, coq-elpi will be evicted from _build (not _build_ci/elpi/_build) so do make ci-elpi again
• add -I $OPAM_SWITCH_PREFIX/.opam-switch/sources/elpi.$elpi_version to the dune-dbg call (or do directory while in ocamldebug) if you want to step in elpi (as opposed to rocq-elpi) code (IDK why it can't use the sources installed at the findlib location $OPAM_SWITCH_PREFIX/lib/elpi)
• Maybe it would also make sense to automatically add -I for every directory in _build_ci?
• it would be nice to not need --no-build, but I don't know how to achieve that.

eg (break is at the beginning of check_may_eval, (ocd) is the ocamldebug prompt) if /tmp/foo.v contains Check Prop.:

(ocd) break @ "vernacentries" 1836
Loading program... done.
Breakpoint 1 at 5100824: file vernac/vernacentries.ml, line 1836, characters 3-1635
(ocd) run
Time: 13461033 - pc: 5100824 - module Vernacentries
Breakpoint: 1
1836   <|b|>let glopt = query_command_selector glopt in
(ocd) p rc
rc: Constrexpr.constr_expr = Prop

If run stops on loading modules, with messages like Module(s) Firstorder_plugin__Ground loaded, you are enjoying break_on_load, which lets you set breakpoints before code loading. If inconvenient, disable it with set break_on_load off.

Consider https://github.com/coq/coq/blob/87f54b09c80566736b30471590cd20f702ed0558/tactics/tactics.ml#L2178-L2195

let keep hyps =
  Proofview.Goal.enter begin fun gl ->
  Proofview.tclENV >>= fun env ->
  let ccl = Proofview.Goal.concl gl in
  let sigma = Tacmach.project gl in
  let cl,_ =
    fold_named_context_reverse (fun (clear,keep) decl ->
      let decl = map_named_decl EConstr.of_constr decl in
      let hyp = NamedDecl.get_id decl in
      if Id.List.mem hyp hyps
        || List.exists (occur_var_in_decl env sigma hyp) keep
        || occur_var env sigma hyp ccl
      then (clear,decl::keep)
      else (hyp::clear,keep))
      ~init:([],[]) (Proofview.Goal.env gl)
  in
  clear cl
  end

(Ltac clear calls keep [])

If we break before the Goal.enter, then next will send us into a bunch of Logic_monad internals and never show us tactics.ml again. step would get us back to tactics.ml after over 100 steps of uninteresting internals.

Instead we should just break on the let ccl = line where monadic computations stop and run to it.

This pattern of setting a breakpoint and running to the next place we want to see must be repeated for every monadic combinator (typically Goal.enter, >>=, and all the tclFOO).

If you forget and end up lost in internals, you can still set your desired breakpoint and run as long as you didn't use next to reach beyond it.