INSTALL
author kleing
Mon May 16 09:35:05 2005 +0200 (2005-05-16)
changeset 15964 f2074e12d1d4
parent 14024 213dcc39358f
child 16476 baa008d0fee9
permissions -rw-r--r--
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
     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-Complex 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 1
   102 
   103 This will install the KDE icon in ~/.kde 
   104 
   105   [ISABELLE_HOME]/bin/isatool install -k 2
   106 
   107 does the same, but in ~/.kde2
   108 
   109 Clicking on Isabelle will invoke the interface wrapper script (capital
   110 Isabelle), which is usually configured to run Proof General (cf. the
   111 ISABELLE_INTERFACE setting).  Additional options may be passed to
   112 Isabelle by editing the application's command line using the standard
   113 KDE properties editing facilities.
   114 
   115 
   116 $Id$