INSTALL
author obua
Wed, 28 Sep 2005 13:17:23 +0200
changeset 17694 b7870c2bd7df
parent 17547 b0d70cf4ed18
child 24797 3bc50959c7f0
permissions -rw-r--r--
mapped "-->" to "hol4-->"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
     1
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     2
Isabelle installation notes
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     3
===========================
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     4
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     5
1) System installation
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     6
----------------------
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     7
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     8
The Isabelle distribution includes both complete sources and
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
     9
precompiled binary packages for common Unix platforms.
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    10
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    11
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    12
Quick installation
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    13
------------------
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    14
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    15
Ready-to-go packages are provided for the ML compiler and runtime
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    16
system, the Isabelle sources, and some major object-logics.  A minimal
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    17
site installation of Isabelle on Linux/x86 works like this:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    18
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    19
  tar -C /usr/local -xzf Isabelle.tar.gz
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    20
  tar -C /usr/local -xzf polyml_x86-linux.tar.gz
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    21
  tar -C /usr/local -xzf HOL_x86-linux.tar.gz
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    22
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    23
The install prefix given above may be changed as appropriate.  By
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    24
default the ML system (and other contributed packages) are expected in
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    25
any of the following locations:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    26
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    27
  1) [ISABELLE_HOME]/contrib
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    28
  2) [ISABELLE_HOME]/..
17547
b0d70cf4ed18 updated for Isabelle2005;
wenzelm
parents: 16653
diff changeset
    29
  4) /usr/local
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    30
  3) /usr/share
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    31
  5) /opt
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    32
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    33
This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
    34
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    35
The installation may be finished as follows:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    36
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    37
  cd [ISABELLE_HOME]
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    38
  ./bin/isatool install -p /usr/local/bin
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    39
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    40
The install utility creates global references to the present Isabelle
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    41
installation, enabling users to invoke the Isabelle executables
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    42
without explicit path names.  Incidently, this is the only place where
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    43
a static reference to [ISABELLE_HOME] is created; thus isatool install
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    44
has to be run again whenever the Isabelle distribution is moved later.
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    45
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    46
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    47
Compiling logics
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    48
----------------
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    49
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    50
The Isabelle.tar.gz archive already contains all Isabelle sources (and
17547
b0d70cf4ed18 updated for Isabelle2005;
wenzelm
parents: 16653
diff changeset
    51
documentation).  Precompiled object-logics are provided for
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    52
convenience.
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    53
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    54
Assuming proper configuration of the underlying ML system
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    55
(cf. Isabelle's etc/settings), further object-logics may be compiled
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    56
like this:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    57
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    58
  [ISABELLE_HOME]/build FOL
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    59
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    60
Special object-logic targets may be specified as follows:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    61
17547
b0d70cf4ed18 updated for Isabelle2005;
wenzelm
parents: 16653
diff changeset
    62
  [ISABELLE_HOME]/build -m HOL-Algebra HOL
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    63
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    64
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    65
2) User installation
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    66
--------------------
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    67
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    68
Running the Isabelle binaries
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    69
-----------------------------
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    70
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    71
Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    72
directly from their location within the distribution directory
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    73
[ISABELLE_HOME] like this:
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    74
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    75
  [ISABELLE_HOME]/bin/isabelle HOL
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    76
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    77
This starts an interactive Isabelle session within the current text
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    78
terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    79
PATH.  An alternative is to create global references to the Isabelle
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    80
executables as follows:
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    81
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    82
  [ISABELLE_HOME]/bin/isatool install -p ~/bin
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
    83
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    84
Note that the site-wide Isabelle installation may already provide
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    85
Isabelle executables in some global bin directory (such as
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    86
/usr/local/bin).
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    87
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    88
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
    89
$Id$