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
|
FAQs for Proof General
======================
$Id$
For latest version, see http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/FAQ
-----------------------------------------------------------------
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.
[ In case of Isabelle under Poly/ML, you should start PG 3.1
using the Isabelle script because it adds a hack to send "f"
after an interrupt is sent. With PG 3.2, the hack is added for
Poly/ML even if you start Emacs first. ]
-----------------------------------------------------------------
Q. How can I keep the Proof General option settings across sessions?
A. Simply use the ordinary XEmacs menu: Options -> Save Options
In FSF Emacs, you can do M-x customize-save-customized
or use the Custom->Save menu in a customize buffer.
-----------------------------------------------------------------
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. How do I use Proof General for Isabelle/Isar instead of Isabelle classic?
A. There are several ways:
1. Use the Isabelle settings mechanism, invoke with "Isabelle"
2. Set the environment variable PROOFGENERAL_ASSISTANTS=isar
before starting Emacs.
3. Put the line (* -*- isar -*- *) at the top of your Isar 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.
To fix, type M-x 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.
-----------------------------------------------------------------
Q. Can I join any mailing lists for Proof General?
A. Of course, email "majordomo@dcs.ed.ac.uk" with the
lines "subscribe proofgeneral" or "subscribe proofgeneral-devel"
in the message body.
|
