author berghofe
Mon, 19 Jul 1999 17:21:40 +0200
changeset 7047 d103b875ef1d
parent 6486 1f1d5e00e0a5
child 8809 85539b33be03
permissions -rw-r--r--
Datatype package now handles arbitrarily branching datatypes.

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:


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


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