diff options
| author | David Aspinall | 2004-02-07 19:31:13 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-02-07 19:31:13 +0000 |
| commit | b9caaa8e4b66817dbc66d0e79b567b3285869fea (patch) | |
| tree | c5420dac1aa1afc28168867ca5cc9c610a46399e /html/download.html | |
| parent | 87174e13a8aa064f6d00ef9248da9938ea4978f6 (diff) | |
Deleted file
Diffstat (limited to 'html/download.html')
| -rw-r--r-- | html/download.html | 248 |
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"); ?> - 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>. |
