Tips for Debugging Proof General
This is based on the file
etc/debugging-tips.txt
distributed with Proof General.
Set the 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. Please do this when running with
interpreted byte code, run
make clean
first.
On Emacs, check the boxes in the menu
Options -> Enter Debugger on Error
Options -> Enter Debugger on Quit
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 Emacs without startup files:
emacs -q -no-site-file
setting the debug flag using the menu or evauating lisp:
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 /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
.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