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
|
<h2>Please register</h2>
<p>
Before downloading Proof General, please
<a href="register.phtml">register</a>.
<br>
The information collected will be used only to help a case for
support for Proof General in the future.
<br>
If you have already registered you do not need to do so again.
</p>
<p>
You may like to consider joining the
Proof General
<a href="mailinglist.phtml">mailing list</a>.
</p>
<p>
You can download the latest
stable release,
<a href="#stable">ProofGeneral-2.1</a>, or the latest pre-release,
<!-- Warning, next line edited by make file -->
<a href="#prerel">ProofGeneral-2.2pre990921</a>.
There is also a complete archive
of the current pre-release
<a href="#devel">for developers</a>.
</p>
<p>
If you are using an older version of one of the proof assistants,
you may wish to check the
<a href="#previous">previous releases</a> of Proof General.
</p>
<hr>
<h2><a name="stable">
Proof General Version 2.1, released 24th August 1999
</a>
</h2>
<p>
This version of Proof General has been tested
with XEmacs 20.4, XEmacs 21 and FSF Emacs 20.3.<br>
It supports Coq version 6.3, LEGO version 1.3.1 and
Isabelle version 99.
<p>
Check the <?php fileshow("ProofGeneral-2.1/CHANGES","CHANGES"); ?> file
for a summary of changes since version 2.0.
<br>
Proof General is available in two formats:
</p>
<ul>
<li> gzip'ed tar file:
<?php download_link("ProofGeneral-2.1.tar.gz") ?>
</li>
<li> Linux RPM package:
<?php download_link("ProofGeneral-2.1-1.noarch.rpm") ?>
<br>
The source RPM is
<?php download_link("ProofGeneral-2.1-1.noarch.rpm","here") ?>.
</li>
</ul>
<p>
Both the tarball and the RPM package include the generic elisp
code, <br>
code for LEGO, Coq, and Isabelle, installation instructions
and documentation.
</p>
<h3> Easy installation! </h3>
<p>
To use Proof General, simply unpack the sources with
</p>
<blockquote>
<tt>tar -xpzf ProofGeneral-2.1.tar.gz</tt>
</blockquote>
<p>
(use <tt>gunzip</tt> in place of -z if you don't have GNU tar),<br>
and then add this one line to your .emacs file:
</p>
<blockquote>
<tt> (load-file "<var>directory</var>/generic/proof-site.el")</tt>
</blockquote>
<p>
Where <var>directory</var> is the directory in which you unpacked
the sources.
<br>
If you use the RPM package, <var>directory</var> is
<tt>/usr/share/emacs/ProofGeneral</tt>
</p>
<p>
Further customization is possible via the Customize menus in
Emacs.
<br>
See the <?php fileshow("ProofGeneral/INSTALL","INSTALL")?>
file in the distribution for more details.
</p>
<p>
Please <a href="mailto:proofgen@dcs.ed.ac.uk">send us</a>
any problems, suggestions, or patches.
</p>
<hr>
<!-- WARNING! Line below automatically edited by makefile. -->
<h2><a name="prerel">Pre-release: ProofGeneral-2.2pre990921</a></h2>
<!-- End Warning. -->
<p>
This pre-release of Proof General may be buggy as new
features are added and experimented with.
<br>
Check the
<!-- WARNING! Line below automatically edited by makefile. -->
<?php fileshow("ProofGeneral-2.2pre990921/CHANGES","CHANGES"); ?> file
<!-- End Warning. -->
for a summary of changes since the last stable version, and
the planned changes to come.
<br>
Please test with the current pre-release before reporting any problems
in a pre-release.
</p>
<ul>
<!-- WARNING! Lines below automatically edited by makefile. -->
<li> gzip'ed tar file:
<?php download_link("ProofGeneral-2.2pre990921.tar.gz") ?>
</li>
<li> Linux RPM package
<?php download_link("ProofGeneral-2.2pre990921-1.noarch.rpm") ?>
<br>
The source RPM is
<?php download_link("ProofGeneral-2.2pre990921-1.src.rpm","here") ?>.
</li>
<!-- End Warning. -->
</ul>
<hr>
<h2><a name="devel">For Developers</a></h2>
<p>
If you are interested in helping to develop the core of Proof General,
we provide a complete archive of <i>all</i> the sources used to build the
current Proof General pre-release. The difference from the working
version distribution above is that we include:
</p>
<ul>
<li> provisional instantiations of Proof General to new provers <br>
(mentioned in the
<?php fileshow("ProofGeneral-2.2pre990921/CHANGES","CHANGES"); ?> file),
</li>
<li> the low-level list of things to do, </li>
<li> developer's Makefile used to generate documentation files <br>
and the release itself from our CVS repository, </li>
<li> some test files, </li>
<li> sources for some of the images,
<li> the web pages.
</ul>
<p>
Note: there are no pre-built documentation files in the developer's
release, because developers should have the right tools!
</p>
<ul>
<li> gzip'ed tar file:
<!-- WARNING! Line below automatically edited by makefile. -->
<?php download_link("ProofGeneral-2.2pre990921-devel.tar.gz") ?>
<!-- End Warning. -->
</li>
</ul>
<p>
You probably <em>don't</em> need to download this if you're only
interested in hacking the Emacs lisp part of the program for
a prover that is currently supported. But you may
still like to check the latest
<!-- WARNING! Line below automatically edited by makefile. -->
<?php fileshow("ProofGeneral-2.2pre990921/todo","low-level to-do list"); ?>.
<!-- End Warning. -->
</p>
<p>
We have a mailing list for developers, at
<a href="mailto:proofgeneral-devel@dcs.ed.ac.uk">
<tt>proofgeneral-devel@dcs.ed.ac.uk</tt></a>.
<br>
To subscribe (or unsubscribe), send a message to
<a href="mailto:majordomo@dcs.ed.ac.uk">
<tt>majordomo@dcs.ed.ac.uk</tt>
</a>
with the words "<tt>subscribe proofgeneral-devel</tt>"
(or "<tt>unsubscribe proofgeneral-devel"</tt>) in the message body.
</p>
<p>
If you are interested in developing the core of Proof General,
we can make our CVS repository accessible to you. Please
<a href="feedback.phtml">ask</a>.
</p>
<hr>
<h2><a name="previous">Previous Releases</a></h2>
<p>
Please note that we do not support these old releases in any way.
</p>
<h4>Proof General Version 2.0, released 16th December 1998</h4>
<p>
This version of Proof General has been tested
with XEmacs 20.4 and FSF Emacs 20.2, 20.3.<br>
It supports Coq version 6.2, LEGO version 1.3.1, and
Isabelle version 98-1.<br>
</p>
<ul>
<li> gzip'ed tar file:
<?php download_link("ProofGeneral-2.0.tar.gz") ?>
</li>
<li> Linux RPM package:
<?php download_link("ProofGeneral-2.0-1.noarch.rpm") ?>
<br>
The source RPM is
<?php download_link("ProofGeneral-2.0-1.noarch.rpm","here") ?>.
</li>
</ul>
<p>
|
