blob: 4c04c42fbe6f498b7ed5162f55a5de70cf55c92d (
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
|
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();;'
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
============================
Preferably use ocaml 3.06 (pretty-printing is broken with ocaml 3.07/3.08)
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
- 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
|
