simplified;
authorwenzelm
Tue Sep 26 17:04:17 2000 +0200 (2000-09-26)
changeset 10081352412857003
parent 10080 8fb8c17d1cb5
child 10082 7c2021b7c664
simplified;
INSTALL
     1.1 --- a/INSTALL	Tue Sep 26 17:03:52 2000 +0200
     1.2 +++ b/INSTALL	Tue Sep 26 17:04:17 2000 +0200
     1.3 @@ -1,158 +1,110 @@
     1.4  
     1.5 -Isabelle installation and compilation notes
     1.6 -===========================================
     1.7 +Isabelle installation notes
     1.8 +===========================
     1.9 +
    1.10 +1) System installation
    1.11 +----------------------
    1.12 +
    1.13 +The Isabelle distribution includes both complete sources and
    1.14 +precompiled binary packages for common Unix platforms.
    1.15 +
    1.16 +
    1.17 +Quick installation
    1.18 +------------------
    1.19 +
    1.20 +Ready-to-go packages are provided for the ML compiler and runtime
    1.21 +system, the Isabelle sources, and some major object-logics.  A minimal
    1.22 +site installation of Isabelle on Linux/x86 works like this:
    1.23 +
    1.24 +  tar -C /usr/local -xzf Isabelle.tar.gz
    1.25 +  tar -C /usr/local -xzf polyml_base.tar.gz
    1.26 +  tar -C /usr/local -xzf polyml_x86-linux.tar.gz
    1.27 +  tar -C /usr/local -xzf HOL_x86-linux.tar.gz
    1.28 +
    1.29 +The install prefix given above may be changed as appropriate.  By
    1.30 +default the ML system (and other contributed packages) are expected in
    1.31 +any of the following locations:
    1.32 +
    1.33 +  1) [ISABELLE_HOME]/contrib
    1.34 +  2) [ISABELLE_HOME]/..
    1.35 +  3) /usr/share
    1.36 +  4) /usr/local
    1.37 +  5) /opt
    1.38 +
    1.39 +This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
    1.40  
    1.41 -1) User installation
    1.42 +The installation may be finished as follows:
    1.43 +
    1.44 +  cd [ISABELLE_HOME]
    1.45 +  ./configure
    1.46 +  ./bin/isatool install -p /usr/local/bin
    1.47 +
    1.48 +Note that the configure script is only required for systems that do
    1.49 +not have bash and perl in the canonical places (/bin/bash and
    1.50 +/usr/bin/perl).
    1.51 +
    1.52 +The install utility creates global references to the present Isabelle
    1.53 +installation, enabling users to invoke the Isabelle executables
    1.54 +without explicit path names.  Incidently, this is the only place where
    1.55 +a static reference to [ISABELLE_HOME] is created; thus isatool install
    1.56 +has to be run again whenever the Isabelle distribution is moved later.
    1.57 +
    1.58 +
    1.59 +Compiling logics
    1.60 +----------------
    1.61 +
    1.62 +The Isabelle.tar.gz archive already contains all Isabelle sources (and
    1.63 +documentation). Precompiled object-logics are provided for
    1.64 +convenience.
    1.65 +
    1.66 +Assuming proper configuration of the underlying ML system
    1.67 +(cf. Isabelle's etc/settings), further object-logics may be compiled
    1.68 +like this:
    1.69 +
    1.70 +  [ISABELLE_HOME]/build FOL
    1.71 +
    1.72 +Special object-logic targets may be specified as follows:
    1.73 +
    1.74 +  [ISABELLE_HOME]/build -m HOL-Real HOL
    1.75 +
    1.76 +
    1.77 +2) User installation
    1.78  --------------------
    1.79  
    1.80 -Here we assume that Isabelle has already been installed at your site.
    1.81 -Otherwise see 2) below of how to get the Isabelle system installed in
    1.82 -the first place.
    1.83 -
    1.84 +Running the Isabelle binaries
    1.85 +-----------------------------
    1.86  
    1.87 -1a) Running the Isabelle binaries
    1.88 ----------------------------------
    1.89 -
    1.90 -The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
    1.91 +Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
    1.92  directly from their location within the distribution directory
    1.93  [ISABELLE_HOME] like this:
    1.94  
    1.95    [ISABELLE_HOME]/bin/isabelle HOL
    1.96  
    1.97 -This starts an interactive Isabelle session within your current text
    1.98 -terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
    1.99 -search PATH, but this is not strictly necessary.
   1.100 -
   1.101 -
   1.102 -Please do *not* copy (or link) the Isabelle scripts anywhere else ---
   1.103 -they just won't work!  If you really want to install independent
   1.104 -Isabelle binaries somewhere else then do it like this:
   1.105 +This starts an interactive Isabelle session within the current text
   1.106 +terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
   1.107 +PATH.  An alternative is to create global references to the Isabelle
   1.108 +executables as follows:
   1.109  
   1.110    [ISABELLE_HOME]/bin/isatool install -p ~/bin
   1.111  
   1.112 -Your site-wide Isabelle installation may already provide Isabelle
   1.113 -executables in some global bin directory (such as /usr/bin).
   1.114 +Note that the site-wide Isabelle installation may already provide
   1.115 +Isabelle executables in some global bin directory (such as
   1.116 +/usr/local/bin).
   1.117  
   1.118  
   1.119 -1b) Isabelle as KDE application
   1.120 --------------------------------
   1.121 +Isabelle as KDE application
   1.122 +---------------------------
   1.123  
   1.124 -Isabelle may be installed as application icon on the KDE desktop like
   1.125 -this:
   1.126 +Users may install an Isabelle application icon on the KDE desktop as
   1.127 +follows:
   1.128  
   1.129    [ISABELLE_HOME]/bin/isatool install -k
   1.130  
   1.131 -You may have to refresh the KDE desktop in order to see the new icon.
   1.132  Clicking on Isabelle will invoke the interface wrapper script (capital
   1.133 -Isabelle), which is usually configured to run Proof General (see also
   1.134 -the ISABELLE_INTERFACE setting).  Additional options may be passed to
   1.135 +Isabelle), which is usually configured to run Proof General (cf. the
   1.136 +ISABELLE_INTERFACE setting).  Additional options may be passed to
   1.137  Isabelle by editing the application's command line using the standard
   1.138 -KDE desktop functionality.
   1.139 -
   1.140 -
   1.141 -2) System installation
   1.142 -----------------------
   1.143 -
   1.144 -The Isabelle distribution is available both as traditional source-only
   1.145 -tar.gz archives, and as binary packages (currently only RPM for
   1.146 -Linux/x86).  In any case, the resulting Isabelle installation always
   1.147 -contains the full sources, thus any part of the system be recompiled
   1.148 -later, too.
   1.149 -
   1.150 -
   1.151 -2a) Binary installation
   1.152 -----------------------
   1.153 -
   1.154 -Ready-to-go RPM packages are provided for the ML compiler and runtime
   1.155 -system, the Isabelle sources, and some major object-logics.  These
   1.156 -packages should work on any major Linux/x86 platform based on RPM
   1.157 -package management.
   1.158 -
   1.159 -A minimal installation would work like this (executed as root):
   1.160 -
   1.161 -  rpm -i --prefix /usr/share polyml.i386.rpm
   1.162 -  rpm -i --prefix /usr/share isabelle.rpm
   1.163 -  rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
   1.164 -
   1.165 -Note that installed RPMs may be removed like this:
   1.166 -
   1.167 -  rpm -e isabelle-HOL isabelle polyml
   1.168 -
   1.169 -The install prefix given above may be changed.  By default the ML
   1.170 -system (and other contributed packages) are expected in either of the
   1.171 -following three locations:
   1.172 -
   1.173 -  1) [ISABELLE_HOME]/contrib
   1.174 -  2) [ISABELLE_HOME]/..
   1.175 -  3) /usr/share
   1.176 -  4) /usr/local
   1.177 -
   1.178 -This may be changed further by editing [ISABELLE_HOME]/etc/settings
   1.179 -manually.
   1.180 -
   1.181 -Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
   1.182 -Isabelle as platform independent sources.  Precompiled object-logics
   1.183 -are provided for convenience.
   1.184 -
   1.185 -
   1.186 -Recompiling logics
   1.187 -------------------
   1.188 -
   1.189 -Some people prefer to be able to reconstruct the full system from the
   1.190 -sources, rather than installing precompiled packages blindly.  We do
   1.191 -not provide source RPMs, yet any parts of Isabelle may be recompiled
   1.192 -after installation of the main isabelle.rpm package (which contains
   1.193 -only sources anyway).
   1.194 -
   1.195 -Assuming proper configuration of the underlying ML system, Isabelle
   1.196 -object-logics may be recompiled like this:
   1.197 -
   1.198 -  [ISABELLE_HOME]/build HOL FOL
   1.199 -
   1.200 -
   1.201 -Source installation
   1.202 --------------------
   1.203 -
   1.204 -Traditional tar.gz archives are provided for the full Isabelle sources
   1.205 -and documentation as well.  Make sure your ML system (e.g. Poly/ML
   1.206 -etc.) has already been installed properly; then proceed as follows.
   1.207 -
   1.208 -* Unpacking the archives.  After unpacking the Isabelle distribution
   1.209 -archives (using tar and gzip) you are left with some directory
   1.210 -IsabelleYY-X.
   1.211 -
   1.212 -* Auto configuration.  There are some minor adaptions to be made of
   1.213 -the Isabelle distribution to your system environment (locations of
   1.214 -bash and perl).  Simply do it like this:
   1.215 -
   1.216 -  cd [ISABELLE_HOME]
   1.217 -  ./configure
   1.218 -
   1.219 -Note that this does not store any references to [ISABELLE_HOME].  You
   1.220 -may safely move the system later, without having to run ./configure
   1.221 -again.
   1.222 -
   1.223 -* ML system settings and compilation.  Before actual compilation you
   1.224 -have to tell Isabelle about your Standard ML system.  These settings
   1.225 -reside in ./etc/settings, which may be also overridden by
   1.226 -~/isabelle/etc/settings. There are already various sample
   1.227 -configurations in ./etc/settings commented out.
   1.228 -
   1.229 -To build the core Isabelle/Pure and the default object-logic, just
   1.230 -type
   1.231 -
   1.232 -  ./build
   1.233 -
   1.234 -More object-logics can be made in a similar fashion:
   1.235 -
   1.236 -  ./build FOL HOL
   1.237 -
   1.238 -Explicit make targets may be given as follows:
   1.239 -
   1.240 -  ./build -m HOL-Real HOL
   1.241 -
   1.242 -After successful compilation you are ready to run the system, see 1)
   1.243 -above for more information.
   1.244 +KDE properties editing facilities.
   1.245  
   1.246  
   1.247  $Id$