INSTALL
changeset 2759 79def3619417
child 2772 263c0c212dfe
equal deleted inserted replaced
2758:f433eb78b927 2759:79def3619417
       
     1 
       
     2 ***************************************************************************
       
     3 
       
     4 IMPORTANT NOTE: This file describes the *new* installation procedure
       
     5 using various scripts that are still supposed beta for Isabelle94-8.
       
     6 If you encounter any problems, you may want to try compiling Isabelle
       
     7 the olden way as described in README.
       
     8 
       
     9 ***************************************************************************
       
    10 
       
    11 
       
    12 Isabelle installation notes
       
    13 ===========================
       
    14 
       
    15 1. Unpacking
       
    16 ------------
       
    17 
       
    18 Unpacking the Isabelle distribution archive (using tar and gzip)
       
    19 leaves you with some directory IsabelleYY-X. You may install this
       
    20 anywhere, but please just *not* as ~/isabelle!
       
    21 
       
    22 The place where you put the contents of IsabelleYY-X will be referred
       
    23 to as [ISABELLE_HOME] subsequently.
       
    24 
       
    25 
       
    26 2. Auto configuration
       
    27 ---------------------
       
    28 
       
    29 There are some minor adaptions to be made of the Isabelle distribution
       
    30 to your system environment. Simply type:
       
    31 
       
    32   cd [ISABELLE_HOME]
       
    33   ./configure
       
    34 
       
    35 
       
    36 3. ML system settings and compilation
       
    37 -------------------------------------
       
    38 
       
    39 Before actual compilation you have to tell Isabelle about your
       
    40 Standard ML system.  These settings reside in ./etc/settings, which
       
    41 may be also overridden by ~/isabelle/etc/settings. There are already
       
    42 various sample configurations in ./etc/settings commented out.
       
    43 
       
    44 To build the core Isabelle/Pure, now just type:
       
    45 
       
    46   ./build
       
    47 
       
    48 Objects logics can be made similarly, e.g.:
       
    49 
       
    50   ./build FOL HOL
       
    51 
       
    52 
       
    53 4. Running the system
       
    54 ---------------------
       
    55 
       
    56 Provided that compilation was succesful, you can now run something
       
    57 like:
       
    58 
       
    59   [ISABELLE_HOME]/bin/isabelle FOL
       
    60 
       
    61 to start and interactive Isabelle session within your current
       
    62 terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
       
    63 PATH. Please do *not* copy (or link) the Isabelle scripts somewhere
       
    64 else -- or they just won't work!
       
    65 
       
    66 Other users may directly run your Isabelle installation without
       
    67 additional configuration, provided that no globally required settings
       
    68 reside in your ~/isabelle/etc/settings.
       
    69 
       
    70 
       
    71 $Id$