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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
Tips for Debugging Proof General -- David Aspinall
====================================================
Emacs debug flags
=================
If Proof General gives an error, you can set the Emacs debug
flags to find out where in the code it occurs, showing a
stack trace.
On Emacs, check the boxes in the Options menu:
Options -> Enter Debugger on Error
Options -> Enter Debugger on Quit
On XEmacs you can find the check boxes under the menu Options ->
Troubleshooting.
You can also set these variables directly in lisp:
(setq debug-on-error t) ; debug on errors
(setq debug-on-quit t) ; debug on CTRL-G for looping code
You can make settings like this using M-x set-variable, or 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-:).
Debugging start-up problems
===========================
If you get an error when visiting a theorem prover file
(i.e. around the time that the splash screen appears), try
starting XEmacs normally:
xemacs -q -no-site-file
setting the debug flag:
M-x eval-expression RET (setq debug-on-error t) RET
and then visiting a theory file (e.g. empty Test.thy), *before*
loading Proof General. Load Proof General with the command:
M-x load-file <PATH-TO-ProofGeneral>/generic/proof-site.el
And then issue the command to switch the buffer into the mode
which is giving you problems, e.g.
M-x isar-mode RET
Hopefully this should produce a stack trace. (The stack trace
may otherwise be hidden, since some versions of Emacs try to
hide errors which occur when a file is visited).
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 edebug-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
|
