diff options
Diffstat (limited to 'dev/debugging.txt')
| -rw-r--r-- | dev/debugging.txt | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/dev/debugging.txt b/dev/debugging.txt index d3fbf48a..4c04c42f 100644 --- a/dev/debugging.txt +++ b/dev/debugging.txt @@ -12,15 +12,20 @@ Debugging from Coq toplevel using Caml trace mechanism 6. Test your Coq command and observe the result of tracing your functions 7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;' + Hints: To remove high-level pretty-printing features (coercions, + notations, ...), use "Set Printing All". It will affect the #trace + printers too. + Debugging from Caml debugger ============================ + Preferably use ocaml 3.06 (pretty-printing is broken with ocaml 3.07/3.08) Needs tuareg mode in Emacs Coq must be configured with -debug and -local (./configure -debug -local) 1. M-x camldebug - 2. give the binary name coqtop.byte - 3. give dev/ocamldebug-v7 + 2. give the binary name bin/coqtop.byte + 3. give ../dev/ocamldebug-coq 4. source db (to get pretty-printers) 5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml source @@ -36,8 +41,9 @@ Debugging from Caml debugger 7. some hints: - To debug a failure/error/anomaly, add a breakpoint in - Vernacinterp.call just before "if !Options.debug" then go "back" to - find where the failure/error/anomaly has been raised + Vernac.vernac_com at the with clause of the "try ... interp com + with ..." block, then go "back" a few steps to find where the + failure/error/anomaly has been raised - If "source db" fails, first recompile top_printers.ml with "make dev/top_printers.cmo" |