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