path: root/html/download.html

<h2>Please register</h2>
<p>
Before downloading Proof General, <i>please</i>
<a href="register">register</a>.
It's free, it only takes a moment.
If you have already registered you do not need to do so again.
<!-- Let's remove this rant for now.  
The statistics collected from registrations are used to help
make a case for support for Proof General, and nothing else.  
It is likely that development of Proof General will <i>finish soon</i> 
unless we 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 or even a paper letter to the <a
href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>.  And if you
can offer to help resource the development of Proof General
in some way, please
<a href="feedback">contact us</a>. -->
</p>

<p>
You can join the
Proof General
<a href="mailinglist">mailing list</a>
for announcements of new versions.
Developers and beta-testers may like to download
a <a href="develdownload.html">development release</a>
of Proof General.
If you use an old version of a proof assistant and/or an
old Emacs version, you may need to download one of the 
<a href="oldrel.php">previous releases</a>.
</p>
<h2><a name="stable">
    Proof General Version 3.4, to be released August 2002.
    </a>
</h2>
<p>
Proof General is distributed under the terms of
the 
<?php fileshow("ProofGeneral/COPYING","GNU General Public License"); ?>.
<br>
See <a href="#prereq">below</a> for software pre-requisites for running Proof General.
</p>

<p>
The next stable version of Proof General will be 3.4, to be released
in August.  Until then, please try a 
<a href="develdownload.html">development release</a> and
<a href="feedback">report any difficulties</a>, 
to help make the next release of Proof General as 
robust as possible.  Thanks!

<!--
<p>
Proof General is available as an archive and an RPM package.
</p>
<table width="80%" cellspacing=8>
<tr>
<td width=150>gzip'ed tar file</td>
<td><?php download_link("ProofGeneral-3.3.tar.gz") ?></td>
</tr>
<tr>
<td>zip file</td>
<td><?php download_link("ProofGeneral-3.3.zip") ?></td>
</tr>
<tr>
<td>RPM package </td>
<td><?php download_link("ProofGeneral-3.3-1.noarch.rpm") ?></td>
</tr>
<tr>
<td>individual files</td>
<td><a href="ProofGeneral-3.3">browse individual files</a>
</tr>
</table>
<p>
Both the tarball and the RPM package include the generic elisp
code, 
code for the supported provers, installation instructions
and documentation in Info and HTML formats.
Documentation is available in other formats
here <a href="doc">here</a>.  
If you want to format the documentation yourself,
you may like to download the
<?php download_link("ProofGeneralPortrait.eps.gz", 
"front page image") ?>.
Note that we don't ship an SRPM now, since you can build the RPM directly 
from the source tarball using <tt>rpm -ta</tt>.
</p>
<p>
-->

<!--
This version of Proof General has been tested
with XEmacs 21.4 and (briefly with) GNU Emacs 20.7.
It supports earlier versions of both Emacsen, but
we recommend using these versions.
This version of Proof General does <b>not</b> support 
GNU Emacs 21.x, please try out a <a href="develdownload.html">development release</a>
instead.
</p>
<p>
Check the <?php fileshow("ProofGeneral-3.3/CHANGES","CHANGES"); ?> file
for a summary of changes since version 3.2.
</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," ); ?>)
before reporting problems.  If you find a problem not already mentioned, 
please 
<?php hlink("feedback.html","send us a note","Feedback form")?>.
</p>
-->

<br>
<br>

<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 21.1 of 
<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
<br>
Both Emacsen are available for a variety of platforms, including
Unix variants, Windows 95/98/NT/2k, and Mac OS.
</li>
<li>
A proof assistant, for example:
<?php fileshow("ProofGeneral/coq/README","Coq"); ?>;
<?php fileshow("ProofGeneral/isa/README","Isabelle"); ?>
&nbsp;or <?php fileshow("ProofGeneral/isa/README","Isabelle/Isar"); ?>;
<?php fileshow("ProofGeneral/lego/README","LEGO"); ?>;
<?php fileshow("ProofGeneral/phox/README","PhoX"); ?>.
<br>
(click on links for version details; see <a href=".">front page</a> for
other assistants).
<br>
Or write your own support for a new assistant!
</li>
</ul>
</p>

<p>
There is also an <strong>optional</strong> component for using
Proof General:
<ul>
<li>
For displaying logical and mathematical symbols, the excellent
<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
package. 
<br>It's very easy to install.  See <a href="#xsyminstall">here</a> 
for installation notes.
<br>Versions of X-Symbol supported:
<b>version 3.4 (stable)</b>, and <b>version 4.4 (beta)</b>.
<br>
The stable version of X-Symbol only works with XEmacs on systems running X.
The beta version also works with Emacs 21.1 and later, and has limited
support for XEmacs on Windows.
</li>
<!-- <li> -->
<!-- For GNU Emacs, a version of <tt>func-menu.el</tt> to get  -->
<!-- <a href="features#funcmenu">function menus</a>. -->
<!-- <br>Unfortunately I can't find a version of this that -->
<!-- works with current GNU 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>
Compatibility across the multitude of Emacs versions is quite troublesome. 
<br>
XEmacs has been better tested with Proof General than GNU Emacs.
<br>
Earlier versions of either variant <i>may</i> work with Proof General
but are not officially supported because we cannot test backward
compatibility widely. Please <a href="feedback">send us fixes</a>
rather than bug reports if you discover problems.
Later versions of both Emacs variants <i>should</i> work with
Proof General: if you discover problems, please check
to see if they have been solved in a more recent
<a href="develdownload">development release</a> before
reporting.


<h3><a name="install">Easy installation of Proof General</a></h3> 
<p>
To use Proof General, simply unpack the sources with 
</p>
 <blockquote>
   <tt>tar xpzf ProofGeneral-3.4.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.4/INSTALL","INSTALL")?> 
file in the distribution for more details.
</p>

<h3><a name="xsyminstall">Easy installation of X-Symbol</a></h3> 

<p>
X-Symbol is easy to install in XEmacs 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/xemacs-packages<br>
 cd ~/.xemacs/xemacs-packages<br>
 tar xpzf ../x-symbol-pkg.tar.gz<br>
</tt></blockquote>
<p>
For GNU Emacs, you must remove the <tt>.elc</tt> files supplied, and
add some code to your <tt>.emacs</tt>.  See 
<a href="http://x-symbol.sourceforge.net/news.html">this page</a>
for details.
More installation options are given
in the <a href="http://x-symbol.sourceforge.net/man/x-symbol_2.html">the X-Symbol manual</a>.