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
|
<!-- <h2><a name="why">Why should I use Proof General?</a></h2> -->
<p>
It doesn't matter if you're an Emacs militant or a pacifist!
</p>
<p>
Proof General will be useful to you if you use a proof
assistant, and you'd like some of the following features:
</p>
<dl>
<?php dt("Script management.") ?>
<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. Commands are provided to process new parts of the
buffer, or undo already processed parts.
</p>
<p>
Take a look at this
<a href="screenshot.phtml">screenshot</a>
of Proof General to see script managament in action.
</p>
</dd>
<?php dt("Multiple files.") ?>
<dd>
Script management in Proof General can work across many script
files. When a script is visited in the editor, it is
coloured to reflect whether the proof assistant has loaded it in
this session.
<p>
Dependencies between script files is
communicated from the proof assistant to Proof General.
If you want to edit a file which has been loaded into the
proof assistant already, Proof General will unlock the file
and all the files which depend on it. This connects the
editor with the theory dependency or make system of the
proof assistant.
</p>
<?php footnote("Multiple files currently supported in LEGO and Isabelle only")?>
</dd>
<?php dt("Proof by Pointing.") ?>
<dd>
<em>Proof by pointing</em> allows you to click on a subterm of
a goal to be proved, and apply an appropriate rule or
tactic automatically.
<p>
Proof by pointing uses the
interface to highlight subterms under the mouse, and Proof General
uses the subterm structure to make it easy
to cut and paste complicated subterms.
</p>
<?php footnote("No assistant fully supports proof-by-pointing in Proof General
yet. LEGO provides subterm markup for exploring term
structure.") ?>
</dd>
<?php dt("Toolbar.") ?>
<dd>
Proof General has a toolbar with buttons for starting a proof,
manoeuvring in the proof script, restarting the prover
and saving a proof.
<p>
Using the toolbar, you can replay proofs without knowing any
low-level commands of the proof assistant or any Emacs hot-keys!
</p>
<?php footnote("Toolbar is available in XEmacs only") ?>
</dd>
<?php dt("Syntax highlighting.") ?>
<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>
<?php dt("Tags.") ?>
<dd>
Tags are an editing feature which allow you to quickly locate
the definition or declaration of a particular identifier.
<p>
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>
<?php dt("Definitions Menu.") ?>
<dd>
A pull-down menu gives easy
access to definitions, declarations and proofs in the current
buffer.
<?php footnote("Definitions menu is available in XEmacs only") ?>
</dd>
<?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>
<?php dt("Adaptability.") ?>
<dd>
Proof General is designed to be generic, so you can adapt it
to a new proof assistant if you know a little bit of Emacs
Lisp.
<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.
To get the most from Proof General (proof-by-pointing, for example),
it may be necessary to augment 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.phtml","tell us ","Feedback form")?>
how you get on.
</dd>
</dl>
<p>
For more details of the above features, see the
<?php link_root("doc","documentation page.") ?>
</p>
|
