1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
|
FAQs for using Proof General
============================
With thanks to the anonymous authors of questions/answers below.
For latest version, see http://proofgeneral.inf.ed.ac.uk/FAQ
Please also check the BUGS file.
-----------------------------------------------------------------
Q. Emacs appears to hang when the prover process is started.
A. This may be because of UTF-8 issues e.g in Red Hat 8.0/9/glibc 2.2
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.
Doing this inside PG/Emacs seems tricky; locale settings are
set/inherited in strange ways. One solution is to run the Emacs
process itself in a different locale, for example, starting XEmacs
by typing:
$ LANG=en_GB xemacs &
Another solution is to set LANG inside a file ~/.i18n, which will
be read the shell. This will affect all applications, though.
[ suggestions for a better workaround inside Emacs would be welcome ]
-----------------------------------------------------------------
Q. XEmacs appears to hang on certain malformed inputs to the prover.
A. This symptom may be caused by using non-Mule versions of XEmacs.
Please make sure you use a Mule-enabled version.
-----------------------------------------------------------------
Q. XEmacs 21.4 displays a progress bar during fontification which
sometimes gets stuck or messes up the display.
Is this a Proof General bug? What can I do?
A. This is an XEmacs bug. What you can do is prevent the use
of the ugly widget, for example by adding
(setq progress-feedback-use-echo-area t)
inside your configuration file `.xemacs/init.el'.
-----------------------------------------------------------------
Q. I have a problem installing/using Proof General, what can I do?
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, send a message to
da+pg-support@inf.ed.ac.uk in the first instance.
-----------------------------------------------------------------
Q. I'm using Proof General for prover X, then I load a file for prover Y.
The buffer doesn't enter the mode for prover Y. Why not?
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.
-----------------------------------------------------------------
Q. I have just installed Emacs, ProofGeneral and a proof assistant.
It works but X-Symbol is not being activated.
A. Once X-Symbol is picked up by Emacs (e.g. is working for TeX),
you should enable it inside Proof General by the menu item:
Proof-General -> Options -> X-Symbol
To enable it automatically every time you use Proof General,
type
M-x customize-variable RET isar-x-symbol-enable RET
and change/set/save the setting to `on'.
Note that we don't do this by default, because from the system's
perspective it is difficult to determine if this will succeed ---
or just produce funny characters that confuse new users even more.
If you are using Isabelle, the wrapper script will load X-Symbol
from any location, and you can enable it by passing the option
"-x true".
-----------------------------------------------------------------
Q. I notice that editing Isabelle files in Proof General with XEmacs
21.4 is very slow. Can this be fixed?
A. You could consider adding the following line to your init file:
(setq lookup-syntax-properties nil)
This hack bypasses some very slow code in the font-lock system, but
it also disables some syntax-related features, so use with care.
-----------------------------------------------------------------
Q. I'm afraid I got stuck very early on. I sent the following line:
by (swap_res_tac [psubsetI] 1;
Notice that I forgot the right bracket. The line went pink, the
buffer went read-only and nothing I tried would let me fix the
error.
A. The proof process is waiting for more input, but Proof General
doesn't realise this and waits for a response. You
should type something in the proof shell, or interrupt the process
with C-c C-c or the Stop button.
-----------------------------------------------------------------
Q. How can I keep the Proof General option settings across sessions?
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 ->
Customize), use the customize buttons, or M-x customize-save-customized.
-----------------------------------------------------------------
Q. How do I use Proof General for Isabelle classic instead of Isabelle/Isar?
A. There are several ways:
1. Use the Isabelle settings mechanism, invoke with "Isabelle"
2. Set the environment variable PROOFGENERAL_ASSISTANTS=isa
before starting Emacs.
3. Put the line (* -*- isa -*- *) at the top of your files.
Unfortunately Isabelle/Isar and Isabelle classic are two quite
separate Proof General instances. Ideally they should be
combined into one, if anyone fancies some elisp hacking...
-----------------------------------------------------------------
Q. When using X-Symbol, why do I sometimes see funny characters like
\233 in the buffer?
A. These are part of the 8 bit character codes used by X Symbol to
get symbols from particular fonts. Sometimes X-Symbol forgets to
fontify the buffer properly to make it use the right fonts.
(That's being rather unkind to X-Symbol: several things can
go wrong one way or another).
To fix, type
M-x x-symbol-decode-recorde
If that doesn't work, type M-x font-lock-mode twice to turn font-lock
off then on. Or reload the file.
Note that X-Symbol is more robust when used with XEmacs/Mule.
Read the X-Symbol documentation for (much) more information.
http://x-symbol.sourceforge.net/man/
-----------------------------------------------------------------
Q. I would like to use the X-Symbol fonts in PG not just at the
standard size but also for larger sizes since I use PG during
talks, where I set the font size to 24.
A. Nobody has designed large versions of the X-Symbol fonts but it is
possible to scale-up the existing ones, by adding
(setq x-symbol-xsymb1-fonts
'(("-xsymb-xsymb1-medium-r-normal-*-*-240-*-*-*-*-xsymb-xsymb1")
("-xsymb-xsymb1_sub-medium-r-normal-*-*-180-*-*-*-*-xsymb-xsymb1")
("-xsymb-xsymb1_sup-medium-r-normal-*-*-180-*-*-*-*-xsymb-xsymb1")))
(setq x-symbol-xsymb0-fonts
'(("-adobe-symbol-medium-r-normal-*-*-240-*-*-*-*-adobe-fontspecific"
"-xsymb-xsymb0-medium-r-normal--*-240-75-75-p-85-adobe-fontspecific")
("-xsymb-xsymb0_sub-medium-r-normal--18-180-75-75-p-74-adobe-fontspecific"
"-adobe-symbol_sub-medium-r-normal-*-*-180-*-*-*-*-adobe-fontspecific")
("-xsymb-xsymb0_sup-medium-r-normal--18-180-75-75-p-74-adobe-fontspecific"
"-adobe-symbol_sup-medium-r-normal-*-*-180-*-*-*-*-adobe-fontspecific")))
to your .emacs, which causes the special fonts to come up in size
24; the normal font you can change manually. Of course you can also
select smaller sizes. Most of the symbols look reasonable, except
that they appear almost bold.
For more information about this, see the X-Symbol FAQ, at
http://x-symbol.sourceforge.net/man/x-symbol_8.html#SEC100
-----------------------------------------------------------------
Q. Can I join any mailing lists for Proof General?
A. Of course, email "proofgeneral-request@informatics.ed.ac.uk"
with the line "subscribe" in the message body, to join the
user's and announcements list.
There is also a list for developers, proofgeneral-devel
Visit http://www.proofgeneral.org/mailinglist for more details.
-----------------------------------------------------------------
Q. I see spurious ^M characters at the end of lines in the
windows showing output from the prover. How can I remove
them?
A. Customize the value of `proof-shell-strip-crs-from-output'.
-----------------------------------------------------------------
$Id$
|
