New/updated information files

1 files changed, 120 insertions, 190 deletions

diff --git a/BUGS b/BUGS
index f0ee6118..5ff3c5ed 100644
--- a/BUGS
+++ b/BUGS
@@ -1,207 +1,137 @@
-Known Bugs and Workarounds for Proof General.
-=============================================
+-*- outline -*-
 
-Contact:  proofgen@dcs.ed.ac.uk
+* Known Bugs and Workarounds for Proof General.
+
+Contact:  mailto:proofgen@dcs.ed.ac.uk
 See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS
 
+Generic bugs are listed here, which may affect all of the supported
+provers.  See lego/BUGS coq/BUGS, etc, for specific bug lists for each
+of the provers supported.
+
+* Proof General 3.0 BUGS addendum (fixed in current pre-rel)
+
+** FSF Emacs: problem with version 20.5
+
+  PG freezes when starting a proof assistant.  
+  Fixed in the current pre-release.
+
+** Problems with Japanese versions of FSF Emacs (at least) 
 
-Proof General 3.0 BUGS addendum
-===============================
+  These have older versions of CL macros (defined in file "egg")
+  with Japanese documentation.
+  Hopefully fixed in current pre-release, please send in details of
+  any problems!
 
-* FSF Emacs: problem with version 20.5: PG freezes when starting a
-proof assistant.  Fixed in the current pre-release.
+** You may occasionally see duplications of short (<10 chars)
+ messages from the proof assistant.  This is caused by a too high
+ setting of the configuration variable
+ proof-shell-eager-annotation-start-length.  
+ Fixed in current pre-release.
 
-* Problems with Japanese versions of FSF Emacs (at least) which have
-older versions of CL macros (defined in file "egg").  Hopefully fixed
-in current pre-release, please send in details of any problems!
 
 
 
 
-Generic problems
-================
 
-* If you have problems using Mule versions of FSF Emacs (beware
-setting standard-display-european): Pascal Brisset suggests adding
-this line to .emacs should help:
+* Generic problems
+
+** If you have problems using Mule versions of FSF Emacs 
+
+Beware setting standard-display-european: Pascal Brisset suggests
+adding this line to .emacs should help:
 
    (setq process-coding-system-alist '(("" . no-conversion))) 
 
-* If the proof assistant goes into a loop displaying lots of
-information, it may be difficult or impossible to interrupt it,
-because Emacs doesn't get a chance to process the C-c C-c keypress
-or "Stop" button push (or anything else).  In this situation, you
-will need to send an interrupt to the (e.g.) Isabelle process from
-another shell.  This problem can happen with looping rewrite rules in
-the Isabelle simplifier, when tracing rewriting.
-
-* Highlighting script buffers in recent versions of FSF Emacs is a
-mess.  The underlying text property implementation has changed
-and it seems difficult to get the desired behaviour of highlighting
-now.   Workaround: switch to using XEmacs.
-
-* If you use C-x C-v or C-x C-w on a script file which is in active
-scripting mode, Proof General will lose track of the file.
-Workaround: always turn off active scripting first with C-c C-s.
-
-* Toolbar enablers for XEmacs 21: since these have been switched on,
-it is apparent that the recognition of completed proofs may be
-unreliable (it wasn't used before).  Also there is a timing issue,
-so that occasionally the buttons are disabled/enabled when they
-shouldn't be.  An extra click on the toolbar solves this.
-
-* Ordinary undo in the script buffer can edit the "uneditable region"
-in XEmacs.  This doesn't happen in FSFmacs.  Test case:
+** If the proof assistant goes into a loop displaying lots of information
+
+It may be difficult or impossible to interrupt it, because Emacs
+doesn't get a chance to process the C-c C-c keypress or "Stop" button
+push (or anything else).  In this situation, you will need to send an
+interrupt to the (e.g.) Isabelle process from another shell.  This
+problem can happen with looping rewrite rules in the Isabelle
+simplifier, when tracing rewriting.
+
+** Do not use C-x C-v or C-x C-w on a script file in active scripting mode
+
+ Proof General will lose track of the file.
+ Workaround: always turn off active scripting first with C-c C-s.
+
+** Toolbar enablers for XEmacs 21, some artefacts.
+
+ There is a timing issue, so that occasionally the buttons are
+ disabled/enabled when they shouldn't be.  An extra click on the
+ toolbar solves this.
+
+** Ordinary undo in the script buffer can edit the "uneditable region"
+
+  In XEmacs.  This doesn't happen in FSFmacs.  Test case:
   Insert some nonsense text after the locked region.
   Kill the line. Process to the next command.
   Press C-x u, nonsense text appears in locked region.
-Workaround: take care with undo in XEmacs.
-
-* In FSFmacs, when proof-strict-read-only is set and font lock 
-is switched on, spurious "Region read only" errors are given
-which break font lock.   
-Workaround: turn off proof-strict-read-only, font-lock, or for
-the best of all possible worlds, switch to XEmacs.
-
-* As of FSFmacs 20.3, multi-byte character codes are used.  This
-breaks some of the code in Proof General, which is turned off in
-case the suspicious looking function toggle-enable-multibyte-characters 
-is present.  The code that is turned off deals with term markup
-for proof by pointing, which only affects LEGO at the moment.
-This problem could affect forthcoming versions of XEmacs (but hasn't
-as far as XEmacs 21.1).  Can anybody tell me if it affects Mule
-versions of Emacs?
-Workaround: for LEGO pbp, use FSFmacs 20.2, or XEmacs 20.4/later.
-
-* Using C-g can leave script management in a mess.  The code
-needs to have some regions protected from Emacs interrupts.
-Workaround: Don't type C-g while script management is processing.  
-If you do, use proof-restart-scripting.
-
-* Outline-mode does not work in processed proof script files due to
-read-only restrictions of the protected region.  This is an inherent
-problem with outline because it works by modifying the buffer.
-Workaround: none, nevermind.  (If it's hugely needed we could support
-modified outline commands).
-
-* Multiple file handling for Lego and Isabelle is slightly vulnerable.
-Files are not locked when they are being read by the prover, so a long
-file could be edited and saved as the prover is processing it,
-resulting in a loss of synchronization between Emacs and the proof
-assistant.  Files ought to be coloured red while they are being
-processed, just as single lines are.   Workaround: be careful not
-to edit a file as it is being read by the proof assistant!
-
-* XEmacs sometimes has strange start-up delays of several seconds,
-possibly due to face allocation, when running remotely and
-displaying on an 8-bit display.  One workaround (and in fact the
-recommended way of working) is to run XEmacs locally and only
-the proof assistant on your fast compute server, by setting 
-proof-rsh-command.
-
-* When proof-rsh-command is set to "ssh host" and you issue Ctrl-c to
-interrupt, the whole process may be killed instead of interrupted.
-This isn't a bug in Proof General, but the behaviour of ssh.  Try
-using rsh instead, it is said to forward signals to the remote command.
-
-* In tty mode, the binding C-c C-RET has no effect.  
-Workaround: manually bind C-c RET to 'proof-goto-point instead.
-
-* You may occasionally see duplications of short (<10 chars)
-messages from the proof assistant.  This is caused by a too high
-setting of the configuration variable
-proof-shell-eager-annotation-start-length.  
-Add (setq proof-shell-eager-annotation-start-length 1) to your .emacs
-if it bothers you badly.  This fix will be made in the next
-pre-release phase, it was too late to make it in time for testing for
-release 3.0.
-
-
-LEGO Proof General Bugs
-=======================
-
-* PBP doesn't work on FSF, see note above.
-
-* [FSF specific] `proof-zap-commas-region' does not work for Emacs
-  20.2 on lego/example.l . On *initially* fontifying the buffer,
-  commas are not zapped [unfontified]. However, when entering text,
-  commata are zapped correctly. Workaround: don't stare too much at commata
-
-* If LEGO attempts to write a (object) file in a non-writable
-  directory, it forgets the protocol mechanism on how to interact with 
-  Proof General and gets stuck. Workaround: Directly enter "Configure
-  AnnotateOn" in the Proof Shell to recover.
-
-* After a `Discharge', retraction ought to only be possible back to
-the first declaration/definition which is discharged. However, LEGO
-Proof General does not know that Discharge has such a non-local
-effect.  Workaround: retract back to the first
-declaration/definition which is discharged.
-
-* A thorny issue is local definitions in a proof state. LEGO cannot
-undo them explicitly. Workaround: retract back to a command before a
-definition.
-
-* Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone
-in a proof state by the Proof General. Workaround: retract back to the
-start of the proof.
-
-* After LEGO has issued a `*** QED ***' you may undo steps in the proof
-as long as you don't issue a `Save' command or start a new proof. The
-LEGO Proof General assumes that all proofs are terminated with a
-proper `Save' command. Workaround: Always issue a `Save' command after
-completing a proof. If you forget one, you should retract to a point
-before the offending proof development.
-
-*legotags doesn't find all declarations. It cannot handle lists e.g.,
-with [x,y:nat]; it only tags x but not y. [The same problem exists for
-coqtags] Workaround: don't rely too much on the etags mechanism.
-
-
-Coq Proof General Bugs
-======================
-
-* coqtags doesn't find all declarations. It cannot handle lists e.g.,
-with "Parameter x,y:nat" it only tags x but not y. [The same problem
-exists for legotags] Workaround: don't rely too much on the etags
-mechanism.
-
-* User defined tactics cannot be retracted. Workaround: you may need
-to retract to the beginning of the proof.
-
-* Surely others that aren't mentioned here.  Please report them
-to proofgen@dcs.ed.ac.uk.
-
-
-Isabelle Proof General Bugs
-===========================
-
-* 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.
-
-* There is a general difficulty with proof scripts containing ML
-structures, functions, 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.
-
-
-Isabelle and Isabelle/Isar Proof General Bugs
-=============================================
-
-* We've heard from one user that there are problems using 
-Proof General with Isabelle compiled under MLWorks for Sun
-Ultra/Solaris2.7.  These may be to do with the piped 
-communication mechnism; perhaps MLWorks doesn't flush the
-output after printing prompts.  If anyone discovers this,
-a possible work-around is to set process-connection-type to
-t instead of nil in proof-shell.el.  Please report to
-proofgen@dcs.ed.ac.uk if you try this!
+  Workaround: take care with undo in XEmacs.
+
+** In FSFmacs, spurious "Region read only" errors
+
+ When proof-strict-read-only is set and font lock is on, these
+ errors are given which break font lock.   
+ Workaround: turn off proof-strict-read-only, font-lock, or for
+ the best of all possible worlds, switch to XEmacs.
+
+** As of FSFmacs 20.3, multi-byte character codes are used.  
+
+  This breaks some of the code in Proof General, which is turned off in
+  case the suspicious looking function
+  toggle-enable-multibyte-characters is present.  The code that is
+  turned off deals with term markup for proof by pointing, which only
+  affects LEGO at the moment.  This problem could affect forthcoming
+  versions of XEmacs (but hasn't as far as XEmacs 21.1).  Can anybody
+  tell me if it affects Mule versions of Emacs?  Workaround: for LEGO
+  pbp, use FSFmacs 20.2, or XEmacs 20.4/later.
+
+** Using C-g can leave script management in a mess.  
+
+  The code is not fully protected from Emacs interrupts.
+  Workaround: Don't type C-g while script management is processing.  
+  If you do, use proof-restart-scripting.
+
+** Outline-mode does not work in processed proof script files 
+
+ Because of read-only restrictions of the protected region.  
+ This is an inherent problem with outline because it works by 
+ modifying the buffer.
+ Workaround: none, nevermind.  (If it's hugely needed we could support
+ modified outline commands).
+
+** Multiple file handling for Lego and Isabelle is slightly vulnerable.
+
+ Files are not locked when they are being read by the prover, so a long
+ file could be edited and saved as the prover is processing it,
+ resulting in a loss of synchronization between Emacs and the proof
+ assistant.  Files ought to be coloured red while they are being
+ processed, just as single lines are.   Workaround: be careful not
+ to edit a file as it is being read by the proof assistant!
+
+** XEmacs sometimes has strange start-up delays of several seconds.
+
+ Possibly due to face allocation, when running remotely and
+ displaying on an 8-bit display.  One workaround (and in fact the
+ recommended way of working) is to run XEmacs locally and only
+ the proof assistant on your fast compute server, by setting 
+ proof-rsh-command.
+
+** When proof-rsh-command is set to "ssh host", C-c C-c broken
+
+ The whole process may be killed instead of interrupted.  This isn't a
+ bug in Proof General, but the behaviour of ssh.  Try using rsh
+ instead, it is said to forward signals to the remote command.
+
+** In tty mode, the binding C-c C-RET has no effect.  
+
+ Workaround: manually bind C-c RET to 'proof-goto-point instead.
+
+
+
+
+
+