INSTALL

added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),
replaced unspecific 'error' invocations with raising of specific SMT exceptions,
added annotations to traced SMT problem and solver output

Isabelle installation notes
===========================

1) System installation
----------------------

The Isabelle distribution includes both complete sources and
precompiled binary packages for common Unix-like 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_x86-linux.tar.gz
  tar -C /usr/local -xzf HOL_x86-linux.tar.gz

The install prefix given above may be changed as appropriate; there is
no need to install into a system directory like /usr/local at all.  By
default the ML system (and other contributed packages) are expected in
any of the following locations:

  1) [ISABELLE_HOME]/contrib
  2) [ISABELLE_HOME]/..
  4) /usr/local
  3) /usr/share
  5) /opt

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

The installation may be finished as follows:

  cd [ISABELLE_HOME]
  ./bin/isabelle 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.  This is the only place where a static
reference to [ISABELLE_HOME] is created; thus isabelle 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-Algebra HOL


2) User installation
--------------------

Running the Isabelle binaries
-----------------------------

Users may invoke the main Isabelle binaries (isabelle and
isabelle-process) directly from their location within the distribution
directory [ISABELLE_HOME] like this:

  [ISABELLE_HOME]/bin/isabelle tty -l 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/isabelle 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).