author obua
Tue, 13 Sep 2005 17:05:59 +0200
changeset 17335 7cff05c90a0e
parent 16653 c12c2f411f77
child 17547 b0d70cf4ed18
permissions -rw-r--r--
fixed INST: has same semantic now as INST_TYPE for repetitions

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

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