summaryrefslogtreecommitdiff
path: root/dev/doc/debugging.txt
blob: 2480b8edb325e7ded37556381ea01aa660ea58ff (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
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 
     installing the advanced term pretty printers)
  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();;'

  You can avoid typing #use "include" (or "base_include") after Drop
  by adding the following lines in your $HOME/.ocamlinit :

   if Filename.basename Sys.argv.(0) = "coqtop.byte"
   then ignore (Toploop.use_silently Format.std_formatter "include")

  Hints: To remove high-level pretty-printing features (coercions,
  notations, ...), use "Set Printing All". It will affect the #trace
  printers too.

Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled
with -rectypes are loaded in an environment with -rectypes set but
there is no way to tell the toplevel to support -rectypes. To make it
works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to
hack script/coqmktop.ml, then recompile coqtop.byte. The procedure
above then works as soon as coqtop.byte is called with at least one
argument (add neutral option -byte to ensure at least one argument).


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 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
   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
     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
   - Alternatively, for an error or an anomaly, add breakpoints in the middle  
     of each of error* functions or anomaly* functions in lib/util.ml
   - If "source db" fails, recompile printers.cma with
     "make dev/printers.cma" and try again

Global gprof-based 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

Per function profiling
======================

   1. To profile function foo in file bar.ml, add the following lines, just
      after the definition of the function:

     let fookey = Profile.declare_profile "foo";;
     let foo a b c = Profile.profile3 fookey foo a b c;;

     where foo is assumed to have three arguments (adapt using
     Profile.profile1, Profile. profile2, etc).

     This has the effect to cumulate the time passed in foo under a
     line of name "foo" which is displayed at the time coqtop exits.