--- a/Admin/website/installation.html Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/installation.html Mon Sep 26 20:52:36 2005 +0200
@@ -19,19 +19,22 @@
<h2>General</h2>
<p>
- Isabelle runs on common Unix platforms.
- For Linux, Solaris and MaxOS / Darwin, we provide ready-to-install bundles;
- for other Unices, Isabelle has to be built from scratch.
+ Isabelle runs on common Unix platforms. We provide
+ ready-to-use binary packages for Linux/x86, MaxOS X /
+ Darwin, and Solaris. For other platforms, Isabelle logics
+ need to be compiled separately (see also <a
+ href="//dist/packages/Isabelle/INSTALL">INSTALL</a>).
</p>
<p>
- A usable Isabelle system consists of the following components:
+ A practically usable Isabelle system consists of the
+ following components:
</p>
<ul>
<li>a suitable ML environment for Standard ML</li>
- <li>the Isabelle system itself, including the desired object logic(s)
- (e. g. HOL)</li>
+ <li>the Isabelle system itself, including the desired object logics
+ (e. g. HOL, HOL-Complex)</li>
<li>the ProofGeneral user interface</li>
</ul>
@@ -42,157 +45,130 @@
<ul>
<li><a href="#install_linux">Linux (x86)</a></li>
+ <li><a href="#install_darwin">MacOS X / Darwin (ppc)</a></li>
<li><a href="#install_solaris">Solaris (sparc)</a></li>
- <li><a href="#install_darwin">MacOS X / Darwin</a></li>
- <li><a href="#install_windows">Windows</a></li>
</ul>
<h2 id="install_linux">Linux</h2>
- <p>Commonly, an installation of Isabelle could work as follows:</p>
+ <p>Installation of Isabelle/HOL on common Linux/x86 platforms
+ works as follows:</p>
<ul>
- <li>Ensure that your system has a running XEmacs 21 or Emacs 21
- with mule support (for ProofGeneral)</li>
- <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
- <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
- the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
- and Isabelle,
- either from our <a href="download.html">package page</a> or from the
- links below. When you download ProofGeneral, please
- <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
+ <li>For ProofGeneral, ensure that your system has a
+ working installation of XEmacs 21, or Emacs 21 with
+ mule support. The XEmacs 21.1.x and 21.4.x versions
+ are known to work reasonably well, but the beta branch
+ of XEmacs 21.5.x usually fails!</li>
+
+ <li>Get the packages for <a
+ href="http://www.polyml.org">Poly/ML</a>, <a
+ href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a>
+ and Isabelle – all of this is available from the
+ Isabelle <a href="download.html">Packages</a> page.
+ When you download ProofGeneral for the first time,
+ please <a
+ href="http://proofgeneral.inf.ed.ac.uk/register">register</a>.</li>
+
+ <li>Likewise download the compiled images of the desired
+ Isabelle object logics.</li>
+
<li>Unpack the archives to an appropriate location, e. g.
<tt class="shellcmd">/usr/local</tt>:
<ul class="shellcmd">
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
</ul>
</li>
- <li>Under most circumstances, the default settings of Isabelle should be reasonable for
- invoking Isabelle/ProofGeneral without further ado:
+
+ <li>Under most circumstances, the default settings of
+ Isabelle should be reasonable for invoking
+ Isabelle/ProofGeneral without further ado:
<ul class="shellcmd">
<li>/usr/local/Isabelle/bin/Isabelle</li>
</ul>
- Note that there is a separate option in
- the Proof General <em>Options</em> menu to enable X-Symbol.
- </li>
- <li>If Emacs appears to hang when the prover process is started, see the
- <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
- advice.
+
+ Failure on this is typically a problem with unstable
+ XEmacs versions; consider command line option
+ <code>-p</code> to specify a different xemacs
+ executable.
+
+ The X-Symbol package is already included in Proof
+ General, but needs to be enabled separately; use the
+ <code>-x</code> command line option, or the
+ <em>Options</em> menu.
</li>
</ul>
- <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
+ <h2 id="install_darwin">MaxOS X / Darwin</h2>
+
+ <p>Ensure that your system provides the following:</p>
+ <ul>
+ <li>MacOS X 10.2.2 or higher</li>
+
+ <li>XEmacs 21, or Emacs 21 with mule support (for
+ ProofGeneral) – for further reference, see the
+ <a href="installation_macos_emacs.html">MacOS X Emacs
+ hints</a>. </li>
+ </ul>
+
+ <p>Then installation on MacOS X / Darwin is analogous to
+ Linux, but note that some GNU executables are named
+ differently.</p>
+
+ <ul>
+ <li>Unpack the archives to an appropriate location, e. g.
+ <tt class="shellcmd">/usr/local</tt>:
+ <ul class="shellcmd">
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li>
+ </ul>
+ </li>
+
+ <li>Invoke Isabelle/ProofGeneral as follows:
+ <ul class="shellcmd">
+ <li>/usr/local/Isabelle/bin/Isabelle</li>
+ </ul>
+ </li>
+
+ </ul>
<h2 id="install_solaris">Solaris</h2>
- <p>Before you start, ensure the following for your system:</p>
+ <p>Ensure that the following tools are available on your system:</p>
<ul>
+ <li>Perl 5.x</li>
<li>GNU bash 2.x</li>
- <li>perl 5.x</li>
<li>GNU tar 1.13 or higher</li>
<li>GNU gzip 1.3 or higher</li>
- <li>running XEmacs 21 or Emacs 21
- with mule support (for ProofGeneral)</li>
+ <li>XEmacs 21, or Emacs 21 with mule support (for ProofGeneral)</li>
</ul>
- <p>Then, an installation on Solaris is analogous to Linux:</p>
+ <p>The rest of the installation is analogous to Linux (see
+ above).</p>
<ul>
- <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
- <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
- the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
- and Isabelle,
- either from our <a href="download.html">package page</a> or from the
- links below. When you download ProofGeneral, please
- <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
<li>Unpack the archives to an appropriate location, e. g.
<tt class="shellcmd">/usr/local</tt>:
<ul class="shellcmd">
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.tar.gz"?></li>
</ul>
</li>
- <li>Under most circumstances, the default settings of Isabelle should be reasonable for
- invoking Isabelle/ProofGeneral without further ado:
+
+ <li>Invoke Isabelle/ProofGeneral as follows:
<ul class="shellcmd">
<li>/usr/local/Isabelle/bin/Isabelle</li>
</ul>
- Note that there is a separate option in
- the Proof General <em>Options</em> menu to enable X-Symbol.
- </li>
- <li>If Emacs appears to hang when the prover process is started, see the
- <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
- advice.
- </li>
- </ul>
-
- <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
-
- <h2 id="install_darwin">MaxOS X / Darwin</h2>
-
- <p>Before you start, ensure the following for your system:</p>
- <ul>
- <li>running MacOS X 10.2.2 or higher</li>
- <li>running XEmacs 21 or Emacs 21 with mule support (for ProofGeneral)
- – for further reference, see the
- <a href="installation_macos_emacs.html">MacOS X Emacs hints</a>
</li>
</ul>
- <p>Then, an installation on Darwin is analogous to Linux:</p>
-
- <ul>
- <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
- <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
- the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
- and Isabelle,
- either from our <a href="download.html">package page</a> or from the
- links below. When you download ProofGeneral, please
- <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
- <li>Unpack the archives to an appropriate location, e. g.
- <tt class="shellcmd">/usr/local</tt>:
- <ul class="shellcmd">
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li>
- </ul>
- </li>
- <li>Under most circumstances, the default settings of Isabelle should be reasonable for
- invoking Isabelle/ProofGeneral without further ado:
- <ul class="shellcmd">
- <li>/usr/local/Isabelle/bin/Isabelle</li>
- </ul>
- Note that there is a separate option in
- the Proof General <em>Options</em> menu to enable X-Symbol.
- </li>
- <li>If Emacs appears to hang when the prover process is started, see the
- <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
- advice.
- </li>
- </ul>
-
- <h2 id="install_windows">Windows</h2>
-
- <p>Isabelle does not run nativly on Windows; in a restricted fashion,
- you may run Isabelle on Windows using the Cygwin environment.
- See <a href="installation_notes_cygwin.html">Installation notes for
- Cygwin/Windows</a>.</p>
-
- <p>For a serious apporach, you should consider a Windows/Linux dualboot
- installation.</p>
-
</div>
<div class="hr"><hr/></div>
<?include file="//include/footer.include.html"?>