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-Real 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 2 desktop as
follows (version 1 may be specified as well):
[ISABELLE_HOME]/bin/isatool install -k 2
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$