INSTALL
author wenzelm
Fri Mar 08 16:24:06 2002 +0100 (2002-03-08)
changeset 13049 ce180e5b7fa0
parent 11126 b98336d6e834
child 14009 0d648f24bab4
permissions -rw-r--r--
tuned;
wenzelm@2759
     1
wenzelm@10081
     2
Isabelle installation notes
wenzelm@10081
     3
===========================
wenzelm@10081
     4
wenzelm@10081
     5
1) System installation
wenzelm@10081
     6
----------------------
wenzelm@10081
     7
wenzelm@10081
     8
The Isabelle distribution includes both complete sources and
wenzelm@10081
     9
precompiled binary packages for common Unix platforms.
wenzelm@10081
    10
wenzelm@10081
    11
wenzelm@10081
    12
Quick installation
wenzelm@10081
    13
------------------
wenzelm@10081
    14
wenzelm@10081
    15
Ready-to-go packages are provided for the ML compiler and runtime
wenzelm@10081
    16
system, the Isabelle sources, and some major object-logics.  A minimal
wenzelm@10081
    17
site installation of Isabelle on Linux/x86 works like this:
wenzelm@10081
    18
wenzelm@10081
    19
  tar -C /usr/local -xzf Isabelle.tar.gz
wenzelm@10081
    20
  tar -C /usr/local -xzf polyml_base.tar.gz
wenzelm@10081
    21
  tar -C /usr/local -xzf polyml_x86-linux.tar.gz
wenzelm@10081
    22
  tar -C /usr/local -xzf HOL_x86-linux.tar.gz
wenzelm@10081
    23
wenzelm@10081
    24
The install prefix given above may be changed as appropriate.  By
wenzelm@10081
    25
default the ML system (and other contributed packages) are expected in
wenzelm@10081
    26
any of the following locations:
wenzelm@10081
    27
wenzelm@10081
    28
  1) [ISABELLE_HOME]/contrib
wenzelm@10081
    29
  2) [ISABELLE_HOME]/..
wenzelm@10081
    30
  3) /usr/share
wenzelm@10081
    31
  4) /usr/local
wenzelm@10081
    32
  5) /opt
wenzelm@10081
    33
wenzelm@10081
    34
This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
wenzelm@2759
    35
wenzelm@10081
    36
The installation may be finished as follows:
wenzelm@10081
    37
wenzelm@10081
    38
  cd [ISABELLE_HOME]
wenzelm@10081
    39
  ./configure
wenzelm@10081
    40
  ./bin/isatool install -p /usr/local/bin
wenzelm@10081
    41
wenzelm@10081
    42
Note that the configure script is only required for systems that do
wenzelm@10081
    43
not have bash and perl in the canonical places (/bin/bash and
wenzelm@10081
    44
/usr/bin/perl).
wenzelm@10081
    45
wenzelm@10081
    46
The install utility creates global references to the present Isabelle
wenzelm@10081
    47
installation, enabling users to invoke the Isabelle executables
wenzelm@10081
    48
without explicit path names.  Incidently, this is the only place where
wenzelm@10081
    49
a static reference to [ISABELLE_HOME] is created; thus isatool install
wenzelm@10081
    50
has to be run again whenever the Isabelle distribution is moved later.
wenzelm@10081
    51
wenzelm@10081
    52
wenzelm@10081
    53
Compiling logics
wenzelm@10081
    54
----------------
wenzelm@10081
    55
wenzelm@10081
    56
The Isabelle.tar.gz archive already contains all Isabelle sources (and
wenzelm@10081
    57
documentation). Precompiled object-logics are provided for
wenzelm@10081
    58
convenience.
wenzelm@10081
    59
wenzelm@10081
    60
Assuming proper configuration of the underlying ML system
wenzelm@10081
    61
(cf. Isabelle's etc/settings), further object-logics may be compiled
wenzelm@10081
    62
like this:
wenzelm@10081
    63
wenzelm@10081
    64
  [ISABELLE_HOME]/build FOL
wenzelm@10081
    65
wenzelm@10081
    66
Special object-logic targets may be specified as follows:
wenzelm@10081
    67
wenzelm@10081
    68
  [ISABELLE_HOME]/build -m HOL-Real HOL
wenzelm@10081
    69
wenzelm@10081
    70
wenzelm@10081
    71
2) User installation
wenzelm@8809
    72
--------------------
wenzelm@8809
    73
wenzelm@10081
    74
Running the Isabelle binaries
wenzelm@10081
    75
-----------------------------
wenzelm@8809
    76
wenzelm@10081
    77
Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
wenzelm@8809
    78
directly from their location within the distribution directory
wenzelm@8809
    79
[ISABELLE_HOME] like this:
wenzelm@8809
    80
wenzelm@8809
    81
  [ISABELLE_HOME]/bin/isabelle HOL
wenzelm@8809
    82
wenzelm@10081
    83
This starts an interactive Isabelle session within the current text
wenzelm@10081
    84
terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
wenzelm@10081
    85
PATH.  An alternative is to create global references to the Isabelle
wenzelm@10081
    86
executables as follows:
wenzelm@8809
    87
wenzelm@8809
    88
  [ISABELLE_HOME]/bin/isatool install -p ~/bin
wenzelm@2759
    89
wenzelm@10081
    90
Note that the site-wide Isabelle installation may already provide
wenzelm@10081
    91
Isabelle executables in some global bin directory (such as
wenzelm@10081
    92
/usr/local/bin).
wenzelm@8809
    93
wenzelm@8809
    94
wenzelm@10081
    95
Isabelle as KDE application
wenzelm@10081
    96
---------------------------
wenzelm@8809
    97
wenzelm@11126
    98
Users may install an Isabelle application icon on the KDE 2 desktop as
wenzelm@11126
    99
follows (version 1 may be specified as well):
wenzelm@8809
   100
wenzelm@11126
   101
  [ISABELLE_HOME]/bin/isatool install -k 2
wenzelm@2759
   102
wenzelm@10029
   103
Clicking on Isabelle will invoke the interface wrapper script (capital
wenzelm@10081
   104
Isabelle), which is usually configured to run Proof General (cf. the
wenzelm@10081
   105
ISABELLE_INTERFACE setting).  Additional options may be passed to
wenzelm@10029
   106
Isabelle by editing the application's command line using the standard
wenzelm@10081
   107
KDE properties editing facilities.
wenzelm@2759
   108
wenzelm@2759
   109
wenzelm@2759
   110
$Id$