diff options
author | 2003-06-16 14:33:17 +0000 | |
---|---|---|
committer | 2003-06-16 14:33:17 +0000 | |
commit | ab6fc9808b47bc6f1a1916857568419ca06fc573 (patch) | |
tree | d0e47e0afb64bde40bf0887f4b8bb7340fabe6f4 /etc | |
parent | e57f9b2bd34d8f23dbfba30a1da58a4b846ffbcd (diff) |
Updated.
Diffstat (limited to 'etc')
-rw-r--r-- | etc/debugging-tips.txt | 35 |
1 files changed, 32 insertions, 3 deletions
diff --git a/etc/debugging-tips.txt b/etc/debugging-tips.txt index a5c43756..3b513146 100644 --- a/etc/debugging-tips.txt +++ b/etc/debugging-tips.txt @@ -1,5 +1,5 @@ -Tips for Debugging Proof General -- David Aspinall, 1999,2002 -=============================================================== +Tips for Debugging Proof General -- David Aspinall +==================================================== Emacs debug flags ================= @@ -11,10 +11,39 @@ 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 +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) ============================================== |