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