← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to dev/doc/debugging.txt

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
dev/doc/debugging.txt
 
1
Debugging from Coq toplevel using Caml trace mechanism
 
2
======================================================
 
3
 
 
4
  1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
 
5
  2. Access Ocaml toplevel using vernacular command 'Drop.'
 
6
  3. Install load paths and pretty printers for terms, idents, ... using
 
7
     Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer
 
8
     term pretty printer)
 
9
  4. Use #trace to tell which function(s) to trace
 
10
  5. Go back to Coq toplevel with 'go();;'
 
11
  6. Test your Coq command and observe the result of tracing your functions
 
12
  7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;'
 
13
 
 
14
  Hints: To remove high-level pretty-printing features (coercions,
 
15
  notations, ...), use "Set Printing All". It will affect the #trace
 
16
  printers too.
 
17
 
 
18
Debugging from Caml debugger
 
19
============================
 
20
 
 
21
   Needs tuareg mode in Emacs
 
22
   Coq must be configured with -debug and -local (./configure -debug -local)
 
23
 
 
24
   1. M-x camldebug
 
25
   2. give the binary name bin/coqtop.byte
 
26
   3. give ../dev/ocamldebug-coq
 
27
   4. source db  (to get pretty-printers)
 
28
   5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml
 
29
      source
 
30
   6. get more help from ocamldebug manual
 
31
         run
 
32
         step
 
33
         back
 
34
         start
 
35
         next
 
36
         last
 
37
         print x (abbreviated into p x)
 
38
         ...
 
39
   7. some hints: 
 
40
 
 
41
   - To debug a failure/error/anomaly, add a breakpoint in
 
42
     Vernac.vernac_com at the with clause of the "try ... interp com
 
43
     with ..." block, then go "back" a few steps to find where the
 
44
     failure/error/anomaly has been raised
 
45
   - Alternatively, for an error or an anomaly, add breakpoints in the middle  
 
46
     of each of error* functions or anomaly* functions in lib/util.ml
 
47
   - If "source db" fails, recompile printers.cma with
 
48
     "make dev/printers.cma" and try again
 
49
 
 
50
Global gprof-based profiling
 
51
============================
 
52
 
 
53
   Coq must be configured with option -profile
 
54
 
 
55
   1. Run native Coq which must end normally (use Quit or option -batch)
 
56
   2. gprof ./coqtop gmon.out
 
57
 
 
58
Per function profiling
 
59
======================
 
60
 
 
61
   1. To profile function foo in file bar.ml, add the following lines, just
 
62
      after the definition of the function:
 
63
 
 
64
     let fookey = Profile.declare_profile "foo";;
 
65
     let foo a b c = Profile.profile3 fookey foo a b c;;
 
66
 
 
67
     where foo is assumed to have three arguments (adapt using
 
68
     Profile.profile1, Profile. profile2, etc).
 
69
 
 
70
     This has the effect to cumulate the time passed in foo under a
 
71
     line of name "foo" which is displayed at the time coqtop exits.