aboutsummaryrefslogtreecommitdiff
path: root/html/download.html
diff options
context:
space:
mode:
authorDavid Aspinall2004-02-07 19:31:13 +0000
committerDavid Aspinall2004-02-07 19:31:13 +0000
commitb9caaa8e4b66817dbc66d0e79b567b3285869fea (patch)
treec5420dac1aa1afc28168867ca5cc9c610a46399e /html/download.html
parent87174e13a8aa064f6d00ef9248da9938ea4978f6 (diff)
Deleted file
Diffstat (limited to 'html/download.html')
-rw-r--r--html/download.html248
1 files changed, 0 insertions, 248 deletions
diff --git a/html/download.html b/html/download.html
deleted file mode 100644
index e34b5cbc..00000000
--- a/html/download.html
+++ /dev/null
@@ -1,248 +0,0 @@
-<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"); ?>
-&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 <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>.