OCamldebug

Setup

• 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

• If you want to debug code in plugins: add the plugins you're interested in to the libraries for coqc_bin in topbin/dune so that they're statically linked. (should not be needed for OCaml 4.12+ but untested due to previously mentioned issues)

• compile Coq: dune build coq-core.install theories/Init/Prelude.vo.

• get files in _build/install: dune build until it says something (after that you can interrupt). You only need to do this once, files in _build/install are symlinked so will pick up new builds Alternatively just dune build until it finishes (but takes more time)

Run

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)

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).

Enjoy

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

break_on_load

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.

Debugging vs the tactic monad

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.