From f800a01bf3aa57e5f1252cd996b93f315a344251 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 10 Jan 2012 12:59:54 +0000 Subject: Mention critical Emacs bug which destroys characters in certain compiles of Emacs 23.2. See Trac#409. --- FAQ | 182 +++++++++++++++++++++++++++++++++++++------------------------------- 1 file changed, 99 insertions(+), 83 deletions(-) (limited to 'FAQ') 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. \) 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$ -- cgit v1.2.3