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) User installation
1.11 +1) System installation
1.12 +----------------------
1.13 +
1.14 +The Isabelle distribution includes both complete sources and
1.15 +precompiled binary packages for common Unix platforms.
1.16 +
1.17 +
1.18 +Quick installation
1.19 +------------------
1.20 +
1.21 +Ready-to-go packages are provided for the ML compiler and runtime
1.22 +system, the Isabelle sources, and some major object-logics. A minimal
1.23 +site installation of Isabelle on Linux/x86 works like this:
1.24 +
1.25 + tar -C /usr/local -xzf Isabelle.tar.gz
1.26 + tar -C /usr/local -xzf polyml_base.tar.gz
1.27 + tar -C /usr/local -xzf polyml_x86-linux.tar.gz
1.28 + tar -C /usr/local -xzf HOL_x86-linux.tar.gz
1.29 +
1.30 +The install prefix given above may be changed as appropriate. By
1.31 +default the ML system (and other contributed packages) are expected in
1.32 +any of the following locations:
1.33 +
1.34 + 1) [ISABELLE_HOME]/contrib
1.35 + 2) [ISABELLE_HOME]/..
1.36 + 3) /usr/share
1.37 + 4) /usr/local
1.38 + 5) /opt
1.39 +
1.40 +This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
1.41 +
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 +Running the Isabelle binaries
1.84 +-----------------------------
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$