Isabelle compilation and installation notes

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

Unpacking the archive

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

After unpacking the Isabelle distribution archive (using tar and gzip)

you are left with some directory IsabelleYY-X. You may install this

anywhere, but please just *not* as ~/isabelle!!!

The place where you put the contents of IsabelleYY-X will be referred

to as [ISABELLE_HOME] subsequently.

Auto configuration

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

There are some minor adaptions to be made of the Isabelle distribution

to your system environment. Simply type:

  cd [ISABELLE_HOME]

  ./configure

This does not store any references to [ISABELLE_HOME]. You may safely

move the system later, without running ./configure again.

ML system settings and compilation

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

Before actual compilation you have to tell Isabelle about your

Standard ML system.  These settings reside in ./etc/settings, which

may be also overridden by ~/isabelle/etc/settings. There are already

various sample configurations in ./etc/settings commented out.

To build the core Isabelle/Pure and the default object-logic, just

type:

  ./build

More object-logics can be made similarly:

  ./build FOL HOL

Running the system

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

Provided that compilation was successful, you can now run something

like:

  [ISABELLE_HOME]/bin/isabelle FOL

This starts an interactive Isabelle session within your current text

terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's

search PATH.

Please do *not* copy (or link) the Isabelle scripts anywhere else, or

they just won't work!  If you really feel the urge to install

independent Isabelle binaries anywhere else do it like this:

  [ISABELLE_HOME]/bin/isatool install -p /usr/local/bin

$Id$