INSTALL
author wenzelm
Mon Feb 08 15:55:35 1999 +0100 (1999-02-08)
changeset 6258 1f85c03fb3df
parent 5396 cfc1fe0b8490
child 6345 f4a3c3bb3e38
permissions -rw-r--r--
no deps on compile time sources;
wenzelm@2759
     1
wenzelm@2759
     2
Isabelle installation notes
wenzelm@2759
     3
===========================
wenzelm@2759
     4
wenzelm@3263
     5
Unpacking the archive
wenzelm@3263
     6
---------------------
wenzelm@2759
     7
wenzelm@3263
     8
After unpacking the Isabelle distribution archive (using tar and gzip)
wenzelm@3263
     9
you are left with some directory IsabelleYY-X. You may install this
wenzelm@3117
    10
anywhere, but please just *not* as ~/isabelle!!!
wenzelm@2759
    11
wenzelm@2759
    12
The place where you put the contents of IsabelleYY-X will be referred
wenzelm@2759
    13
to as [ISABELLE_HOME] subsequently.
wenzelm@2759
    14
wenzelm@2759
    15
wenzelm@3263
    16
Auto configuration
wenzelm@3263
    17
------------------
wenzelm@2759
    18
wenzelm@2759
    19
There are some minor adaptions to be made of the Isabelle distribution
wenzelm@2759
    20
to your system environment. Simply type:
wenzelm@2759
    21
wenzelm@2759
    22
  cd [ISABELLE_HOME]
wenzelm@2759
    23
  ./configure
wenzelm@2759
    24
wenzelm@6258
    25
This does not store any references to [ISABELLE_HOME]. You may safely
wenzelm@6258
    26
move the system later, without running ./configure again.
wenzelm@6258
    27
wenzelm@2759
    28
wenzelm@3263
    29
ML system settings and compilation
wenzelm@3263
    30
----------------------------------
wenzelm@2759
    31
wenzelm@2759
    32
Before actual compilation you have to tell Isabelle about your
wenzelm@2759
    33
Standard ML system.  These settings reside in ./etc/settings, which
wenzelm@2759
    34
may be also overridden by ~/isabelle/etc/settings. There are already
wenzelm@2759
    35
various sample configurations in ./etc/settings commented out.
wenzelm@2759
    36
wenzelm@3117
    37
To build the core Isabelle/Pure and the default object-logic, just
wenzelm@3117
    38
type:
wenzelm@2759
    39
wenzelm@2759
    40
  ./build
wenzelm@2759
    41
wenzelm@3117
    42
More object-logics can be made similarly:
wenzelm@2759
    43
wenzelm@2759
    44
  ./build FOL HOL
wenzelm@2759
    45
wenzelm@2759
    46
wenzelm@3263
    47
Running the system
wenzelm@3263
    48
------------------
wenzelm@2759
    49
wenzelm@3263
    50
Provided that compilation was successful, you can now run something
wenzelm@2759
    51
like:
wenzelm@2759
    52
wenzelm@2759
    53
  [ISABELLE_HOME]/bin/isabelle FOL
wenzelm@2759
    54
wenzelm@3263
    55
This starts an interactive Isabelle session within your current text
wenzelm@2759
    56
terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
wenzelm@5395
    57
search PATH.
wenzelm@5395
    58
wenzelm@5395
    59
Please do *not* copy (or link) the Isabelle scripts anywhere else --
wenzelm@5395
    60
or they just won't work!  If you really feel the urge to install
wenzelm@5396
    61
independent Isabelle binaries somewhere you should rather do it like
wenzelm@5396
    62
this:
wenzelm@5396
    63
wenzelm@5396
    64
  [ISABELLE_HOME]/bin/isatool install /usr/local/bin
wenzelm@5396
    65
wenzelm@2759
    66
wenzelm@2759
    67
wenzelm@2759
    68
$Id$