diff options
| -rw-r--r-- | configure.ml | 2 | ||||
| -rw-r--r-- | dev/README | 30 | ||||
| -rw-r--r-- | dev/doc/debugging.md | 27 |
3 files changed, 41 insertions, 18 deletions
diff --git a/configure.ml b/configure.ml index 06aa5e766..97dc14c00 100644 --- a/configure.ml +++ b/configure.ml @@ -1056,7 +1056,7 @@ let _ = print_summary () let write_dbg_wrapper f = safe_remove f; - let o = open_out f in + let o = open_out_bin f in (* _bin to avoid adding \r on Cygwin/Windows *) let pr s = fprintf o s in pr "#!/bin/sh\n\n"; pr "###### ocamldebug-coq : a wrapper around ocamldebug for Coq ######\n\n"; diff --git a/dev/README b/dev/README index b446c3e97..6b83579de 100644 --- a/dev/README +++ b/dev/README @@ -1,4 +1,4 @@ -This directory contains informations and tools to help developing the +This directory contains information and tools to help develop the Coq system ====================== @@ -6,30 +6,30 @@ This directory contains informations and tools to help developing the Debugging and profiling (in current directory - see doc/debugging.txt) ----------------------- -ocamldebug-coq: to launch ocaml debugger +ocamldebug-coq: to launch ocaml debugger (generated by the configure script) -db: to install pretty-printers from ocaml debugger -base_db: to install raw pretty-printers from ocaml debugger +db: to install pretty-printers from ocaml debugger +base_db: to install raw pretty-printers from ocaml debugger -include: to install pretty-printers from ocaml toplevel +include: to install pretty-printers from ocaml toplevel (use with the coq Drop command) base_include: to install raw pretty-printers from ocaml toplevel -vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging +vm_printers.ml, top_printers.ml: ML pretty-printers for debugging -Miscellaneous informations about the code (directory doc) +Miscellaneous information about the code (directory doc) ----------------------------------------- -changes.txt: (partial) per-version summary of the evolutions of Coq ML source -style.txt: a few style recommendations for writing Coq ML files -debugging.txt: help for debugging or profiling -universes.txt: help to debug universes -translate.txt: help to use coq translator +changes.md: (partial) per-version summary of the evolution of Coq ML source +style.txt: a few style recommendations for writing Coq ML files +debugging.md: help for debugging or profiling +universes.txt: help for debugging universes +translate.txt: help for using coq translator extensions.txt: some help about TACTIC EXTEND -header: standard header for Coq ML files -perf-analysis: analysis of perfs measured on the compilation of user contribs -cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation +header: standard header for Coq ML files +perf-analysis: analysis of perfs measured on the compilation of user contribs +cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fa145d498..fd3cbd1bc 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 ============================ |