diff options
Diffstat (limited to 'html/download.html')
| -rw-r--r-- | html/download.html | 224 |
1 files changed, 224 insertions, 0 deletions
diff --git a/html/download.html b/html/download.html new file mode 100644 index 00000000..ee94ef94 --- /dev/null +++ b/html/download.html @@ -0,0 +1,224 @@ +<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. +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> (quickly!). +</p> + +<p> +You may like to join the +Proof General +<a href="mailinglist">mailing list</a>. +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, +you may need to download one of the +<a href="oldrel.php">previous releases</a>. +</p> +<p> +Please check the +<?php fileshow("ProofGeneral/COPYING","license conditions "); ?> +for using Proof General. +<br> +See <a href="#prereq">below</a> for software pre-requisites for running Proof General. +</p> + +<h2><a name="stable"> + Proof General Version 3.3, released 10th September 2001 + </a> +</h2> + +<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> +<!-- WARNING! Lines below automatically edited by makefile. --> +<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 the latest versions available. +</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," ); ?>) +<!-- <?php fileshow("ProofGeneral/hol98/BUGS","hol98/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 20.7 of the much poorer +<a href="http://www.gnu.org/software/emacs/">GNU GNU Emacs</a>. +<br> +Both Emacsen are available for a variety of platforms, including +Unix variants and Windows 95/98/NT/2k. +</li> +<li> +One or more of the supported proof assistants. Or write your own +support for a new assistant. +<br> +See the +<a href="main">front page</a> 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://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>X-Symbol presently only works with XEmacs on systems running X. +</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> +<p> +All components mentioned above are distributed under the GPL license. +</p> +<br> +<br> + +<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.3.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.3/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 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> +<p> +NB: if you have version 21.x of XEmacs, you may need to install +x-symbol inside a subdirectory +<tt>~/.xemacs/xemacs-packages</tt> instead of +<tt>~/.xemacs</tt>. + |