aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/deboguage.txt
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