INSTALL
changeset 8809 85539b33be03
parent 6486 1f1d5e00e0a5
child 9927 7a9652294fe0
     1.1 --- a/INSTALL	Fri May 05 22:18:40 2000 +0200
     1.2 +++ b/INSTALL	Fri May 05 22:23:27 2000 +0200
     1.3 @@ -1,67 +1,148 @@
     1.4  
     1.5 -Isabelle compilation and installation notes
     1.6 +Isabelle installation and compilation notes
     1.7  ===========================================
     1.8  
     1.9 -Unpacking the archive
    1.10 ----------------------
    1.11 +1) User installation
    1.12 +--------------------
    1.13 +
    1.14 +Here we assume that Isabelle has already been installed at your site.
    1.15 +Otherwise see 2) below of how to get the Isabelle system installed in
    1.16 +the first place.
    1.17 +
    1.18 +
    1.19 +1a) Running the Isabelle binaries
    1.20 +---------------------------------
    1.21 +
    1.22 +The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
    1.23 +directly from their location within the distribution directory
    1.24 +[ISABELLE_HOME] like this:
    1.25 +
    1.26 +  [ISABELLE_HOME]/bin/isabelle HOL
    1.27 +
    1.28 +This starts an interactive Isabelle session within your current text
    1.29 +terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
    1.30 +search PATH, but this is not strictly necessary.
    1.31 +
    1.32 +
    1.33 +Please do *not* copy (or link) the Isabelle scripts anywhere else ---
    1.34 +they just won't work!  If you really want to install independent
    1.35 +Isabelle binaries somewhere else then do it like this:
    1.36 +
    1.37 +  [ISABELLE_HOME]/bin/isatool install -p ~/bin
    1.38  
    1.39 -After unpacking the Isabelle distribution archive (using tar and gzip)
    1.40 -you are left with some directory IsabelleYY-X. You may install this
    1.41 -anywhere, but please just *not* as ~/isabelle!!!
    1.42 +Your site-wide Isabelle installation may already provide Isabelle
    1.43 +executables in some global bin directory (such as /usr/bin).
    1.44 +
    1.45 +
    1.46 +1b) Isabelle as KDE application
    1.47 +-------------------------------
    1.48 +
    1.49 +Isabelle may be installed as application icon on the KDE desktop like
    1.50 +this:
    1.51 +
    1.52 +  [ISABELLE_HOME]/bin/isatool install -k
    1.53  
    1.54 -The place where you put the contents of IsabelleYY-X will be referred
    1.55 -to as [ISABELLE_HOME] subsequently.
    1.56 +Clicking on that icon will invoke the interface wrapper script
    1.57 +(capital Isabelle), which may be configured to run your favorite
    1.58 +Isabelle user interface via the ISABELLE_INTERFACE setting.
    1.59 +Additional options may be passed by editing the application's command
    1.60 +line (by using the standard KDE desktop functionality).
    1.61 +
    1.62 +
    1.63 +2) System installation
    1.64 +----------------------
    1.65 +
    1.66 +The Isabelle distribution is available both as traditional source-only
    1.67 +tar.gz archives, and as binary packages (currently only RPM for
    1.68 +Linux/x86).  In any case, the resulting Isabelle installation always
    1.69 +contains the full sources, thus any part of the system be recompiled
    1.70 +later, too.
    1.71  
    1.72  
    1.73 -Auto configuration
    1.74 +2a) Binary installation
    1.75 +----------------------
    1.76 +
    1.77 +Ready-to-go RPM packages are provided for the ML compiler and runtime
    1.78 +system, the Isabelle sources, and some major object-logics.  These
    1.79 +packages should work on any major RPM-based Linux/x86 platform (such
    1.80 +as SuSE, RedHat etc.).  A typical installation procedure would be like
    1.81 +this (executed as root):
    1.82 +
    1.83 +  rpm -i smlnj-110.0-3.i386.rpm
    1.84 +  rpm -i --prefix /usr/share isabelle.rpm
    1.85 +  rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
    1.86 +
    1.87 +The install prefix may be changed as indicated.  By default the ML
    1.88 +system is expected to be at the same directory level as Isabelle
    1.89 +itself; changing this arrangement requires
    1.90 +[ISABELLE_HOME]/etc/settings to be adapted manually.
    1.91 +
    1.92 +
    1.93 +Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
    1.94 +Isabelle as platform independent sources.  Precompiled object-logics
    1.95 +are provided for convenience.
    1.96 +
    1.97 +
    1.98 +Recompiling logics
    1.99  ------------------
   1.100  
   1.101 -There are some minor adaptions to be made of the Isabelle distribution
   1.102 -to your system environment. Simply type:
   1.103 +Some people prefer to be able to reconstruct the full system from the
   1.104 +sources, rather than installing RPM packages blindly.  We do not
   1.105 +provide source RPMs, yet any parts of Isabelle may be recompiled after
   1.106 +installation of the main isabelle.rpm package (which contains only
   1.107 +sources anyway).
   1.108 +
   1.109 +Assuming proper configuration of the underlying ML system, Isabelle
   1.110 +object-logics may be recompiled like this:
   1.111 +
   1.112 +  [ISABELLE_HOME]/build HOL FOL
   1.113 +
   1.114 +
   1.115 +Source installation
   1.116 +-------------------
   1.117 +
   1.118 +Traditional tar.gz archives are provided for the full Isabelle sources
   1.119 +and documentation as well.  Make sure your ML system (SML/NJ, Poly/ML
   1.120 +etc.) has already been installed properly; then proceed as follows.
   1.121 +
   1.122 +
   1.123 +* Unpacking the archives.  After unpacking the Isabelle distribution
   1.124 +archives (using tar and gzip) you are left with some directory
   1.125 +IsabelleYY-X.  Basically, this may be installed anywhere --- just note
   1.126 +that ~/isabelle would be a really bad idea, though.  The place where
   1.127 +you put the contents of IsabelleYY-X will be referred to as
   1.128 +[ISABELLE_HOME] subsequently.
   1.129 +
   1.130 +
   1.131 +* Auto configuration.  There are some minor adaptions to be made of
   1.132 +the Isabelle distribution to your system environment (mostly locations
   1.133 +of bash and perl).  Simply do it like this:
   1.134  
   1.135    cd [ISABELLE_HOME]
   1.136    ./configure
   1.137  
   1.138 -This does not store any references to [ISABELLE_HOME]. You may safely
   1.139 -move the system later, without running ./configure again.
   1.140 +Note that this does not store any references to [ISABELLE_HOME].  You
   1.141 +may safely move the system later, without having to run ./configure
   1.142 +again.
   1.143  
   1.144  
   1.145 -ML system settings and compilation
   1.146 -----------------------------------
   1.147 -
   1.148 -Before actual compilation you have to tell Isabelle about your
   1.149 -Standard ML system.  These settings reside in ./etc/settings, which
   1.150 -may be also overridden by ~/isabelle/etc/settings. There are already
   1.151 -various sample configurations in ./etc/settings commented out.
   1.152 +* ML system settings and compilation.  Before actual compilation you
   1.153 +have to tell Isabelle about your Standard ML system.  These settings
   1.154 +reside in ./etc/settings, which may be also overridden by
   1.155 +~/isabelle/etc/settings. There are already various sample
   1.156 +configurations in ./etc/settings commented out.
   1.157  
   1.158  To build the core Isabelle/Pure and the default object-logic, just
   1.159 -type:
   1.160 +type
   1.161  
   1.162    ./build
   1.163  
   1.164 -More object-logics can be made similarly:
   1.165 +More object-logics can be made in a similar fashion:
   1.166  
   1.167    ./build FOL HOL
   1.168  
   1.169 -
   1.170 -Running the system
   1.171 -------------------
   1.172 -
   1.173 -Provided that compilation was successful, you can now run something
   1.174 -like:
   1.175 -
   1.176 -  [ISABELLE_HOME]/bin/isabelle FOL
   1.177 -
   1.178 -This starts an interactive Isabelle session within your current text
   1.179 -terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
   1.180 -search PATH.
   1.181 -
   1.182 -Please do *not* copy (or link) the Isabelle scripts anywhere else, or
   1.183 -they just won't work!  If you really feel the urge to install
   1.184 -independent Isabelle binaries anywhere else do it like this:
   1.185 -
   1.186 -  [ISABELLE_HOME]/bin/isatool install -p /usr/local/bin
   1.187 -
   1.188 +After successful compilation you are ready to run the system, see 1)
   1.189 +above for more information.
   1.190  
   1.191  
   1.192  $Id$