author webertj
Tue, 15 Jun 2004 00:06:40 +0200
changeset 14942 78ddcbebace1
parent 14024 213dcc39358f
child 16476 baa008d0fee9
permissions -rw-r--r--
entries for ZChaff and BerkMin added/modified

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
  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:

  ./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

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

Assuming proper configuration of the underlying ML system
(cf. Isabelle's etc/settings), further object-logics may be compiled
like this:


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

Isabelle as KDE application

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

  [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.