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
|
<!-- FIXME: would be nice to provide links from features
mentioned here to user-manual. -->
<h2>Features of Proof General</h2>
<p>
It doesn't matter if you're an Emacs militant or a pacifist!
</p>
<p> The aim of Proof General is to provide powerful and configurable
interfaces which help user-interaction with proof assistants. Proof
General targets power users rather than novices, but is designed to be
useful to both. Proof General leads to an environment for serious
<i>proof engineering</i> of interactively-constructed proofs.
</p>
<p>Proof General is used by many people for organizing large proof
developments, and also for teaching interactive proof.
They enjoy the following features:</p>
</p>
<dl>
<?php dt("Script management","script") ?>
<dd>
A <em>proof script</em> is a sequence of commands sent to
a proof assistant to construct a proof, usually stored in
a file. <em>Script management</em> connects the editing of a
proof script directly to an interactive proof process,
maintaining consistency between the edit buffer
and the state of the proof assistant.
<p>
Proof General colours a proof script to show the state in the proof
assistant. Parts of a proof script that have been processed are
displayed in blue and are "locked" -- they cannot be edited. Parts
of the script currently being processed by the proof assistant are
shown in red. Bodies of completed proofs in the locked region
can be hidden from view to help browsing.
Proof General has commands for processing new parts
of the buffer, or undoing already processed parts.
</p>
<p>
Take a look at these
<a href="screenshot">screenshots</a>
of Proof General to see script management in action.
</p>
</dd>
</dl><dl>
<?php dt("Simplified interaction model","simple") ?>
<dd>
Proof General is designed for proof assistants which have a
command-line (shell) interpreter. When using Proof General, the proof
assistant's shell is hidden from the user. Communication takes
place via three buffers (Emacs text widgets). The <i>script
buffer</i> holds input, the commands to construct a proof. The
<i>goals buffer</i> displays the current list of subgoals to be
solved. The <i>response buffer</i> displays other output from the
proof assistant. By default, only two of these three buffers are
displayed at once. This means that the user only sees the output
from the most recent interaction, rather than a screen full of
output from the proof assistant.
<p>
Despite this more friendly communication model, Proof General does not
commandeer the proof assistant shell: the user still has complete
access to it if necessary.
</p>
</dd>
</dl><dl>
<?php dt("Multiple files","multiple") ?>
<dd>
Script management in Proof General can work across many script
files, integrating with the file handling of
the proof assistant. When a script is visited in the editor, it
is locked (coloured) to reflect whether the proof assistant has
loaded it in this session. When a file is unlocked, all of the
files which depend on it are automatically unlocked too.
<p>
Dependencies between script files are either communicated from the
proof assistant to Proof General, or maintained automatically by
Proof General (based on the order in which files were processed).
</p>
</dd>
</dl><dl>
<?php dt("Subterm highlighting and proof by pointing","pbp") ?>
<dd>
<p>
Using hidden markup in the concrete syntax, Proof General allows the
user to explore the structure of complex terms output by the prover.
This provides nifty features for cutting-and-pasting subterms,
querying the type of a subterm, looking up the definition of an
identifier, and so on.
</p>
<p>
<em>Proof by pointing</em> uses this markup to allow the prover
to suggest steps in a proof, guided by the user's gestures
in displayed goals. For example, clicking on a hypothesis inserts
a proof step into the script to solve a goal using that hypothesis,
and executes it.
</p>
<?php footnote("Subterm markup is only fully supported by LEGO at the moment, with an experimental implementation of proof by pointing. Isabelle highlights only variables. If you would like to see these features better supported in your favourite proof assistant, please canvas the implementor to add subterm-markup support.") ?>
</dd>
</dl><dl>
<?php dt("Toolbar and menus","toolbar") ?>
<dd>
Proof General has a toolbar with buttons for examining
the proof state, starting a proof, manoeuvring in the proof script,
restarting the prover, saving a proof, searching for a theorem,
issuing a command, interrupting the assistant, and getting help.
<p>
Using the toolbar, you can replay proofs without knowing any
low-level commands of the proof assistant or any Emacs hot-keys!
<p>
Additionally, the toolbar commands and many more besides are
available on menus; you don't need to know magical key presses for
any features.
</p>
</dd>
</dl><dl>
<?php dt("Syntax highlighting","fontlock") ?>
<dd>
Syntax highlighting is an editing feature which decorates a file
with different colours or fonts according to the syntax of some
language (usually a programming language).
<p>
Proof General decorates proof scripts: proof commands are
highlighted and different fonts may be used for definitions and
assumptions, for example.
</p>
</dd>
</dl><dl>
<?php dt("Real symbols","xsymbol") ?>
<dd>
Proof General has a close integration with the
powerful
<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
package, which makes it easy to transparently use real symbols and
Greek letters in your proofs.
<br>
Instead of seeing "not P", you see "¬ P", instead
of "a * b", you see "a × b", etc.
<br>
(Those examples are simple so they will work on most browsers
without needing images, see the
<a href="screenshot">screenshots</a> for more examples.)
<p>
</dd>
</dl><dl>
<?php dt("Proof-script editing facilities","funcmenu") ?>
<dd>
<p>
Many facilities are provided for editing proof scripts.
The <i>completion</i> mechanism of Emacs can be used to
help type keywords and identifier names.
The <i>outline</i> mode of Emacs allows hiding of parts of proof scripts;
a further special <i>proof hiding</i> facility is provided to
hide the body of completed proofs.
<i>Navigation</i> in the script is supported by a pull-down menu
which gives easy access to the theorems, definitions, and declarations
in the current buffer.
</p>
<!-- it is in FSF Emacs if you download func-menu.el from somewhere -->
<!-- <?php footnote("Definitions menu is available in XEmacs only") ?> -->
<p>
</dd>
</dl><dl>
<?php dt("Remote proof assistant.") ?>
<dd>
Sometimes you may want to run a proof assistant on a powerful remote
machine. Proof General can communicate with a proof assistant running
remotely, while your files and editor reside on your local machine.
<p></p>
</dd>
</dl><dl>
<?php dt("Tags","tags") ?>
<dd>
Tags are an editing feature which allow you to quickly locate the
definition or declaration of a particular identifier. Proof General
is supplied with utilities to make tag indexes for Emacs.
This makes it easy to quickly access
definitions from a standard library, for example, and in large proof
developments split across multiple files.
<!-- <?php footnote("Tags programs are provided for LEGO and Coq") ?> -->
<p></p>
</dd>
</dl><dl>
<?php dt("Adaptability","generic") ?>
<dd>
Proof General is designed to be adaptable. Many aspects
of its behaviour can be easily customized (using dialogue boxes and
buttons, no text file editing!).
<p>
Most importantly, Proof General is generic, so you can adapt it to
a new proof assistant with surprisingly little effort.
<p>
Adapting for a new proof assistant is mainly a matter of setting
some variables with regular expressions to help parse output from
the prover, and setting other variables with commands to send to the
prover. See this basic
<?php fileshow("ProofGeneral/demoisa/demoisa-easy.el",
"example instance"); ?>.
To get the most from Proof General (proof by pointing, for
example), it may be necessary to put some hooks in
the output routines of the proof assistant.
</p>
Please feel free to download Proof General to customize it for a new
system, and
<?php hlink("feedback.html","tell us ","Feedback form")?>
how you get on.
</dd>
</dl>
<p>
For (even) more details of Proof General's features, see the manuals and
papers on the <a href="doc">documentation page</a>.
</p>
|
