Admin/page/dist-content/binary.content

dummy (generated by makedist);

%title%
Isabelle Binary Distribution

%body%

<p>

<strong>NOTE.</strong> The binary distribution is designed for easy
installation of Isabelle, and related tools such as Proof General and
X-Symbol.  There is no manual intervention required, provided that the
versions of packages as provided below are used.


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

This is the binary distribution of <!-- _GP_ distname --> for
Linux/x86 systems.  It requires RPM based package management (as used
by most Linux distributions), and root user access to install.

<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 main 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 system (recommended)", "contrib/proofgeneral.rpm", "../..") -->
  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") -->
</table>
</center>

<p>

Example installation in <tt>/usr/share</tt> (the default location):

<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               #requires XEmacs-21
rpm -i --prefix /usr/share xsymbol.rpm
</pre>

<p>


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

The following distribution of <!-- _GP_ distname --> works for any
Linux/x86 or Solaris/Sparc system -- only Poly/ML is platform
dependent.  Installation does not rely on package management; it may
be performed by non-root users as well.

<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 main system", distname . ".tar.gz", "../..") -->
  <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") -->  <!-- _GP_ download("Proof General system (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            #requires XEmacs-21
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>

<p>