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