Debugging from Rocq toplevel using OCaml toplevel

Launch bytecode version of Rocq (dune exec -- dev/shim/coqtop.byte)
Access OCaml toplevel using vernacular command Drop.
Use #trace to tell which function(s) to trace, or type any other OCaml toplevel commands or OCaml expressions
Go back to Rocq toplevel with #quit;; or #go;;
Test your Rocq command and observe the result of tracing your functions
Freely switch from Rocq to OCaml toplevels with Drop. and #quit;;/#go;;

Note

To access plugin modules in the OCaml toplevel, you have to use names such as Ltac_plugin__Tacinterp.

Tip

To remove high-level pretty-printing features (coercions, notations, ...), use Set Printing All. It will affect the #trace printers too.

Debugging with ocamldebug from Emacs or command line

See build-system.dune.md#ocamldebug

Global gprof-based profiling

Rocq must be configured with option -profile.

Run native Rocq which must end normally (use Quit or option -batch)
gprof ./coqtop gmon.out

Per function profiling

See the documentation in lib/newProfile.mli.