INSTALL
author berghofe
Wed, 24 Nov 2004 10:37:38 +0100
changeset 15326 ff21cddee442
parent 14024 213dcc39358f
child 16476 baa008d0fee9
permissions -rw-r--r--
Made test_term escape special characters in strings that caused the ML compiler to fail.
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_base.tar.gz
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    21
  tar -C /usr/local -xzf polyml_x86-linux.tar.gz
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    22
  tar -C /usr/local -xzf HOL_x86-linux.tar.gz
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    23
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    24
The install prefix given above may be changed as appropriate.  By
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]/..
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    30
  3) /usr/share
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    31
  4) /usr/local
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]
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    39
  ./configure
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    40
  ./bin/isatool install -p /usr/local/bin
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    41
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    42
Note that the configure script is only required for systems that do
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    43
not have bash and perl in the canonical places (/bin/bash and
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    44
/usr/bin/perl).
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    45
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    46
The install utility creates global references to the present Isabelle
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    47
installation, enabling users to invoke the Isabelle executables
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    48
without explicit path names.  Incidently, this is the only place where
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    49
a static reference to [ISABELLE_HOME] is created; thus isatool install
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    50
has to be run again whenever the Isabelle distribution is moved later.
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    51
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    52
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    53
Compiling logics
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    54
----------------
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    55
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    56
The Isabelle.tar.gz archive already contains all Isabelle sources (and
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    57
documentation). Precompiled object-logics are provided for
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    58
convenience.
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    59
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    60
Assuming proper configuration of the underlying ML system
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    61
(cf. Isabelle's etc/settings), further object-logics may be compiled
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    62
like this:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    63
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    64
  [ISABELLE_HOME]/build FOL
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    65
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    66
Special object-logic targets may be specified as follows:
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    67
14024
213dcc39358f HOL-Real -> HOL-Complex
kleing
parents: 14009
diff changeset
    68
  [ISABELLE_HOME]/build -m HOL-Complex HOL
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    69
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    70
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    71
2) User installation
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    72
--------------------
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    73
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    74
Running the Isabelle binaries
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    75
-----------------------------
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    76
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    77
Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    78
directly from their location within the distribution directory
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    79
[ISABELLE_HOME] like this:
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    80
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    81
  [ISABELLE_HOME]/bin/isabelle HOL
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    82
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    83
This starts an interactive Isabelle session within the current text
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    84
terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    85
PATH.  An alternative is to create global references to the Isabelle
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    86
executables as follows:
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    87
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    88
  [ISABELLE_HOME]/bin/isatool install -p ~/bin
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
    89
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    90
Note that the site-wide Isabelle installation may already provide
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    91
Isabelle executables in some global bin directory (such as
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    92
/usr/local/bin).
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    93
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    94
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    95
Isabelle as KDE application
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
    96
---------------------------
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
    97
14009
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
    98
Users may install an Isabelle application icon on the KDE desktop as
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
    99
follows:
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
   100
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
   101
  [ISABELLE_HOME]/bin/isatool install -k 1
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
   102
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
   103
This will install the KDE icon in ~/.kde 
8809
85539b33be03 updated;
wenzelm
parents: 6486
diff changeset
   104
11126
b98336d6e834 isatool install -k;
wenzelm
parents: 10081
diff changeset
   105
  [ISABELLE_HOME]/bin/isatool install -k 2
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
   106
14009
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
   107
does the same, but in ~/.kde2
0d648f24bab4 removed references to KDE versions (works for any).
kleing
parents: 11126
diff changeset
   108
10029
b889474af53f updated;
wenzelm
parents: 9927
diff changeset
   109
Clicking on Isabelle will invoke the interface wrapper script (capital
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
   110
Isabelle), which is usually configured to run Proof General (cf. the
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
   111
ISABELLE_INTERFACE setting).  Additional options may be passed to
10029
b889474af53f updated;
wenzelm
parents: 9927
diff changeset
   112
Isabelle by editing the application's command line using the standard
10081
352412857003 simplified;
wenzelm
parents: 10038
diff changeset
   113
KDE properties editing facilities.
2759
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
   114
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
   115
79def3619417 Isabelle installation notes;
wenzelm
parents:
diff changeset
   116
$Id$