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