Admin/page/dist-content/packages.content

tuned;

%title%
Isabelle Packages

%body%

<p>

The following source and binary packages of <!-- _GP_ distname -->
provide everything required for easy installation of the full Isabelle
working environment on common Unix platforms.

<p>

A <em>minimal</em> Isabelle installation requires only <tt>bash</tt>
and <tt>perl</tt> (usually provided by the operating system), and a
suitable implementation of Standard ML (e.g. Poly/ML as provided
below).  A <em>comfortable</em> Isabelle working environment demands
further user interface support, as provided by <a
href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a>
together with the (optional) <a
href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
package.  Both of these should be used with a recent version of <a
href="http://www.xemacs.org">XEmacs</a> (e.g. version 21.1).

<p>

We provide ready-to-go packages for Isabelle, Proof General and
X-Symbol.  While XEmacs-21 is not included here, most operating system
distributions already provide suitable packages, although not
installed by default.

<p>

Following the example installation procedures below, there is
<em>no</em> separate configuration required of any of these
components.  After installation, users may invoke the Isabelle
executables without further ado.

<p>


<h2>(1) Linux/x86 systems with RPM</h2>

This version of the <!-- _GP_ distname --> distribution is for generic
Linux/x86 systems with RPM package management, as used by most Linux
distributions.  Note that <tt>rpm</tt> requires root user access for
installation.

<p>

<!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
<center>
<table border="0" cellspacing="5" cellpadding="4" width="520">
  <!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") -->
  <!-- _GP_ download("Isabelle system", "isabelle.rpm", "../..") -->
  <!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") -->
  <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "isabelle-HOL-Real.i386.rpm", "../..") -->
  <!-- _GP_ download("Isabelle/ZF image (optional)", "isabelle-ZF.i386.rpm", "../..") -->
  <!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") -->
  <!-- _GP_ download("Proof General (recommended)", "contrib/proofgeneral.rpm", "../..") -->
  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") -->
</table>
</center>

<p>

Example installation procedure (the location of <tt>--prefix
/usr/share</tt> may be changed):

<pre>
rpm -i --prefix /usr/share polyml.i386.rpm
rpm -i --prefix /usr/share isabelle.rpm
rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
rpm -i --prefix /usr/share proofgeneral.rpm
rpm -i --prefix /usr/share xsymbol.rpm
</pre>

Note that installed RPMs may be removed like this:

<pre>
rpm -e xsymbol proofgeneral isabelle-HOL isabelle polyml
</pre>

<p>


<h2>(2) Other Linux/x86 or Solaris/Sparc systems</h2>

The following <!-- _GP_ distname --> distribution works for any
Linux/x86 or Solaris/Sparc system.  Installation does not rely on
package management at all.

<p>

<!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
<center>
<table border="0" cellspacing="5" cellpadding="4" width="520">
  <!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
  <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") -->
  <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
  <!-- _GP_ download("Isabelle system", distname . ".tar.gz", "../..") -->
  <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") -->  <!-- _GP_ download("Proof General (recommended)", "contrib/ProofGeneral.tar.gz", "../..") -->
  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") -->
</table>
</center>

<p>

Example installation in <tt>/usr/local</tt> for Linux/x86:

<pre>
tar -C /usr/local -x -z -f polyml_base.tar.gz
tar -C /usr/local -x -z -f polyml_x86-linux.tar.gz
tar -C /usr/local -x -z -f <!-- _GP_ distname . ".tar.gz"-->
tar -C /usr/local -x -z -f ProofGeneral.tar.gz
tar -C /usr/local -x -z -f x-symbol.tar.gz

cd <!-- _GP_ "/usr/local/" . distname -->
./configure
./build
./bin/isatool install -p /usr/local/bin
</pre>

<p>