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 -After unpacking the Isabelle distribution archive (using tar and gzip)
1.15 -you are left with some directory IsabelleYY-X. You may install this
1.16 -anywhere, but please just *not* as ~/isabelle!!!
1.17 +Here we assume that Isabelle has already been installed at your site.
1.18 +Otherwise see 2) below of how to get the Isabelle system installed in
1.19 +the first place.
1.20
1.21 -The place where you put the contents of IsabelleYY-X will be referred
1.22 -to as [ISABELLE_HOME] subsequently.
1.23
1.24 +1a) Running the Isabelle binaries
1.25 +---------------------------------
1.26
1.27 -Auto configuration
1.28 +The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
1.29 +directly from their location within the distribution directory
1.30 +[ISABELLE_HOME] like this:
1.31 +
1.32 + [ISABELLE_HOME]/bin/isabelle HOL
1.33 +
1.34 +This starts an interactive Isabelle session within your current text
1.35 +terminal. You may want to put [ISABELLE_HOME]/bin into your shell's
1.36 +search PATH, but this is not strictly necessary.
1.37 +
1.38 +
1.39 +Please do *not* copy (or link) the Isabelle scripts anywhere else ---
1.40 +they just won't work! If you really want to install independent
1.41 +Isabelle binaries somewhere else then do it like this:
1.42 +
1.43 + [ISABELLE_HOME]/bin/isatool install -p ~/bin
1.44 +
1.45 +Your site-wide Isabelle installation may already provide Isabelle
1.46 +executables in some global bin directory (such as /usr/bin).
1.47 +
1.48 +
1.49 +1b) Isabelle as KDE application
1.50 +-------------------------------
1.51 +
1.52 +Isabelle may be installed as application icon on the KDE desktop like
1.53 +this:
1.54 +
1.55 + [ISABELLE_HOME]/bin/isatool install -k
1.56 +
1.57 +Clicking on that icon will invoke the interface wrapper script
1.58 +(capital Isabelle), which may be configured to run your favorite
1.59 +Isabelle user interface via the ISABELLE_INTERFACE setting.
1.60 +Additional options may be passed by editing the application's command
1.61 +line (by using the standard KDE desktop functionality).
1.62 +
1.63 +
1.64 +2) System installation
1.65 +----------------------
1.66 +
1.67 +The Isabelle distribution is available both as traditional source-only
1.68 +tar.gz archives, and as binary packages (currently only RPM for
1.69 +Linux/x86). In any case, the resulting Isabelle installation always
1.70 +contains the full sources, thus any part of the system be recompiled
1.71 +later, too.
1.72 +
1.73 +
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$