INSTALL
author wenzelm
Tue Sep 19 23:50:43 2000 +0200 (2000-09-19)
changeset 10029 b889474af53f
parent 9927 7a9652294fe0
child 10038 839340b78fc8
permissions -rw-r--r--
updated;
     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 --force --prefix /usr/share polyml.i386.rpm
    74   rpm -i --force --prefix /usr/share isabelle.rpm
    75   rpm -i --force --prefix /usr/share isabelle-HOL.i386.rpm
    76 
    77 The install prefix may be changed as indicated.  By default the ML
    78 system (and other contributed packages) are expected in either of the
    79 following three locations:
    80 
    81   1) [ISABELLE_HOME]/contrib
    82   2) [ISABELLE_HOME]/..
    83   3) /usr/share
    84   4) /usr/local
    85 
    86 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
    87 
    88 Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    89 Isabelle as platform independent sources.  Precompiled object-logics
    90 are provided for convenience.
    91 
    92 
    93 Recompiling logics
    94 ------------------
    95 
    96 Some people prefer to be able to reconstruct the full system from the
    97 sources, rather than installing precompiled packages blindly.  We do
    98 not provide source RPMs, yet any parts of Isabelle may be recompiled
    99 after installation of the main isabelle.rpm package (which contains
   100 only sources anyway).
   101 
   102 Assuming proper configuration of the underlying ML system, Isabelle
   103 object-logics may be recompiled like this:
   104 
   105   [ISABELLE_HOME]/build HOL FOL
   106 
   107 
   108 Source installation
   109 -------------------
   110 
   111 Traditional tar.gz archives are provided for the full Isabelle sources
   112 and documentation as well.  Make sure your ML system (e.g. Poly/ML
   113 etc.) has already been installed properly; then proceed as follows.
   114 
   115 * Unpacking the archives.  After unpacking the Isabelle distribution
   116 archives (using tar and gzip) you are left with some directory
   117 IsabelleYY-X.
   118 
   119 * Auto configuration.  There are some minor adaptions to be made of
   120 the Isabelle distribution to your system environment (locations of
   121 bash and perl).  Simply do it like this:
   122 
   123   cd [ISABELLE_HOME]
   124   ./configure
   125 
   126 Note that this does not store any references to [ISABELLE_HOME].  You
   127 may safely move the system later, without having to run ./configure
   128 again.
   129 
   130 * ML system settings and compilation.  Before actual compilation you
   131 have to tell Isabelle about your Standard ML system.  These settings
   132 reside in ./etc/settings, which may be also overridden by
   133 ~/isabelle/etc/settings. There are already various sample
   134 configurations in ./etc/settings commented out.
   135 
   136 To build the core Isabelle/Pure and the default object-logic, just
   137 type
   138 
   139   ./build
   140 
   141 More object-logics can be made in a similar fashion:
   142 
   143   ./build FOL HOL
   144 
   145 Explicit make targets may be given as follows:
   146 
   147   ./build -m HOL-Real HOL
   148 
   149 After successful compilation you are ready to run the system, see 1)
   150 above for more information.
   151 
   152 
   153 $Id$