-*- outline -*-

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

  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!

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






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

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