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
|
Debugging from Coq toplevel using Caml trace mechanism
======================================================
1. Launch bytecode version of Coq (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.
Debugging from Caml debugger
============================
Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
Coq must be configured with `-local` (`./configure -local`) and the
byte-code version of `coqtop` must have been generated with `make byte`.
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, do a "make printers" and try again (it should build
top_printers.cmo and the core cma files).
- If you build Coq with an OCaml version earlier than 4.06, and have the
OCAMLRUNPARAM environment variable set, Coq may hang on startup when run
from the debugger. If this happens, unset the variable, re-start Emacs, and
run the debugger 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
======================
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.
|
