Known Bugs and Workarounds.
===========================

$Id$

* Toolbar: retract button can give "BUG" error message "called from
wrong buffer" when the process is inactive.

* Ordinary undo in 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.

* 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.

* You can't use more than one proof assistant at a time in the same
Emacs session.  Attempting to load Proof General for a second prover
will fail.  Workaround: stick to one prover per Emacs session, 
make sure that the proof-assistants variables only enables 
Proof General for the provers you need.

* Outline-mode does not work in proof script files due to read-only
restrictions of protected region.  Workaround: none, nevermind.
(If it's hugely needed we could support modified outline commands).

* There is an obscure bug with processes on Solaris which results in
buffers full of ^G after certain combinations of input.  Workaround:
get a patch from Sun, or use Linux.

* XEmacs sessions perhaps grow excessively in terms of memory
allocation. Maybe some of the spans aren't removed properly.
Setting a limit on the size of the process buffer doesn't seem to
help.  (1998/10/06: Is this bug still present?  Test examples?)

*`proof-find-next-terminator' (bound to C-c C-e) doesn't work
properly. Workaround: use other means to navigate in a proof scipt
buffer. 


FSF Emacs specific bugs
=======================

*`proof-zap-commas-region' does not work for Emacs 20.2 on
  lego/example.l . On *initially* fontifying the buffer,
  commas are not zapped. However, when entering text, commata are
  zapped correctly. Workaround: don't stare too much at commata

LEGO Proof General Bugs
=======================

* 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 issues are 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.

Isabelle Proof General Bugs
===========================

* General difficulty with complex proof scripts.  Since Isabelle uses
ML as a top-level language for writing proof-scripts, Proof General
may have difficulty understanding scripts which stray too far away
from the standard functions, tactics, and tacticals.  You will
usually notice when a function, or whatever, doesn't get highlighted
as you might expect.  This probably has no detrimental impact on the
interface unless you use your own "goal" or "qed" forms.