INSTALL
changeset 8809 85539b33be03
parent 6486 1f1d5e00e0a5
child 9927 7a9652294fe0
equal deleted inserted replaced
8808:204f4ebbba64 8809:85539b33be03
     1 
     1 
     2 Isabelle compilation and installation notes
     2 Isabelle installation and compilation notes
     3 ===========================================
     3 ===========================================
     4 
     4 
     5 Unpacking the archive
     5 1) User installation
     6 ---------------------
     6 --------------------
     7 
     7 
     8 After unpacking the Isabelle distribution archive (using tar and gzip)
     8 Here we assume that Isabelle has already been installed at your site.
     9 you are left with some directory IsabelleYY-X. You may install this
     9 Otherwise see 2) below of how to get the Isabelle system installed in
    10 anywhere, but please just *not* as ~/isabelle!!!
    10 the first place.
    11 
       
    12 The place where you put the contents of IsabelleYY-X will be referred
       
    13 to as [ISABELLE_HOME] subsequently.
       
    14 
    11 
    15 
    12 
    16 Auto configuration
    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
    17 ------------------
    87 ------------------
    18 
    88 
    19 There are some minor adaptions to be made of the Isabelle distribution
    89 Some people prefer to be able to reconstruct the full system from the
    20 to your system environment. Simply type:
    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:
    21 
   120 
    22   cd [ISABELLE_HOME]
   121   cd [ISABELLE_HOME]
    23   ./configure
   122   ./configure
    24 
   123 
    25 This does not store any references to [ISABELLE_HOME]. You may safely
   124 Note that this does not store any references to [ISABELLE_HOME].  You
    26 move the system later, without running ./configure again.
   125 may safely move the system later, without having to run ./configure
       
   126 again.
    27 
   127 
    28 
   128 
    29 ML system settings and compilation
   129 * ML system settings and compilation.  Before actual compilation you
    30 ----------------------------------
   130 have to tell Isabelle about your Standard ML system.  These settings
    31 
   131 reside in ./etc/settings, which may be also overridden by
    32 Before actual compilation you have to tell Isabelle about your
   132 ~/isabelle/etc/settings. There are already various sample
    33 Standard ML system.  These settings reside in ./etc/settings, which
   133 configurations in ./etc/settings commented out.
    34 may be also overridden by ~/isabelle/etc/settings. There are already
       
    35 various sample configurations in ./etc/settings commented out.
       
    36 
   134 
    37 To build the core Isabelle/Pure and the default object-logic, just
   135 To build the core Isabelle/Pure and the default object-logic, just
    38 type:
   136 type
    39 
   137 
    40   ./build
   138   ./build
    41 
   139 
    42 More object-logics can be made similarly:
   140 More object-logics can be made in a similar fashion:
    43 
   141 
    44   ./build FOL HOL
   142   ./build FOL HOL
    45 
   143 
    46 
   144 After successful compilation you are ready to run the system, see 1)
    47 Running the system
   145 above for more information.
    48 ------------------
       
    49 
       
    50 Provided that compilation was successful, you can now run something
       
    51 like:
       
    52 
       
    53   [ISABELLE_HOME]/bin/isabelle FOL
       
    54 
       
    55 This starts an interactive Isabelle session within your current text
       
    56 terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
       
    57 search PATH.
       
    58 
       
    59 Please do *not* copy (or link) the Isabelle scripts anywhere else, or
       
    60 they just won't work!  If you really feel the urge to install
       
    61 independent Isabelle binaries anywhere else do it like this:
       
    62 
       
    63   [ISABELLE_HOME]/bin/isatool install -p /usr/local/bin
       
    64 
       
    65 
   146 
    66 
   147 
    67 $Id$
   148 $Id$