INSTALL
author wenzelm
Wed Sep 20 14:59:19 2000 +0200 (2000-09-20)
changeset 10038 839340b78fc8
parent 10029 b889474af53f
child 10081 352412857003
permissions -rw-r--r--
tuned rpm command lines;
     1 
     2 Isabelle installation and compilation notes
     3 ===========================================
     4 
     5 1) User installation
     6 --------------------
     7 
     8 Here we assume that Isabelle has already been installed at your site.
     9 Otherwise see 2) below of how to get the Isabelle system installed in
    10 the first place.
    11 
    12 
    13 1a) Running the Isabelle binaries
    14 ---------------------------------
    15 
    16 The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
    17 directly from their location within the distribution directory
    18 [ISABELLE_HOME] like this:
    19 
    20   [ISABELLE_HOME]/bin/isabelle HOL
    21 
    22 This starts an interactive Isabelle session within your current text
    23 terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
    24 search PATH, but this is not strictly necessary.
    25 
    26 
    27 Please do *not* copy (or link) the Isabelle scripts anywhere else ---
    28 they just won't work!  If you really want to install independent
    29 Isabelle binaries somewhere else then do it like this:
    30 
    31   [ISABELLE_HOME]/bin/isatool install -p ~/bin
    32 
    33 Your site-wide Isabelle installation may already provide Isabelle
    34 executables in some global bin directory (such as /usr/bin).
    35 
    36 
    37 1b) Isabelle as KDE application
    38 -------------------------------
    39 
    40 Isabelle may be installed as application icon on the KDE desktop like
    41 this:
    42 
    43   [ISABELLE_HOME]/bin/isatool install -k
    44 
    45 You may have to refresh the KDE desktop in order to see the new icon.
    46 Clicking on Isabelle will invoke the interface wrapper script (capital
    47 Isabelle), which is usually configured to run Proof General (see also
    48 the ISABELLE_INTERFACE setting).  Additional options may be passed to
    49 Isabelle by editing the application's command line using the standard
    50 KDE desktop functionality.
    51 
    52 
    53 2) System installation
    54 ----------------------
    55 
    56 The Isabelle distribution is available both as traditional source-only
    57 tar.gz archives, and as binary packages (currently only RPM for
    58 Linux/x86).  In any case, the resulting Isabelle installation always
    59 contains the full sources, thus any part of the system be recompiled
    60 later, too.
    61 
    62 
    63 2a) Binary installation
    64 ----------------------
    65 
    66 Ready-to-go RPM packages are provided for the ML compiler and runtime
    67 system, the Isabelle sources, and some major object-logics.  These
    68 packages should work on any major Linux/x86 platform based on RPM
    69 package management.
    70 
    71 A minimal installation would work like this (executed as root):
    72 
    73   rpm -i --prefix /usr/share polyml.i386.rpm
    74   rpm -i --prefix /usr/share isabelle.rpm
    75   rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
    76 
    77 Note that installed RPMs may be removed like this:
    78 
    79   rpm -e isabelle-HOL isabelle polyml
    80 
    81 The install prefix given above may be changed.  By default the ML
    82 system (and other contributed packages) are expected in either of the
    83 following three locations:
    84 
    85   1) [ISABELLE_HOME]/contrib
    86   2) [ISABELLE_HOME]/..
    87   3) /usr/share
    88   4) /usr/local
    89 
    90 This may be changed further by editing [ISABELLE_HOME]/etc/settings
    91 manually.
    92 
    93 Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    94 Isabelle as platform independent sources.  Precompiled object-logics
    95 are provided for convenience.
    96 
    97 
    98 Recompiling logics
    99 ------------------
   100 
   101 Some people prefer to be able to reconstruct the full system from the
   102 sources, rather than installing precompiled packages blindly.  We do
   103 not provide source RPMs, yet any parts of Isabelle may be recompiled
   104 after installation of the main isabelle.rpm package (which contains
   105 only sources anyway).
   106 
   107 Assuming proper configuration of the underlying ML system, Isabelle
   108 object-logics may be recompiled like this:
   109 
   110   [ISABELLE_HOME]/build HOL FOL
   111 
   112 
   113 Source installation
   114 -------------------
   115 
   116 Traditional tar.gz archives are provided for the full Isabelle sources
   117 and documentation as well.  Make sure your ML system (e.g. Poly/ML
   118 etc.) has already been installed properly; then proceed as follows.
   119 
   120 * Unpacking the archives.  After unpacking the Isabelle distribution
   121 archives (using tar and gzip) you are left with some directory
   122 IsabelleYY-X.
   123 
   124 * Auto configuration.  There are some minor adaptions to be made of
   125 the Isabelle distribution to your system environment (locations of
   126 bash and perl).  Simply do it like this:
   127 
   128   cd [ISABELLE_HOME]
   129   ./configure
   130 
   131 Note that this does not store any references to [ISABELLE_HOME].  You
   132 may safely move the system later, without having to run ./configure
   133 again.
   134 
   135 * ML system settings and compilation.  Before actual compilation you
   136 have to tell Isabelle about your Standard ML system.  These settings
   137 reside in ./etc/settings, which may be also overridden by
   138 ~/isabelle/etc/settings. There are already various sample
   139 configurations in ./etc/settings commented out.
   140 
   141 To build the core Isabelle/Pure and the default object-logic, just
   142 type
   143 
   144   ./build
   145 
   146 More object-logics can be made in a similar fashion:
   147 
   148   ./build FOL HOL
   149 
   150 Explicit make targets may be given as follows:
   151 
   152   ./build -m HOL-Real HOL
   153 
   154 After successful compilation you are ready to run the system, see 1)
   155 above for more information.
   156 
   157 
   158 $Id$