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
|
<h2>Please register</h2>
<p>
Before downloading Proof General, <i>please</i>
<a href="register.phtml">register</a>.
It only takes a moment.
<br>
The information collected 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.
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>
Developers and beta-testers may like to download
a <a href="devel.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>
<hr>
<h2><a name="prereq">
What you need to run Proof General
</a>
</h2>
<p>
To run Proof General, you should have:
</p>
<ul>
<li>
Version 20.4 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.2 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 NT.
</li>
<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>X-Symbol presently only works with XEmacs.
Its use with Proof General is optional.
</li>
<li>
For FSF Emacs, a version of <tt>func-menu.el</tt> to get
<?php link_root("features#funcmenu","function menus") ?>.
<br>I haven't been able to find a recent version of this that
works with FSF Emacs, I'd be grateful if anyone can send me
a pointer or a hacked version which does.
Proof General works fine without this feature.
</ul>
<p>
All these components are distributed under the
GPL license.
</p>
<br>
<br>
<h2><a name="stable">
Proof General Version 2.1, released 24th August 1999
</a>
</h2>
<p>
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>
You probably don't need the
<?php download_link("ProofGeneral-2.1-1.noarch.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("download","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 20.4, XEmacs 21.1 and FSF Emacs 20.3.
It supports Coq version 6.3, LEGO version 1.3.1 and
some pre-release versions of Isabelle version 99.
Check the <?php fileshow("ProofGeneral-2.1/CHANGES","CHANGES"); ?> file
for a summary of changes since version 2.0.
</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> first 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>
|
