path: root/BUGS

Known Bugs and Workarounds for Proof General.
=============================================

$Id$

Contact:  proofgen@dcs.ed.ac.uk
See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS

-----------------

Generic problems
================

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

* Synchronization during start-up: if you press C-c C-n quickly
in succession whilst the prover is cranked up, synchronization
may be spoilt, and you see the message "script management confused"
later on.  This is a minor bug, most likely to be noticed when it
takes a while to start the proof assistant (e.g. Isabelle!).
Workarounds: many!  Type slowly.  Use C-c C-RET.  Start the prover
first via the menu, or C-c C-s.

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



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
===========================

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

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