INSTALL
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 8809 85539b33be03
child 9927 7a9652294fe0
permissions -rw-r--r--
added HOL/Prolog
     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 smlnj-110.0-3.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; changing this arrangement requires
    78 [ISABELLE_HOME]/etc/settings to be adapted manually.
    79 
    80 
    81 Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    82 Isabelle as platform independent sources.  Precompiled object-logics
    83 are provided for convenience.
    84 
    85 
    86 Recompiling logics
    87 ------------------
    88 
    89 Some people prefer to be able to reconstruct the full system from the
    90 sources, rather than installing RPM packages blindly.  We do not
    91 provide source RPMs, yet any parts of Isabelle may be recompiled after
    92 installation of the main isabelle.rpm package (which contains only
    93 sources anyway).
    94 
    95 Assuming proper configuration of the underlying ML system, Isabelle
    96 object-logics may be recompiled like this:
    97 
    98   [ISABELLE_HOME]/build HOL FOL
    99 
   100 
   101 Source installation
   102 -------------------
   103 
   104 Traditional tar.gz archives are provided for the full Isabelle sources
   105 and documentation as well.  Make sure your ML system (SML/NJ, Poly/ML
   106 etc.) has already been installed properly; then proceed as follows.
   107 
   108 
   109 * Unpacking the archives.  After unpacking the Isabelle distribution
   110 archives (using tar and gzip) you are left with some directory
   111 IsabelleYY-X.  Basically, this may be installed anywhere --- just note
   112 that ~/isabelle would be a really bad idea, though.  The place where
   113 you put the contents of IsabelleYY-X will be referred to as
   114 [ISABELLE_HOME] subsequently.
   115 
   116 
   117 * Auto configuration.  There are some minor adaptions to be made of
   118 the Isabelle distribution to your system environment (mostly locations
   119 of bash and perl).  Simply do it like this:
   120 
   121   cd [ISABELLE_HOME]
   122   ./configure
   123 
   124 Note that this does not store any references to [ISABELLE_HOME].  You
   125 may safely move the system later, without having to run ./configure
   126 again.
   127 
   128 
   129 * ML system settings and compilation.  Before actual compilation you
   130 have to tell Isabelle about your Standard ML system.  These settings
   131 reside in ./etc/settings, which may be also overridden by
   132 ~/isabelle/etc/settings. There are already various sample
   133 configurations in ./etc/settings commented out.
   134 
   135 To build the core Isabelle/Pure and the default object-logic, just
   136 type
   137 
   138   ./build
   139 
   140 More object-logics can be made in a similar fashion:
   141 
   142   ./build FOL HOL
   143 
   144 After successful compilation you are ready to run the system, see 1)
   145 above for more information.
   146 
   147 
   148 $Id$