added PG hang to FAQ
Fri, 22 Apr 2005 04:12:24 +0200
changeset 15812 c1d36b9c7c3b
parent 15811 ef719c524227
child 15813 741978011e12
added PG hang to FAQ
--- a/Admin/page/main-content/faq.content	Fri Apr 22 02:09:10 2005 +0200
+++ b/Admin/page/main-content/faq.content	Fri Apr 22 04:12:24 2005 +0200
@@ -209,6 +209,39 @@
+    <table class="question" width="100%"><tr><td>ProofGeneral appears to hang when Isabelle is started.</td></tr></table>
+    <table class="answer" width="100%"><tr>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse 9.0/9.1
+    <p>
+   RedHat 8 and later 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.
+   <p>
+   Doing this inside PG/Emacs seems tricky; locale settings are
+   set/inherited in strange ways.  One solution is to run the Emacs
+   process itself with an altered locale setting, for example,
+   starting XEmacs by typing:
+   <p>
+   <tt>$  LC_CTYPE=en_GB Isabelle &</tt>
+   <p>
+   The supplied proofgeneral script makes this setting if it sees
+   the string UTF in the current value of LC_CTYPE. Depending on your 
+   distribution, this variable might also be called <tt>LANG</tt>.
+   <p>
+   Alternatively you can set LC_CTYPE or LANG inside a file ~/.i18n, which will
+   be read by the shell.  This will affect all applications, though.
+   [ suggestions for a better workaround inside Emacs would be welcome ]
+   <p>
+   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 mainly harmless.
+   Notice that the variable `buffer-file-coding-system' may determine
+   the format that files are saved in.<td></td></tr></table>
     <table class="question" width="100%"><tr><td>X-Symbol doesn't seem to work. What can I