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