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
|
<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.
</p>
<p>
If you are using an older version of a proof assistant,
you may wish to check the
<a href="oldrel.phtml">previous releases</a> of Proof General.
</p>
<hr>
<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.
</p>
<p>
This version of Proof General has been tested
with XEmacs 20.4, XEmacs 21 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>
|
