diff options
| author | Jim Fehrle | 2017-12-23 13:37:52 -0800 |
|---|---|---|
| committer | Théo Zimmermann | 2017-12-29 15:32:12 +0100 |
| commit | 2aeb740de93a0b32efe71bbd3a129e39bc6439e5 (patch) | |
| tree | 70160ddfb211aeed97d987a2bf1f451811300495 /dev/doc/debugging.md | |
| parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) | |
Add instructions for debugging from the command line (and in Windows)
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
Diffstat (limited to 'dev/doc/debugging.md')
| -rw-r--r-- | dev/doc/debugging.md | 27 |
1 files changed, 25 insertions, 2 deletions
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fa145d498a..fd3cbd1bc3 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -22,8 +22,8 @@ Debugging from Coq toplevel using Caml trace mechanism printers too. -Debugging from Caml debugger -============================ +Debugging with ocamldebug from Emacs +==================================== Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\ Coq must be configured with `-local` (`./configure -local`) and the @@ -59,6 +59,29 @@ Debugging from Caml debugger from the debugger. If this happens, unset the variable, re-start Emacs, and run the debugger again. +Debugging with ocamldebug from the command line +=============================================== + +In the `coq` directory: +1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq. +2. Run `make` (to compile the .v files) +3. Run `make byte` +4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH. + Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH. (The + CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.) +5. Run `dev/ocamldebug-coq bin/coqtop.byte` (on Cygwin/Windows, use `... bin/coqtop.byte.exe`) +6. Enter `source db` to load printers +7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc. +8. See the ocamldebug manual for more information. A few points: + - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml). + `break` can be abbreviated as `b`. + - `backtrace` or `bt` to see the call stack + - `step` or `s` goes into called functions; `next` or `n` skips over them + - `list` or `li` shows the code just before and after the current stack frame + - `print <var>` or `p <var>` to see the value of a variable +Note that `make byte` doesn't recompile .v files. `make` recompiles all of them if there +are changes in any .ml file--safer but much slower. + Global gprof-based profiling ============================ |