blob: 6e48634835c42ce4309fa4aa08a3ad1163fa15d5 (
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
|
Debuggage
=========
dans Emacs. nécessite le mode tuareg.
Coq doit être configuré avec -debug et -local (./configure -debug -local)
1. M-x camldebug
2. spécifier le binaire bin/coqtop.byte
3. spécifier ../dev/ocamldebug-coq
4. source db (pour avoir les pretty-printers)
5. poser ses points d'arrêts avec C-x C-a C-b (penser "add breakpoint")
directement dans le source ocaml
6. ensuite voir le man d'ocamldebug
run
step
next
last
print x
...
Profiling
=========
Coq doit être configuré avec -profile
1. Lancer Coq en natif, qui doit terminer normalement (utiliser Quit
ou l'option -batch)
2. gprof ./coqtop gmon.out
|
