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
|
FAQs for using Proof General
============================
For latest version, see http://www.proofgeneral.org/FAQ
Credits to the anonymous authors of questions/answers below.
-----------------------------------------------------------------
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'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. Simply use the ordinary XEmacs menu: Options -> Save Options
In GNU Emacs, you can do M-x customize-save-customized
or use the Custom->Save menu in a customize buffer.
-----------------------------------------------------------------
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 font-lock-fontify-buffer or M-x x-symbol-fontify.
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$
|
