INSTALL
author wenzelm
Tue Oct 16 18:34:51 2007 +0200 (2007-10-16)
changeset 25057 021fcbe2aaa5
parent 24797 3bc50959c7f0
child 28504 7ad7d7d6df47
permissions -rw-r--r--
Mark A. Hillebrand, DFKI: Robust sub/superscripts in LaTeX document output.
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_x86-linux.tar.gz
wenzelm@10081
    21
  tar -C /usr/local -xzf HOL_x86-linux.tar.gz
wenzelm@10081
    22
wenzelm@24797
    23
The install prefix given above may be changed as appropriate; there is
wenzelm@24797
    24
no need to install into a system directory like /usr/local at all.  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@17547
    30
  4) /usr/local
wenzelm@10081
    31
  3) /usr/share
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
  ./bin/isatool install -p /usr/local/bin
wenzelm@10081
    40
wenzelm@10081
    41
The install utility creates global references to the present Isabelle
wenzelm@10081
    42
installation, enabling users to invoke the Isabelle executables
wenzelm@10081
    43
without explicit path names.  Incidently, this is the only place where
wenzelm@10081
    44
a static reference to [ISABELLE_HOME] is created; thus isatool install
wenzelm@10081
    45
has to be run again whenever the Isabelle distribution is moved later.
wenzelm@10081
    46
wenzelm@10081
    47
wenzelm@10081
    48
Compiling logics
wenzelm@10081
    49
----------------
wenzelm@10081
    50
wenzelm@10081
    51
The Isabelle.tar.gz archive already contains all Isabelle sources (and
wenzelm@17547
    52
documentation).  Precompiled object-logics are provided for
wenzelm@10081
    53
convenience.
wenzelm@10081
    54
wenzelm@10081
    55
Assuming proper configuration of the underlying ML system
wenzelm@10081
    56
(cf. Isabelle's etc/settings), further object-logics may be compiled
wenzelm@10081
    57
like this:
wenzelm@10081
    58
wenzelm@10081
    59
  [ISABELLE_HOME]/build FOL
wenzelm@10081
    60
wenzelm@10081
    61
Special object-logic targets may be specified as follows:
wenzelm@10081
    62
wenzelm@17547
    63
  [ISABELLE_HOME]/build -m HOL-Algebra HOL
wenzelm@10081
    64
wenzelm@10081
    65
wenzelm@10081
    66
2) User installation
wenzelm@8809
    67
--------------------
wenzelm@8809
    68
wenzelm@10081
    69
Running the Isabelle binaries
wenzelm@10081
    70
-----------------------------
wenzelm@8809
    71
wenzelm@10081
    72
Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
wenzelm@8809
    73
directly from their location within the distribution directory
wenzelm@8809
    74
[ISABELLE_HOME] like this:
wenzelm@8809
    75
wenzelm@8809
    76
  [ISABELLE_HOME]/bin/isabelle HOL
wenzelm@8809
    77
wenzelm@10081
    78
This starts an interactive Isabelle session within the current text
wenzelm@10081
    79
terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
wenzelm@10081
    80
PATH.  An alternative is to create global references to the Isabelle
wenzelm@10081
    81
executables as follows:
wenzelm@8809
    82
wenzelm@8809
    83
  [ISABELLE_HOME]/bin/isatool install -p ~/bin
wenzelm@2759
    84
wenzelm@10081
    85
Note that the site-wide Isabelle installation may already provide
wenzelm@10081
    86
Isabelle executables in some global bin directory (such as
wenzelm@10081
    87
/usr/local/bin).
wenzelm@8809
    88
wenzelm@8809
    89
wenzelm@2759
    90
$Id$