Isabelle installation notes

===========================

1) System installation

----------------------

The Isabelle distribution includes both complete sources and

precompiled binary packages for common Unix platforms.

Quick installation

------------------

Ready-to-go packages are provided for the ML compiler and runtime

system, the Isabelle sources, and some major object-logics.  A minimal

site installation of Isabelle on Linux/x86 works like this:

  tar -C /usr/local -xzf Isabelle.tar.gz

  tar -C /usr/local -xzf polyml_base.tar.gz

  tar -C /usr/local -xzf polyml_x86-linux.tar.gz

  tar -C /usr/local -xzf HOL_x86-linux.tar.gz

The install prefix given above may be changed as appropriate.  By

default the ML system (and other contributed packages) are expected in

any of the following locations:

  1) [ISABELLE_HOME]/contrib

  2) [ISABELLE_HOME]/..

  3) /usr/share

  4) /usr/local

  5) /opt

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

The installation may be finished as follows:

  cd [ISABELLE_HOME]

  ./configure

  ./bin/isatool install -p /usr/local/bin

Note that the configure script is only required for systems that do

not have bash and perl in the canonical places (/bin/bash and

/usr/bin/perl).

The install utility creates global references to the present Isabelle

installation, enabling users to invoke the Isabelle executables

without explicit path names.  Incidently, this is the only place where

a static reference to [ISABELLE_HOME] is created; thus isatool install

has to be run again whenever the Isabelle distribution is moved later.

Compiling logics

----------------

The Isabelle.tar.gz archive already contains all Isabelle sources (and

documentation). Precompiled object-logics are provided for

convenience.

Assuming proper configuration of the underlying ML system

(cf. Isabelle's etc/settings), further object-logics may be compiled

like this:

  [ISABELLE_HOME]/build FOL

Special object-logic targets may be specified as follows:

  [ISABELLE_HOME]/build -m HOL-Complex HOL

2) User installation

--------------------

Running the Isabelle binaries

-----------------------------

Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)

directly from their location within the distribution directory

[ISABELLE_HOME] like this:

  [ISABELLE_HOME]/bin/isabelle HOL

This starts an interactive Isabelle session within the current text

terminal.  [ISABELLE_HOME]/bin may be put into the shell's search

PATH.  An alternative is to create global references to the Isabelle

executables as follows:

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

Note that the site-wide Isabelle installation may already provide

Isabelle executables in some global bin directory (such as

/usr/local/bin).

Isabelle as KDE application

---------------------------

Users may install an Isabelle application icon on the KDE desktop as

follows:

  [ISABELLE_HOME]/bin/isatool install -k 1

This will install the KDE icon in ~/.kde 

  [ISABELLE_HOME]/bin/isatool install -k 2

does the same, but in ~/.kde2

Clicking on Isabelle will invoke the interface wrapper script (capital

Isabelle), which is usually configured to run Proof General (cf. the

ISABELLE_INTERFACE setting).  Additional options may be passed to

Isabelle by editing the application's command line using the standard

KDE properties editing facilities.

$Id$