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
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
|
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.
-----------------------------------------------------------------
Q1. Proof General fails to load with an error message on start-up,
containing text like this:
Proof General was compiled for GNU Emacs 22.2 but
running on XEmacs 23.0: please run "make clean; make"
What's wrong?
A1. We distribute compiled .elcs for GNU Emacs 22.2, so you will have to
delete them and (optionally) recompile for your preferred
Emacs version. Using the Makefile:
make clean # removes all .elc files.
and then a command like this:
make EMACS=emacs-23.0
-----------------------------------------------------------------
Q2. Proof General fails to load with an error message like this:
file mode specification error:
(file-error "cannot open load file" "executable")
What's wrong?
A2. You're missing some Emacs (probably XEmacs) packages. See
the section "Dependency on Other Emacs Packages" in INSTALL.
Quicker answer: install the "XEmacs Sumo" package collection.
-----------------------------------------------------------------
Q3. Emacs appears to hang when the prover process is started.
A3. 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 PG/Emacs 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.
** 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').
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
dedicated window"
A4. 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,
e.g.
-- In single window mode, C-c C-l (proof-layout-windows) refreshes
the display
-- In multiple window mode, if you have accidently deleted the main
window, get a new one with M-x new-frame RET
-----------------------------------------------------------------
Q5. I have a problem installing/using Proof General, what can I do?
A5. 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
else who is using Proof General with a similar setup. The
best way to do this may be through the user mailing list for your
proof assistant. If you think the problem is Proof General related,
consult the PG Wiki and Trac pages.
-----------------------------------------------------------------
Q6. 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
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.
-----------------------------------------------------------------
Q7. 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:
Proof-General -> Options -> Unicode Tokens
To enable it automatically every time you use Proof General,
use
Proof-General -> Options -> Save Options
after doing this.
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 Tokens
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:
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.
A8. 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.
-----------------------------------------------------------------
Q9. How can I keep the Proof General option settings across sessions?
A9. 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.
-----------------------------------------------------------------
Q10. 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:
(proof-definvisible isar-theorem
'(format "thm %s" (read-string "theorem: "))
[(control t)])
(NB: it binds the key C-c C-a C-t). See the documentation for
`proof-definvisible' and `proof-defshortcut`.
-----------------------------------------------------------------
Q11. Why do I get a warning "Bad version of xml.el found, ..."?
A11. 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
(e.g. it is quite different from the latest xml.el with GNU Emacs
development versions).
This message is probably nothing to worry about unless you are using
the same Emacs session for other packages that heavily use xml.el
(e.g. GNUS).
-----------------------------------------------------------------
Q12. Undo behaviour in Coq seems to stop working with very long
sequences of commands.
A12. Coq has a limited history for Undo. Change
Coq -> Settings -> Undo Depth
to something higher. Default is 200 (100 outside PG).
-----------------------------------------------------------------
Q13. Can I join any mailing lists for Proof General?
A13. Of course, email "proofgeneral-request@informatics.ed.ac.uk"
with the line "subscribe" in the message body, to join the
users' and announcements list.
There is also a list for developers, proofgeneral-devel:
http://proofgeneral.inf.ed.ac.uk/mailinglist
for more details.
$Id$
|
