diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-23 12:24:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-23 12:24:29 +0000 |
| commit | af93a4a3640123e1a5acacaab0db9d9a8983613b (patch) | |
| tree | 30ae03cd0db4f039dcf846c23d417d1639b73430 /dev/debugging.txt | |
| parent | 91c0f3e4d91ac285fe23ac80a5d24e5e42c36da9 (diff) | |
MAJ coq v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6495 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/debugging.txt')
| -rw-r--r-- | dev/debugging.txt | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/dev/debugging.txt b/dev/debugging.txt index d3fbf48a0..56cfe6463 100644 --- a/dev/debugging.txt +++ b/dev/debugging.txt @@ -15,12 +15,13 @@ Debugging from Coq toplevel using Caml trace mechanism Debugging from Caml debugger ============================ + Needs ocaml 3.06 (broken with ocaml 3.07 and 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 +37,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" |