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
|
<h2>Please register</h2>
<p>
Before downloading Proof General, <i>please</i>
<a href="register.phtml">register</a>.
It's free, it only takes a moment.
If you have already registered you do not need to do so again.
</p>
<p>
The statistics collected from registrations will be used to help a
case for support for Proof General, and nothing else. It is likely
that development of Proof General will <i>finish very soon</i> unless
we can find new resources. As a courtesy, we do not make registration
compulsory and I can tell from the server logs that the majority of
people downloading do not register. But if you don't register
now, please consider returning to register later if you find Proof
General interesting or useful. If you don't want to fill the form,
please <a href="mailto:proofgen@dcs.ed.ac.uk">send an email</a>
directly.
</p>
<p>
You may like to join the
Proof General
<a href="mailinglist.phtml">mailing list</a>.
Developers and beta-testers may like to download
a <a href="develdownload.phtml">development release</a>
of Proof General.
If you use an old version of a proof assistant,
you may need to download one of the
<a href="oldrel.phtml">previous releases</a>.
</p>
<p>
Please check the
<?php fileshow("ProofGeneral/COPYING","license conditions "); ?>
for using Proof General.
</p>
<h2><a name="prereq">
What you need to run Proof General
</a>
</h2>
<p>
To run Proof General, you <strong>must</strong> have:
</p>
<ul>
<li>
Version 21.1 or later
of <a href="http://www.xemacs.org">XEmacs</a>
(this UK
<a href="http://sunsite.doc.ic.ac.uk/Mirrors/ftp.xemacs.org/pub/xemacs/">
ftp mirror</a> may help).
<br>
<b>or</b> version 20.5 or later of the much poorer
<a href="http://www.gnu.org/software/emacs/">FSF GNU Emacs</a>.
<br>
Both Emacsen are available for a variety of platforms, including
Unix variants and Windows 95/98/NT.
</li>
<li>
One or more of the supported proof assistants. Or write your own
support for a new assistant.
<br>
See the
<?php link_root("main","front page") ?> for links to supported
assistants.
</li>
</ul>
<p>
There are also some <strong>optional</strong> components for using
Proof General:
<ul>
<li>
For displaying logical and mathematical symbols, the excellent
<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
package.
<br>It's very easy to install. See <a href="#xsyminstall">here</a>
for installation notes.
<br>X-Symbol presently only works with XEmacs on systems running X.
</li>
<!-- <li> -->
<!-- For FSF Emacs, a version of <tt>func-menu.el</tt> to get -->
<!-- <?php link_root("features#funcmenu","function menus") ?>. -->
<!-- <br>Unfortunately I can't find a version of this that -->
<!-- works with current FSF Emacs releases. I'd be grateful -->
<!-- for a pointer to one. -->
<!-- <br> -->
<!-- (The package -->
<!-- <tt>imenu.el</tt> may be a suitable replacement, -->
<!-- and it ships with both Emacsen. Perhaps -->
<!-- somebody could contribute patches to use that -->
<!-- instead of <tt>func-menu</tt>). -->
</ul>
<p>
All components mentioned above are distributed under the GPL license.
</p>
<br>
<br>
<h2><a name="stable">
Proof General Version 3.1, released 23rd March 2000
</a>
</h2>
<p>
Proof General is available as an archive and an RPM package.
</p>
<ul>
<li> gzip'ed tar file:
<?php download_link("ProofGeneral-3.1.tar.gz") ?>,
<br>
or the same thing in a zip file:
<?php download_link("ProofGeneral-3.1.zip") ?>,
</li>
<li> Linux RPM package:
<?php download_link("ProofGeneral-3.1-1.noarch.rpm") ?>
<br>
You probably don't need the
<?php download_link("ProofGeneral-3.1-1.src.rpm",
"source RPM") ?>.
</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 (in Info and HTML formats).
</p>
<p>
Documentation is available in other formats
here <?php link_root("doc","here") ?>.
If you want to format the documentation yourself,
you may like to download the
<?php download_link("ProofGeneralPortrait.eps.gz",
"front page image") ?>.
</p>
<p>
This version of Proof General has been tested
with XEmacs 21.1 and FSF Emacs 20.4.
It supports Coq version 6.3, LEGO version 1.3.1 and
Isabelle99.
</p>
<p>
Check the <?php fileshow("ProofGeneral-3.1/CHANGES","CHANGES"); ?> file
for a summary of changes since version 3.0.
</p>
<p>
Check the latest <?php fileshow("ProofGeneral/BUGS","BUGS"); ?> file
(also
<?php fileshow("ProofGeneral/lego/BUGS","lego/BUGS, "); ?>
<?php fileshow("ProofGeneral/coq/BUGS","coq/BUGS, "); ?>
<?php fileshow("ProofGeneral/isa/BUGS","isa/BUGS, "); ?>
<?php fileshow("ProofGeneral/isar/BUGS","isar/BUGS," ); ?>)
<!-- <?php fileshow("ProofGeneral/hol98/BUGS","hol98/BUGS"); ?>) -->
before reporting problems. If you find a problem not already mentioned,
please
<?php hlink("feedback.phtml","send us a note","Feedback form")?>.
</p>
<br>
<br>
<h3><a name="install">Easy installation</a></h3>
<p>
To use Proof General, simply unpack the sources with
</p>
<blockquote>
<tt>tar xpzf ProofGeneral-3.1.tar.gz</tt>
</blockquote>
<p>
(use <tt>gunzip</tt> first in place of <tt>z</tt> 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>
If you're using Windows, then download the zip file.
<br>
Use a zip file utility to unpack it somewhere, for example
<tt>c:\\ProofGeneral</tt>
</p>
<p>
Further customization is possible via the Customize menus in
Emacs.
<br>
See the <?php fileshow("ProofGeneral-3.1/INSTALL","INSTALL")?>
file in the distribution for more details.
</p>
<h3><a name="xsyminstall">Easy installation of X-Symbol</a></h3>
<p>
Contrary to what you may expect from the documentation of
X-Symbol, it's very easy to install and configures itself
automatically.
</p>
<p>
Simply download the binary package file, and do something
like this to install in your home directory:
</p>
<blockquote><tt>
mkdir -p ~/.xemacs<br>
cd ~/.xemacs<br>
tar xpzf ../x-symbol-pkg.tar.gz<br>
</tt></blockquote>
|
