diff options
| -rw-r--r-- | html/download.html | 214 | ||||
| -rw-r--r-- | html/index.html | 9 |
2 files changed, 223 insertions, 0 deletions
diff --git a/html/download.html b/html/download.html new file mode 100644 index 00000000..03948ac0 --- /dev/null +++ b/html/download.html @@ -0,0 +1,214 @@ +<h2>Please register</h2> +<p> +Before downloading Proof General, <i>please</i> +<a href="register.html">register</a>. +It's free, it only takes a moment. +If you have already registered you do not need to do so again. +</p> +<p> +The statistics collected from registrations 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. 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. +</p> + +<p> +You may like to join the +Proof General +<a href="mailinglist.html">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.html">previous releases</a>. +</p> +<p> +Please check the +<?php fileshow("ProofGeneral/COPYING","license conditions "); ?> +for using Proof General. +</p> + +<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.5 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 Windows 95/98/NT. +</li> +<li> +One or more of the supported proof assistants. Or write your own +support for a new assistant. +<br> +See the +<?php link_root("main","front page") ?> 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://www.fmi.uni-passau.de/~wedler/x-symbol/">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 FSF Emacs, a version of <tt>func-menu.el</tt> to get --> +<!-- <?php link_root("features#funcmenu","function menus") ?>. --> +<!-- <br>Unfortunately I can't find a version of this that --> +<!-- works with current FSF 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> + + +<h2><a name="stable"> + Proof General Version 3.1, released 23rd March 2000 + </a> +</h2> + +<p> +Proof General is available as an archive and an RPM package. +</p> +<ul> + <li> gzip'ed tar file: + <?php download_link("ProofGeneral-3.1.tar.gz") ?>, + <br> + or the same thing in a zip file: + <?php download_link("ProofGeneral-3.1.zip") ?>, + </li> + <li> Linux RPM package: + <?php download_link("ProofGeneral-3.1-1.noarch.rpm") ?> + <br> + You probably don't need the + <?php download_link("ProofGeneral-3.1-1.src.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("doc","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 21.1 and FSF Emacs 20.4. +It supports Coq version 6.3, LEGO version 1.3.1 and +Isabelle99. +</p> +<p> +Check the <?php fileshow("ProofGeneral-3.1/CHANGES","CHANGES"); ?> file +for a summary of changes since version 3.0. +</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> + +<h3><a name="install">Easy installation</a></h3> +<p> +To use Proof General, simply unpack the sources with +</p> + <blockquote> + <tt>tar xpzf ProofGeneral-3.1.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.1/INSTALL","INSTALL")?> +file in the distribution for more details. +</p> + +<h3><a name="xsyminstall">Easy installation of X-Symbol</a></h3> + +<p> +Contrary to what you may expect from the documentation of +X-Symbol, it's very 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> diff --git a/html/index.html b/html/index.html new file mode 100644 index 00000000..f0cbe7a1 --- /dev/null +++ b/html/index.html @@ -0,0 +1,9 @@ +<?php require('functions.php3'); ?> +<html> +<?php include('head.html'); ?> +<?php + include('header.html'); + include($WANTED . '.html'); + footer(); +?> + |