From 71982ce3a125dcb200e39d3975084aff77fb6ec6 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 31 Jan 2008 23:16:26 +0000 Subject: Updated. --- BUGS | 87 ++++++-------------------------------------------------------------- 1 file changed, 7 insertions(+), 80 deletions(-) (limited to 'BUGS') diff --git a/BUGS b/BUGS index a3bd4083..b9f3c4d6 100644 --- a/BUGS +++ b/BUGS @@ -3,12 +3,10 @@ * Known Bugs and Workarounds for Proof General. For latest, see: http://proofgeneral.inf.ed.ac.uk/trac - See also FAQ: http://proofgeneral.inf.ed.ac.uk/FAQ 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. +provers. See lego/BUGS coq/BUGS, etc, for a few specific bugs. The bugs here are split into problems which apply for all Emacs versions, and those which only apply to particular versions. @@ -18,24 +16,14 @@ PG are mentioned in the FAQ. * Reporting bugs -If you have a problem that is not mentioned here, please contact me at -the address above. Please describe your problem carefully, include a -short demonstration file and tell me the exact version of Emacs and -Proof General that you are using. You can use the menu command - - Proof General -> Help -> Send Bug Report - -to conveniently include the proper version numbers in your message. +If you have a problem that is not mentioned here, please visit the +Trac at the address above to add a ticket. Please describe your +problem carefully, include a short demonstration file and tell us the +exact version of Emacs and Proof General that you are using. * Generic problems, for all Emacs versions -** X-Symbol support removed from "secondary" provers (HOL, ACL2, LEGO, Twelf) - -If anyone was actually using this, please let me know. It should be -very easy to revive by copying coq/x-symbol-coq.el (although a generic -version might be desirable). - ** Visibility control doesn't distinguish theorems with same name. If you have more than one theorem with the same name in a buffer, @@ -101,8 +89,7 @@ If you do, use proof-restart-scripting to be sure of synchronizing. 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). +Workaround: none. ** When proof-rsh-command is set to "ssh host", C-c C-c broken @@ -136,7 +123,7 @@ bug which may be Emacs-related: from now on I will add a note here rather than try to investigate older Emacsen and add more patches to the code. -** XEmacs "nesting too deep for parser" warnings (unresolved in any XEmacs) +** XEmacs "nesting too deep for parser" warnings This is sometimes triggered by very complex output, typically with Isabelle's tracing messages when font-lock is called. @@ -161,30 +148,8 @@ been changed on the file system you see the error: As a result fontification, etc, fails. Workaround: use C-x C-v instead. This problem has gone away since 21.4.12 or so. - Update: this has reappeared in version 21.4.15. - -** GNU 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 on early versions. As -of Emacs 21.3, these glitches have gone. (Although bugs have been -known to return). - -** GNU 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) - -** 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. @@ -192,41 +157,3 @@ 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. -** X-Symbol on GNU Emacs - -X-Symbol 4.X isn't finished yet and will only supported GNU Emacs from -GNU Emacs 21.4 onwards. For the time being there are a few minor -glitches (buffer gets modified during decoding, -subscripts/superscripts don't work, output colouration may spill into -adjacent symbols...), but on the whole it is quite usable (and -rather faster than XEmacs). For more information about X-Symbol, -see http://x-symbol.sourceforge.net. - -** 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. - - -- cgit v1.2.3