INSTALL
author huffman
Wed, 04 Mar 2009 17:12:23 -0800
changeset 30273 ecd6f0ca62ea
parent 29145 b1c6f4563df7
child 30852 59a422908e29
permissions -rw-r--r--
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
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
24797
wenzelm
parents: 17547
diff changeset
    23
The install prefix given above may be changed as appropriate; there is
wenzelm
parents: 17547
diff changeset
    24
no need to install into a system directory like /usr/local at all.  By
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    25
default the ML system (and other contributed packages) are expected in
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    26
any of the following locations:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    27
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    28
  1) [ISABELLE_HOME]/contrib
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    29
  2) [ISABELLE_HOME]/..
17547
b0d70cf4ed18 updated for Isabelle2005;
wenzelm
parents: 16653
diff changeset
    30
  4) /usr/local
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    31
  3) /usr/share
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    32
  5) /opt
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    33
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    34
This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
    35
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    36
The installation may be finished as follows:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    37
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    38
  cd [ISABELLE_HOME]
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    39
  ./bin/isabelle install -p /usr/local/bin
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    40
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    41
The install utility creates global references to the present Isabelle
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    42
installation, enabling users to invoke the Isabelle executables
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    43
without explicit path names.  This is the only place where a static
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    44
reference to [ISABELLE_HOME] is created; thus isabelle install has to
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    45
be run again whenever the Isabelle distribution is moved later.
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    46
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    47
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    48
Compiling logics
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    49
----------------
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    50
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    51
The Isabelle.tar.gz archive already contains all Isabelle sources (and
17547
b0d70cf4ed18 updated for Isabelle2005;
wenzelm
parents: 16653
diff changeset
    52
documentation).  Precompiled object-logics are provided for
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    53
convenience.
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    54
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    55
Assuming proper configuration of the underlying ML system
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    56
(cf. Isabelle's etc/settings), further object-logics may be compiled
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    57
like this:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    58
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    59
  [ISABELLE_HOME]/build FOL
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    60
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    61
Special object-logic targets may be specified as follows:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    62
17547
b0d70cf4ed18 updated for Isabelle2005;
wenzelm
parents: 16653
diff changeset
    63
  [ISABELLE_HOME]/build -m HOL-Algebra HOL
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    64
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    65
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    66
2) User installation
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    67
--------------------
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    68
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    69
Running the Isabelle binaries
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    70
-----------------------------
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    71
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    72
Users may invoke the main Isabelle binaries (isabelle and
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    73
isabelle-process) directly from their location within the distribution
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    74
directory [ISABELLE_HOME] like this:
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    75
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    76
  [ISABELLE_HOME]/bin/isabelle-process HOL
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    77
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    78
This starts an interactive Isabelle session within the current text
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    79
terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    80
PATH.  An alternative is to create global references to the Isabelle
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    81
executables as follows:
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    82
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24797
diff changeset
    83
  [ISABELLE_HOME]/bin/isabelle install -p ~/bin
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
    84
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    85
Note that the site-wide Isabelle installation may already provide
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    86
Isabelle executables in some global bin directory (such as
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    87
/usr/local/bin).