blob: a5c43756a806e97a102ba1ac57d24f746d00c9e6 (
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
|
Tips for Debugging Proof General -- David Aspinall, 1999,2002
===============================================================
Emacs debug flags
=================
If Proof General gives an error, you can set the Emacs debug
flag to find out where in the code it occurs, showing a
stack trace:
(setq debug-on-error t) ; debug on errors
(setq debugon-on-quit t) ; debug on CTRL-G for looping code
You can make settings like this using M-x set-variable, writing Lisp
code as above in the *scratch* buffer, and typing C-x C-e to evaluate
the expressions, or using M-x eval-expression (ESC-:).
Quick hints for edebug (source-level debugger)
==============================================
Source-level debugging is more useful than backtraces, especially if
you are writing your own additions for Proof General.
Load the source file <foo>.el, and locate the function you
want to debug. Type
M-x debug-defun RET
to instrument it for debugging.
When the code reaches the function it will enter the source-level
debugger. Keep pressing space to step through and see the result of
evaluating sub-expressions, or hit "c" to continue.
Pressing ? gives more commands.
Proof General debug messages
============================
Proof General includes internal debugging messages.
Make these settings to see them:
(setq proof-tidy-response nil) ; response buffer never clears
(setq proof-show-debug-messages t) ; debug messages appear in response buffer
|
