INSTALL
author wenzelm
Mon Jun 20 16:41:20 2005 +0200 (2005-06-20)
changeset 16476 baa008d0fee9
parent 14024 213dcc39358f
child 16653 c12c2f411f77
permissions -rw-r--r--
./configure obsolete on virtually all systems, but apt to cause problems;
     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   ./bin/isatool install -p /usr/local/bin
    40 
    41 The install utility creates global references to the present Isabelle
    42 installation, enabling users to invoke the Isabelle executables
    43 without explicit path names.  Incidently, this is the only place where
    44 a static reference to [ISABELLE_HOME] is created; thus isatool install
    45 has to be run again whenever the Isabelle distribution is moved later.
    46 
    47 
    48 Compiling logics
    49 ----------------
    50 
    51 The Isabelle.tar.gz archive already contains all Isabelle sources (and
    52 documentation). Precompiled object-logics are provided for
    53 convenience.
    54 
    55 Assuming proper configuration of the underlying ML system
    56 (cf. Isabelle's etc/settings), further object-logics may be compiled
    57 like this:
    58 
    59   [ISABELLE_HOME]/build FOL
    60 
    61 Special object-logic targets may be specified as follows:
    62 
    63   [ISABELLE_HOME]/build -m HOL-Complex HOL
    64 
    65 
    66 2) User installation
    67 --------------------
    68 
    69 Running the Isabelle binaries
    70 -----------------------------
    71 
    72 Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
    73 directly from their location within the distribution directory
    74 [ISABELLE_HOME] like this:
    75 
    76   [ISABELLE_HOME]/bin/isabelle HOL
    77 
    78 This starts an interactive Isabelle session within the current text
    79 terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
    80 PATH.  An alternative is to create global references to the Isabelle
    81 executables as follows:
    82 
    83   [ISABELLE_HOME]/bin/isatool install -p ~/bin
    84 
    85 Note that the site-wide Isabelle installation may already provide
    86 Isabelle executables in some global bin directory (such as
    87 /usr/local/bin).
    88 
    89 
    90 Isabelle as KDE application
    91 ---------------------------
    92 
    93 Users may install an Isabelle application icon on the KDE desktop as
    94 follows:
    95 
    96   [ISABELLE_HOME]/bin/isatool install -k 1
    97 
    98 This will install the KDE icon in ~/.kde 
    99 
   100   [ISABELLE_HOME]/bin/isatool install -k 2
   101 
   102 does the same, but in ~/.kde2
   103 
   104 Clicking on Isabelle will invoke the interface wrapper script (capital
   105 Isabelle), which is usually configured to run Proof General (cf. the
   106 ISABELLE_INTERFACE setting).  Additional options may be passed to
   107 Isabelle by editing the application's command line using the standard
   108 KDE properties editing facilities.
   109 
   110 
   111 $Id$