1 files changed, 65 insertions, 0 deletions
diff --git a/isa/BUGS b/isa/BUGS
new file mode 100644
index 00000000..b874a599
--- /dev/null
+++ b/isa/BUGS
@@ -0,0 +1,65 @@
+-*- mode:outline -*-
+
+* Isabelle Proof General Bugs
+
+See also ../BUGS for generic bugs.
+
+
+** Issues with tracing mode 
+
+1. Large volumes of output can cause Emacs to hog CPU spending
+all its time processing the output (esp with fontifying and X-symbol
+decoding).   It becomes difficult to use normal editing commands,
+even C-c C-c to interrupt the prover.  Workaround: hitting C-g,
+the Emacs quit key, will interrupt the prover in this state.
+See manual for further description of this.
+
+2. Interrupt response may be lost in large volumes of output, when
+using pty communication.  Symptom is interrupt on C-g, but PG thinks
+the prover is still busy.  Workaround: hit return in the shell buffer,
+or set proof-shell-process-connection-type to nil to use piped
+communication.
+
+** set proof_timing is problematic
+
+It will make the goals display disappear during proof.  This is
+because Proof General only displays goals output that appears *after*
+Isabelle messages, but Isabelle prints the timing message after the
+goals are displayed.
+
+** General difficulty with proof scripts containing ML structures, etc.  
+
+Proof General does not understand full ML syntax(!), so it will be
+confused by structures which contain semi-colons after declarations,
+for example.  Also, it cannot undo function declarations.  See the
+section on ML files in the manual for more details.
+
+** Blocking when processing multiple files, beginning from a .ML file.
+
+Proof General will block the Emacs process when it is waiting for a
+theory file (and it's ancestors) to be read as scripting is turned on.
+To avoid this, assert the theory file rather than the ML file.
+
+** Subsection Interaction with theory database
+
+Isabelle Proof General uses some support from Isabelle to remove and
+reload theories from the theory database.  To maintain consistency,
+Isabelle is rather conservative.  So re-asserting a retracted file will
+often re-load it, even if it has not changed.  (This is because the
+file may have implicit dependencies on things in the global ML
+environment not made apparent by the theory structure).  
+This may lead to seemingly unnecessary repetition of time-consuming
+proofs, so be careful not to retract more than you need!
+
+As of Isabelle 99-1 and Proof General 3.2, there should be much
+less unncessary re-loading of theories; be careful to use Isabelle's
+mechanisms of declaring dependencies in theory file headers.
+
+** Clash with SML mode
+
+Since Isabelle proof scripts are not differentiated from `.ML' files,
+Proof General may compete with `sml-mode' (if you use it) for
+controlling these buffers.  To ensure Proof General wins, load it last.
+
+Workaround: use another extension for real ML files, e.g.  `.sml',
+and disable `.ML' from entering `sml-mode'.