diff options
Diffstat (limited to 'BUGS')
| -rw-r--r-- | BUGS | 179 |
1 files changed, 179 insertions, 0 deletions
@@ -0,0 +1,179 @@ +-*- 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 / glibc 2.2 and (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 & + +Another solution is to set LANG inside a file ~/.i18n, which will +be read the shell. This will affect all applications, though. +[ 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. + + + |