INSTALL

updated;

Isabelle installation and compilation notes
===========================================

1) User installation
--------------------

Here we assume that Isabelle has already been installed at your site.
Otherwise see 2) below of how to get the Isabelle system installed in
the first place.


1a) Running the Isabelle binaries
---------------------------------

The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
directly from their location within the distribution directory
[ISABELLE_HOME] like this:

  [ISABELLE_HOME]/bin/isabelle HOL

This starts an interactive Isabelle session within your current text
terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
search PATH, but this is not strictly necessary.


Please do *not* copy (or link) the Isabelle scripts anywhere else ---
they just won't work!  If you really want to install independent
Isabelle binaries somewhere else then do it like this:

  [ISABELLE_HOME]/bin/isatool install -p ~/bin

Your site-wide Isabelle installation may already provide Isabelle
executables in some global bin directory (such as /usr/bin).


1b) Isabelle as KDE application
-------------------------------

Isabelle may be installed as application icon on the KDE desktop like
this:

  [ISABELLE_HOME]/bin/isatool install -k

You may have to refresh the KDE desktop in order to see the new icon.
Clicking on Isabelle will invoke the interface wrapper script (capital
Isabelle), which is usually configured to run Proof General (see also
the ISABELLE_INTERFACE setting).  Additional options may be passed to
Isabelle by editing the application's command line using the standard
KDE desktop functionality.


2) System installation
----------------------

The Isabelle distribution is available both as traditional source-only
tar.gz archives, and as binary packages (currently only RPM for
Linux/x86).  In any case, the resulting Isabelle installation always
contains the full sources, thus any part of the system be recompiled
later, too.


2a) Binary installation
----------------------

Ready-to-go RPM packages are provided for the ML compiler and runtime
system, the Isabelle sources, and some major object-logics.  These
packages should work on any major Linux/x86 platform based on RPM
package management.

A minimal installation would work like this (executed as root):

  rpm -i --force --prefix /usr/share polyml.i386.rpm
  rpm -i --force --prefix /usr/share isabelle.rpm
  rpm -i --force --prefix /usr/share isabelle-HOL.i386.rpm

The install prefix may be changed as indicated.  By default the ML
system (and other contributed packages) are expected in either of the
following three locations:

  1) [ISABELLE_HOME]/contrib
  2) [ISABELLE_HOME]/..
  3) /usr/share
  4) /usr/local

This may be changed by editing [ISABELLE_HOME]/etc/settings manually.

Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
Isabelle as platform independent sources.  Precompiled object-logics
are provided for convenience.


Recompiling logics
------------------

Some people prefer to be able to reconstruct the full system from the
sources, rather than installing precompiled packages blindly.  We do
not provide source RPMs, yet any parts of Isabelle may be recompiled
after installation of the main isabelle.rpm package (which contains
only sources anyway).

Assuming proper configuration of the underlying ML system, Isabelle
object-logics may be recompiled like this:

  [ISABELLE_HOME]/build HOL FOL


Source installation
-------------------

Traditional tar.gz archives are provided for the full Isabelle sources
and documentation as well.  Make sure your ML system (e.g. Poly/ML
etc.) has already been installed properly; then proceed as follows.

* Unpacking the archives.  After unpacking the Isabelle distribution
archives (using tar and gzip) you are left with some directory
IsabelleYY-X.

* Auto configuration.  There are some minor adaptions to be made of
the Isabelle distribution to your system environment (locations of
bash and perl).  Simply do it like this:

  cd [ISABELLE_HOME]
  ./configure

Note that this does not store any references to [ISABELLE_HOME].  You
may safely move the system later, without having to run ./configure
again.

* ML system settings and compilation.  Before actual compilation you
have to tell Isabelle about your Standard ML system.  These settings
reside in ./etc/settings, which may be also overridden by
~/isabelle/etc/settings. There are already various sample
configurations in ./etc/settings commented out.

To build the core Isabelle/Pure and the default object-logic, just
type

  ./build

More object-logics can be made in a similar fashion:

  ./build FOL HOL

Explicit make targets may be given as follows:

  ./build -m HOL-Real HOL

After successful compilation you are ready to run the system, see 1)
above for more information.


$Id$