diff options
Diffstat (limited to 'html/download.html')
| -rw-r--r-- | html/download.html | 248 |
1 files changed, 248 insertions, 0 deletions
diff --git a/html/download.html b/html/download.html new file mode 100644 index 00000000..e34b5cbc --- /dev/null +++ b/html/download.html @@ -0,0 +1,248 @@ +<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 early-adopters 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, released 29th 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> +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.4.tar.gz") ?></td> +</tr> +<tr> +<td>zip file</td> +<td><?php download_link("ProofGeneral-3.4.zip") ?></td> +</tr> +<tr> +<td>RPM package </td> +<td><?php download_link("ProofGeneral-3.4-1.noarch.rpm") ?> +<br>NB: to build yourself use the tar file with <tt>rpm -ta</tt>.</td> +</tr> +<tr> +<td>individual files</td> +<td><a href="ProofGeneral-3.4">browse individual files</a> +</tr> +</table> +<p> +The archives and RPM include almost everything: the generic +code, specific 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") ?>. --> +</p> + +<p> This version of Proof General has been tested with XEmacs 21.4 and +GNU Emacs 21.2. It should work with <i>some</i> earlier versions of +XEmacs, but we recommend using these Emacs versions for the most +reliable results. Support on GNU Emacs is catching up, but XEmacs is +still the better tested and more fully-featured environment. +See below for links. +</p> +<p> +See the <?php +fileshow("ProofGeneral-3.4/etc/announce","announcement"); ?> for more +details, or check the <?php +fileshow("ProofGeneral-3.4/CHANGES","CHANGES"); ?> file for a summary +of changes since version 3.3. +</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> + +<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 21.4 +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.2 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"); ?> + 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 <i>partially</i>, <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.4 (not yet available), 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>. |