INSTALL
author wenzelm
Tue, 27 May 1997 14:38:49 +0200
changeset 3360 85a7eede097e
parent 3322 bc4d107fb6dd
child 4260 f6bdfbd0e1c3
permissions -rw-r--r--
added 1.09.28 note;


***************************************************************************

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:

  cd [ISABELLE_HOME]
  ./configure


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


$Id$