path: root/BUGS

-*- outline -*-

* Bugs to be fixed before PG 3.5 is released.

The items below are known and will be fixed before 3.5 is released.
Please don't send email about them (unless you can fix them).


** UTF-8 problems with Red Hat 8.0  &  (at least) Coq.  

RedHat 8 has Glibc 2.2 and UTF8 encoded output may be turned on in
default locale.  Unfortunately Proof General relies on 8-bit
characters which are UTF8 prefixes in the output of proof assistants
(inc Coq, Isabelle).  These prefix characters are not flushed to
stdout individually.  As a workaround we must find a way to disable
interpretation of UTF8 in the C libraries that Coq and friends use.

Doing this inside PG/Emacs seems tricky; locale settings are
set/inherited in strange ways.  One solution is to run the Emacs
process itself in a different locale, for example, starting XEmacs by
typing:

  $  LANG=en_GB xemacs &

[ suggestions for a better workaround inside Emacs would be welcome ]



=================================================================

* Known Bugs and Workarounds for Proof General.

Contact:  mailto:bugs@proofgeneral.org
See also: http://www.proofgeneral.org/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.  

The bugs here are split into problems which apply for all Emacs
versions, and those which only apply to particular versions.


* Generic problems, for all Emacs versions

** Visibility control doesn't distinguish theorems with same name.

If you have more than one theorem with the same name in a buffer,
their proof visibilities are controlled together.

** 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.  If that 
doesn't stop things, you can try 'kill -FPE <emacs-pid>'.  
This problem can happen with looping rewrite rules in the Isabelle
simplifier, when tracing rewriting.  It seems to be worse on 
certain architectures, and slower machines.  Behaviour seems
better on Emacs than XEmacs.

** Toolbar enablers unreliable on some platforms.

Occasionally the buttons are disabled/enabled when they shouldn't be.
An extra click on the toolbar may solve this.  If you have problems,
please customize `proof-toolbar-use-button-enablers' to nil to
disable the enablers. 

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

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

** Multiple file scripting 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!



* Problems with particular Emacs versions

** Buggy output fontification with Emacs 21.2 / X-Symbol 4.X

Output colouration may spill into adjacent symbols when X-Symbol
support is switched on.  X-Symbol 4.X isn't yet finished, and will
only officially support Emacs from 21.4 onwards.  It may work with
Isabelle for Emacs 21.X but please don't try it with other provers.

** Emacs menus: options not updated dynamically, positions erratic, etc.

Also, proof assistant specific menus only appear in scripting buffer.
These are drawbacks with GNU Emacs menu support.

** Emacs faces sometimes faulty, esp in console mode

Emacs support is let down in console mode, because faces are not
implemented there.  (XEmacs can use colours and underline in console
mode)

** XEmacs 21.1.9 on Win32

Some strange problems reading files with this version of Emacs. Gives
spurious "end of internal input stream", or silently ignores parts of
files.  Example is coq/coq.el which reads in fine on Linux.
Solution: use a more recent version of XEmacs.  


** If you have problems using Mule versions of GNU Emacs 

Beware setting standard-display-european: Pascal Brisset suggests
adding this line to .emacs should help:

   (setq process-coding-system-alist '(("" . no-conversion))) 



** XEmacs undo in the script buffer can edit the "uneditable region"

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.

** As of GNU Emacs 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.4).  [Can anybody
tell us if it affects Mule versions of Emacs?]  

Workaround: for LEGO pbp, use GNU Emacs 20.2, or XEmacs 20.4/later.

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

** Looping in Emacs 21.2

Several (odd) circumstances cause this version of Emacs to loop,
in particular, when moving the cursor into multi-byte characters.
Workarounds have been added to avoid this: you may see junk
characters in the shell buffer as a side effect.