diff options
Diffstat (limited to 'dev/debugging.txt')
-rw-r--r-- | dev/debugging.txt | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/dev/debugging.txt b/dev/debugging.txt new file mode 100644 index 00000000..d3fbf48a --- /dev/null +++ b/dev/debugging.txt @@ -0,0 +1,50 @@ + +Debugging from Coq toplevel using Caml trace mechanism +====================================================== + + 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) + 2. Access Ocaml toplevel using vernacular command 'Drop.' + 3. Install load paths and pretty printers for terms, idents, ... using + Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer + term pretty printer) + 4. Use #trace to tell which function(s) to trace + 5. Go back to Coq toplevel with 'go();;' + 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();;' + +Debugging from Caml debugger +============================ + + 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 + 4. source db (to get pretty-printers) + 5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml + source + 6. get more help from ocamldebug manual + run + step + back + start + next + last + print x (abbreviated into p x) + ... + 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 + - If "source db" fails, first recompile top_printers.ml with + "make dev/top_printers.cmo" + +Profiling +========= + + Coq must be configured with option -profile + + 1. Run native Coq which must end normally (use Quit or option -batch) + 2. gprof ./coqtop gmon.out |