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