Mention critical Emacs bug which destroys characters in certain

compiles of Emacs 23.2.  See Trac#409.

1 files changed, 99 insertions, 83 deletions

diff --git a/FAQ b/FAQ
index 5777c672..734f6c8f 100644
--- a/FAQ
+++ b/FAQ
@@ -8,7 +8,7 @@ Please also check the BUGS file.
 
 -----------------------------------------------------------------
 
-Q1. Proof General fails to load with an error message on start-up,
+Q. Proof General fails to load with an error message on start-up,
     containing text like this: 
   
        Proof General was compiled for GNU Emacs 23.1 but 
@@ -16,7 +16,7 @@ Q1. Proof General fails to load with an error message on start-up,
 
     What's wrong?
 
-A1. We distribute compiled .elcs for one version of Emacs, but other
+A. We distribute compiled .elcs for one version of Emacs, but other
     versions use different bytecode formats.  You will have to delete
     the compiled files and (optionally) recompile for your preferred
     Emacs version.  Using the Makefile:
@@ -31,71 +31,10 @@ A1. We distribute compiled .elcs for one version of Emacs, but other
 
 -----------------------------------------------------------------
 
-Q2. Emacs appears to hang when the prover process is started.
-
-A2. One thing is to check the variable 'comint-process-echoes' which
-    might be non-nil for the *coq* (or other prover) buffer.  It
-    should be nil.
-
-    The default value of comint-process-echoes is nil.  Move any
-    modifications of this variable away from the top level (e.g.,
-    .emacs file, which affects the *coq*-buffer), and down to the
-    mode-hooks which require them (e.g. shell-mode-hook).  The
-    variable might also have been set by Customize, it can be reset
-    with M-x customize-variable RET comint-process-echoes RET.
-
-    A reason with older versions of Isabelle and Coq (before 2007) was
-    the emergence of UTF-8 support in linuxes with Glibc 2.2 and
-    later, enabled with UTF8 encoded output in your default locale.
-    Proof General used on 8-bit characters which are UTF8 prefixes in
-    the output of proof assistants.  These prefix characters were not
-    flushed to stdout individually.  
-
-     As a workaround we can disable interpretation of UTF8 in the C
-    libraries.  Doing this inside Proof General is unreliable; locale
-    settings are set/inherited in strange ways.  One solution is to
-    run the Emacs process itself with an altered locale setting, e.g.,
-
-    $  LC_CTYPE=en_GB xemacs &
-
-    (where $ is the shell prompt; this example is for my locale which
-     by default is "en_GB.UTF-8": I see this by typing "locale" at
-     the prompt).
-
-    (This fix is attempted in the supplied "proofgeneral" script, as
-    well as making an adjustment in Proof General when the string UTF
-    appears in the current value of LC_CTYPE.  Alternatively you can
-    set LC_CTYPE inside a file ~/.i18n, which will be read the shell.
-    Put a line such as "LC_CTYPE=en_GB" into this file.  However, this
-    action will affect all applications.
-
-    NB: a related issue is warnings from X-Symbol: "Emacs language 
-    environment and system locale specify different encoding, I'll 
-    assume `iso-8859-1'".  This warning appears to be mostly harmless.
-    Notice that the variable `buffer-file-coding-system' may determine
-    the format that files are saved in.  
-
-    Another way to affect this which has been suggested is to add a line
-    like this to the init.el file on XEmacs:
-  
-      (prefer-coding-system 'ctext)
-
-    but I haven't tried this.
-
-    The above fixes should not be necessary with most recent prover
-    versions.  Isabelle 2007 has a "Unicode-safe" interaction mode,
-    enabled by default (to disable, customise `proof-shell-unicode').
-    This is also used by the Isabelle startup scripts.  Coq 8.1 and
-    later do not use non-ASCII characters in output.
-
-  
-
------------------------------------------------------------------
-
-Q4. Help, I'm stuck!! Emacs keeps telling me "Cannot switch buffers in a
+Q. Help, I'm stuck!! Emacs keeps telling me "Cannot switch buffers in a
     dedicated window"  
 
-A4. This can happen if you enabled "Use Three Panes" and then change
+A. This can happen if you enabled "Use Three Panes" and then change
     the panes (window) layout manually, typically by deleting another 
     window or frame so you only have a "dedicated" window on the 
     display.  Don't kill Emacs!  There are many ways of getting out,
@@ -110,9 +49,9 @@ A4. This can happen if you enabled "Use Three Panes" and then change
 
 -----------------------------------------------------------------
 
-Q5. I have a problem installing/using Proof General, what can I do?
+Q. I have a problem installing/using Proof General, what can I do?
 
-A5. Please check the documentation carefully, particularly the
+A. Please check the documentation carefully, particularly the
     requirements for a full-featured and recent Emacs version, as
     mentioned in INSTALL (see "Dependency on Other Emacs Packages").  
     If you still cannot solve your problem, try to contact someone
@@ -125,10 +64,10 @@ A5. Please check the documentation carefully, particularly the
 
 -----------------------------------------------------------------
 
-Q6. I'm using Proof General for prover X, then I load a file for
+Q. I'm using Proof General for prover X, then I load a file for
     prover Y.  I get an error.  Why?
 
-A6. Unfortunately the architecture of Proof General is designed so
+A. Unfortunately the architecture of Proof General is designed so
     that you can only use one prover at a time in the same Emacs
     session.   If you want to run more than one prover at a time,
     you have to run more than one Emacs.
@@ -137,11 +76,11 @@ A6. Unfortunately the architecture of Proof General is designed so
 
 -----------------------------------------------------------------
 
-Q7. I have just installed Emacs, ProofGeneral and a proof assistant.
+Q. I have just installed Emacs, ProofGeneral and a proof assistant.
     It works but Tokens (e.g. \<Longrightarrow>) are not being displayed 
     as symbols.
 
-A7. You need to enable Unicode Tokens by the menu item:
+A. You need to enable Unicode Tokens by the menu item:
 
       Proof-General -> Options -> Unicode Tokens
   
@@ -160,10 +99,24 @@ A7. You need to enable Unicode Tokens by the menu item:
     from any location, and you can enable it by passing the option 
     "-x true".
 
+
 -----------------------------------------------------------------
 
 
-Q8. I'm afraid I got stuck very early on.  I sent the following line:
+Q.  With Unicode symbols enabled, arrows and other symbols appear
+    compressed and overlap one another.
+
+A.  Unfortunately this is a bug in the display engine inside
+    certain versions of Emacs, for example the default version
+    of emacs, Emacs 23.3.1 on Ubuntu 11.10, suffers.
+
+    The solution is to switch to another version (e.g. Emacs 23.2).
+    (See Trac#409).
+
+-----------------------------------------------------------------
+
+
+Q. I'm afraid I got stuck very early on.  I sent the following line:
 
       by (swap_res_tac [psubsetI] 1;
 
@@ -171,7 +124,7 @@ Q8. I'm afraid I got stuck very early on.  I sent the following line:
     buffer went read-only and nothing I tried would let me fix the
     error.  
 
-A8. The proof process is waiting for more input because of the missing
+A. The proof process is waiting for more input because of the missing
     parenthesis, but Proof General doesn't realise this and waits for a
     response.  You should type something in the proof shell buffer
     (*isabelle*), or interrupt the process with C-c C-c or the Stop button.
@@ -179,9 +132,9 @@ A8. The proof process is waiting for more input because of the missing
 
 -----------------------------------------------------------------
 
-Q9. How can I keep the Proof General option settings across sessions?
+Q. How can I keep the Proof General option settings across sessions?
 
-A9. For options set in the Proof General -> Options menu use the 
+A. For options set in the Proof General -> Options menu use the 
     "Save Options" menu item (Proof General -> Options -> Save Options).
 
     For other options set via customize (Proof General -> Advanced -> 
@@ -190,10 +143,10 @@ A9. For options set in the Proof General -> Options menu use the
 
 -----------------------------------------------------------------
 
-Q10. The "Favourites" feature to insert/send fixed strings is great, 
+Q. The "Favourites" feature to insert/send fixed strings is great, 
      but I'd like to define a command which takes arguments.
 
-A10. You can do that in Elisp with a command like this: 
+A. You can do that in Elisp with a command like this: 
 
       (proof-definvisible isar-theorem
         '(format "thm %s" (read-string "theorem: "))
@@ -205,9 +158,9 @@ A10. You can do that in Elisp with a command like this:
 
 -----------------------------------------------------------------
 
-Q11. Why do I get a warning "Bad version of xml.el found, ..."?
+Q. Why do I get a warning "Bad version of xml.el found, ..."?
 
-A11. Your Emacs distribution includes a version of xml.el which has 
+A. Your Emacs distribution includes a version of xml.el which has 
      fundamental bugs.   The patched version of xml.el, in lib/xml-fixed.el
      has been loaded instead.  This works for Proof General because it fixes
      the basic bugs, but it may cause compatibility issues in other packages
@@ -221,10 +174,10 @@ A11. Your Emacs distribution includes a version of xml.el which has
 
 -----------------------------------------------------------------
 
-Q12. Undo behaviour in Coq seems to stop working with very long
+Q. Undo behaviour in Coq seems to stop working with very long
      sequences of commands.
 
-A12. Coq has a limited history for Undo.  Change 
+A. Coq has a limited history for Undo.  Change 
 
 	Coq -> Settings -> Undo Depth
 
@@ -234,9 +187,9 @@ A12. Coq has a limited history for Undo.  Change
 -----------------------------------------------------------------
 
 
-Q13. Can I join any mailing lists for Proof General?
+Q. Can I join any mailing lists for Proof General?
 
-A13. Of course, email "proofgeneral-request@informatics.ed.ac.uk" 
+A. Of course, email "proofgeneral-request@informatics.ed.ac.uk" 
      with the line "subscribe" in the message body, to join the
      users' and announcements list.
 
@@ -247,6 +200,69 @@ A13. Of course, email "proofgeneral-request@informatics.ed.ac.uk"
      for more details.
 
 
+-----------------------------------------------------------------
+
+Q. Emacs appears to hang when the prover process is started.
+
+A. One thing is to check the variable 'comint-process-echoes' which
+    might be non-nil for the *coq* (or other prover) buffer.  It
+    should be nil.
+
+    The default value of comint-process-echoes is nil.  Move any
+    modifications of this variable away from the top level (e.g.,
+    .emacs file, which affects the *coq*-buffer), and down to the
+    mode-hooks which require them (e.g. shell-mode-hook).  The
+    variable might also have been set by Customize, it can be reset
+    with M-x customize-variable RET comint-process-echoes RET.
+
+    A reason with older versions of Isabelle and Coq (before 2007) was
+    the emergence of UTF-8 support in linuxes with Glibc 2.2 and
+    later, enabled with UTF8 encoded output in your default locale.
+    Proof General used on 8-bit characters which are UTF8 prefixes in
+    the output of proof assistants.  These prefix characters were not
+    flushed to stdout individually.  
+
+     As a workaround we can disable interpretation of UTF8 in the C
+    libraries.  Doing this inside Proof General is unreliable; locale
+    settings are set/inherited in strange ways.  One solution is to
+    run the Emacs process itself with an altered locale setting, e.g.,
+
+    $  LC_CTYPE=en_GB xemacs &
+
+    (where $ is the shell prompt; this example is for my locale which
+     by default is "en_GB.UTF-8": I see this by typing "locale" at
+     the prompt).
+
+    (This fix is attempted in the supplied "proofgeneral" script, as
+    well as making an adjustment in Proof General when the string UTF
+    appears in the current value of LC_CTYPE.  Alternatively you can
+    set LC_CTYPE inside a file ~/.i18n, which will be read the shell.
+    Put a line such as "LC_CTYPE=en_GB" into this file.  However, this
+    action will affect all applications.
+
+    NB: a related issue is warnings from X-Symbol: "Emacs language 
+    environment and system locale specify different encoding, I'll 
+    assume `iso-8859-1'".  This warning appears to be mostly harmless.
+    Notice that the variable `buffer-file-coding-system' may determine
+    the format that files are saved in.  
+
+    Another way to affect this which has been suggested is to add a line
+    like this to the init.el file on XEmacs:
+  
+      (prefer-coding-system 'ctext)
+
+    but I haven't tried this.
+
+    The above fixes should not be necessary with most recent prover
+    versions.  Isabelle 2007 has a "Unicode-safe" interaction mode,
+    enabled by default (to disable, customise `proof-shell-unicode').
+    This is also used by the Isabelle startup scripts.  Coq 8.1 and
+    later do not use non-ASCII characters in output.
+
+  
+
+
+
 
 $Id$