INSTALL
changeset 2759 79def3619417
child 2772 263c0c212dfe
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/INSTALL	Fri Mar 07 14:49:56 1997 +0100
     1.3 @@ -0,0 +1,71 @@
     1.4 +
     1.5 +***************************************************************************
     1.6 +
     1.7 +IMPORTANT NOTE: This file describes the *new* installation procedure
     1.8 +using various scripts that are still supposed beta for Isabelle94-8.
     1.9 +If you encounter any problems, you may want to try compiling Isabelle
    1.10 +the olden way as described in README.
    1.11 +
    1.12 +***************************************************************************
    1.13 +
    1.14 +
    1.15 +Isabelle installation notes
    1.16 +===========================
    1.17 +
    1.18 +1. Unpacking
    1.19 +------------
    1.20 +
    1.21 +Unpacking the Isabelle distribution archive (using tar and gzip)
    1.22 +leaves you with some directory IsabelleYY-X. You may install this
    1.23 +anywhere, but please just *not* as ~/isabelle!
    1.24 +
    1.25 +The place where you put the contents of IsabelleYY-X will be referred
    1.26 +to as [ISABELLE_HOME] subsequently.
    1.27 +
    1.28 +
    1.29 +2. Auto configuration
    1.30 +---------------------
    1.31 +
    1.32 +There are some minor adaptions to be made of the Isabelle distribution
    1.33 +to your system environment. Simply type:
    1.34 +
    1.35 +  cd [ISABELLE_HOME]
    1.36 +  ./configure
    1.37 +
    1.38 +
    1.39 +3. ML system settings and compilation
    1.40 +-------------------------------------
    1.41 +
    1.42 +Before actual compilation you have to tell Isabelle about your
    1.43 +Standard ML system.  These settings reside in ./etc/settings, which
    1.44 +may be also overridden by ~/isabelle/etc/settings. There are already
    1.45 +various sample configurations in ./etc/settings commented out.
    1.46 +
    1.47 +To build the core Isabelle/Pure, now just type:
    1.48 +
    1.49 +  ./build
    1.50 +
    1.51 +Objects logics can be made similarly, e.g.:
    1.52 +
    1.53 +  ./build FOL HOL
    1.54 +
    1.55 +
    1.56 +4. Running the system
    1.57 +---------------------
    1.58 +
    1.59 +Provided that compilation was succesful, you can now run something
    1.60 +like:
    1.61 +
    1.62 +  [ISABELLE_HOME]/bin/isabelle FOL
    1.63 +
    1.64 +to start and interactive Isabelle session within your current
    1.65 +terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
    1.66 +PATH. Please do *not* copy (or link) the Isabelle scripts somewhere
    1.67 +else -- or they just won't work!
    1.68 +
    1.69 +Other users may directly run your Isabelle installation without
    1.70 +additional configuration, provided that no globally required settings
    1.71 +reside in your ~/isabelle/etc/settings.
    1.72 +
    1.73 +
    1.74 +$Id$