author wenzelm
Fri, 23 May 1997 18:55:28 +0200
changeset 3322 bc4d107fb6dd
parent 3263 124bb367dc0e
child 4260 f6bdfbd0e1c3
permissions -rw-r--r--


IMPORTANT NOTE: This file describes the *new* installation procedure
using various scripts that are still supposed beta for Isabelle94-8.
If you encounter serious problems, you may want to consider compiling
Isabelle the olden way, as described in README.old.


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


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


More object-logics can be made similarly:

  ./build FOL HOL

Running the system

Provided that compilation was successful, you can now run something

  [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
somewhere else -- or they just won't work!