INSTALL
author wenzelm
Mon Sep 11 20:41:44 2000 +0200 (2000-09-11)
changeset 9927 7a9652294fe0
parent 8809 85539b33be03
child 10029 b889474af53f
permissions -rw-r--r--
tuned;
     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 Clicking on that icon will invoke the interface wrapper script
    46 (capital Isabelle), which may be configured to run your favorite
    47 Isabelle user interface via the ISABELLE_INTERFACE setting.
    48 Additional options may be passed by editing the application's command
    49 line (by using the standard KDE desktop functionality).
    50 
    51 
    52 2) System installation
    53 ----------------------
    54 
    55 The Isabelle distribution is available both as traditional source-only
    56 tar.gz archives, and as binary packages (currently only RPM for
    57 Linux/x86).  In any case, the resulting Isabelle installation always
    58 contains the full sources, thus any part of the system be recompiled
    59 later, too.
    60 
    61 
    62 2a) Binary installation
    63 ----------------------
    64 
    65 Ready-to-go RPM packages are provided for the ML compiler and runtime
    66 system, the Isabelle sources, and some major object-logics.  These
    67 packages should work on any major RPM-based Linux/x86 platform (such
    68 as SuSE, RedHat etc.).  A typical installation procedure would be like
    69 this (executed as root):
    70 
    71   rpm -i --prefix /usr/share polyml.i386.rpm
    72   rpm -i --prefix /usr/share isabelle.rpm
    73   rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
    74 
    75 The install prefix may be changed as indicated.  By default the ML
    76 system is expected to be at the same directory level as Isabelle
    77 itself; see [ISABELLE_HOME]/etc/settings of how to change this.
    78 
    79 Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    80 Isabelle as platform independent sources.  Precompiled object-logics
    81 are provided for convenience.
    82 
    83 
    84 Recompiling logics
    85 ------------------
    86 
    87 Some people prefer to be able to reconstruct the full system from the
    88 sources, rather than installing RPM packages blindly.  We do not
    89 provide source RPMs, yet any parts of Isabelle may be recompiled after
    90 installation of the main isabelle.rpm package (which contains only
    91 sources anyway).
    92 
    93 Assuming proper configuration of the underlying ML system, Isabelle
    94 object-logics may be recompiled like this:
    95 
    96   [ISABELLE_HOME]/build HOL FOL
    97 
    98 
    99 Source installation
   100 -------------------
   101 
   102 Traditional tar.gz archives are provided for the full Isabelle sources
   103 and documentation as well.  Make sure your ML system (SML/NJ, Poly/ML
   104 etc.) has already been installed properly; then proceed as follows.
   105 
   106 * Unpacking the archives.  After unpacking the Isabelle distribution
   107 archives (using tar and gzip) you are left with some directory
   108 IsabelleYY-X.  Basically, this may be installed anywhere --- just note
   109 that ~/isabelle would be a really bad idea, though.  The place where
   110 you put the contents of IsabelleYY-X will be referred to as
   111 [ISABELLE_HOME] subsequently.
   112 
   113 * Auto configuration.  There are some minor adaptions to be made of
   114 the Isabelle distribution to your system environment (mostly locations
   115 of bash and perl).  Simply do it like this:
   116 
   117   cd [ISABELLE_HOME]
   118   ./configure
   119 
   120 Note that this does not store any references to [ISABELLE_HOME].  You
   121 may safely move the system later, without having to run ./configure
   122 again.
   123 
   124 * ML system settings and compilation.  Before actual compilation you
   125 have to tell Isabelle about your Standard ML system.  These settings
   126 reside in ./etc/settings, which may be also overridden by
   127 ~/isabelle/etc/settings. There are already various sample
   128 configurations in ./etc/settings commented out.
   129 
   130 To build the core Isabelle/Pure and the default object-logic, just
   131 type
   132 
   133   ./build
   134 
   135 More object-logics can be made in a similar fashion:
   136 
   137   ./build FOL HOL
   138 
   139 Explicit make targets may be given as follows:
   140 
   141   ./build -m HOL-Real HOL
   142 
   143 After successful compilation you are ready to run the system, see 1)
   144 above for more information.
   145 
   146 
   147 $Id$