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$