From f4b7486b35567382de0814582d74e79e51a22e89 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 31 Aug 2011 19:53:14 +0000 Subject: Add suggestion for Q2 from Esben Andreasen to check comint-process-echoes. --- FAQ | 48 ++++++++++++++++++++++++++++-------------------- 1 file changed, 28 insertions(+), 20 deletions(-) (limited to 'FAQ') diff --git a/FAQ b/FAQ index 6b9bbb90..5777c672 100644 --- a/FAQ +++ b/FAQ @@ -33,17 +33,28 @@ A1. We distribute compiled .elcs for one version of Emacs, but other Q2. Emacs appears to hang when the prover process is started. -A2. This is usually caused by UTF-8 support in recent linuxes with - Glibc 2.2 or later, probably enabled with UTF8 encoded output in - your default locale. Unfortunately Proof General traditionally - relied 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 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., +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 & @@ -52,14 +63,13 @@ A2. This is usually caused by UTF-8 support in recent linuxes with 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). + 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. - 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 + 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 @@ -72,8 +82,6 @@ A2. This is usually caused by UTF-8 support in recent linuxes with but I haven't tried this. - ** Update for PG 3.7 ** - 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'). -- cgit v1.2.3