<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Installation instructions</title>
<?include file="//include/htmlheader.include.html"?>
</head>
<body>
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
<h2>General</h2>
<p>
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/Isabelle/INSTALL">INSTALL</a>).
</p>
<p>
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 logics
(e. g. HOL, HOL-Complex)</li>
<li>the ProofGeneral user interface</li>
</ul>
<p>Optionally, theory graph browsing may be used if a Java JRE 1.1 or above
is installed.</p>
<p>For operating-system-specific instructions:</p>
<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>
</ul>
<h2 id="install_linux">Linux</h2>
<p>Installation of Isabelle/HOL on common Linux/x86 platforms
works as follows:</p>
<ul>
<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/Isabelle2005.tar.gz"?></li>
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_x86-linux.tar.gz"?></li>
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/HOL_x86-linux.tar.gz"?></li>
<li>tar -C /usr/local -xzf <?downloadLink target="//dist/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:
<ul class="shellcmd">
<li>/usr/local/Isabelle/bin/Isabelle</li>
</ul>
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>
<li>Isabelle may also be run without ProofGeneral, as a
plain shell process as follows:
<ul class="shellcmd">
<li>/usr/local/Isabelle/bin/isabelle-process -I</li>
</ul>
Type CTRL-D to exit.
If the above does not work at all, maybe you are
suffering from a known problem of Poly/ML on certain
Linux versions, see also <a
href="http://www.polyml.org/linuxsegfault.html">Segmentation
faults with Linux</a> on the Poly/ML site.
</li>
</ul>
<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/Isabelle2005.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_ppc-darwin.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/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>Ensure that the following tools are available on your system:</p>
<ul>
<li>Perl 5.x</li>
<li>GNU bash 2.x</li>
<li>GNU tar 1.13 or higher</li>
<li>GNU gzip 1.3 or higher</li>
<li>XEmacs 21, or Emacs 21 with mule support (for ProofGeneral)</li>
</ul>
<p>The rest of the installation is analogous to Linux (see
above).</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/Isabelle2005.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_sparc-solaris.tar.gz"?></li>
<li>gtar -C /usr/local -xzf <?downloadLink target="//dist/HOL_sparc-solaris.tar.gz"?></li>
</ul>
</li>
<li>Invoke Isabelle/ProofGeneral as follows:
<ul class="shellcmd">
<li>/usr/local/Isabelle/bin/Isabelle</li>
</ul>
</li>
</ul>
</div>
<div class="hr"><hr/></div>
<?include file="//include/footer.include.html"?>
</body>
</html>