INSTALL

tuned rpm command lines;

+
−
+
−Isabelle installation and compilation notes
+
−===========================================
+
−
+
−1) User installation
+
−--------------------
+
−
+
−Here we assume that Isabelle has already been installed at your site.
+
−Otherwise see 2) below of how to get the Isabelle system installed in
+
−the first place.
+
−
+
−
+
−1a) Running the Isabelle binaries
+
−---------------------------------
+
−
+
−The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
+
−directly from their location within the distribution directory
+
−[ISABELLE_HOME] like this:
+
−
+
−  [ISABELLE_HOME]/bin/isabelle HOL
+
−
+
−This starts an interactive Isabelle session within your current text
+
−terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
+
−search PATH, but this is not strictly necessary.
+
−
+
−
+
−Please do *not* copy (or link) the Isabelle scripts anywhere else ---
+
−they just won't work!  If you really want to install independent
+
−Isabelle binaries somewhere else then do it like this:
+
−
+
−  [ISABELLE_HOME]/bin/isatool install -p ~/bin
+
−
+
−Your site-wide Isabelle installation may already provide Isabelle
+
−executables in some global bin directory (such as /usr/bin).
+
−
+
−
+
−1b) Isabelle as KDE application
+
−-------------------------------
+
−
+
−Isabelle may be installed as application icon on the KDE desktop like
+
−this:
+
−
+
−  [ISABELLE_HOME]/bin/isatool install -k
+
−
+
−You may have to refresh the KDE desktop in order to see the new icon.
+
−Clicking on Isabelle will invoke the interface wrapper script (capital
+
−Isabelle), which is usually configured to run Proof General (see also
+
−the ISABELLE_INTERFACE setting).  Additional options may be passed to
+
−Isabelle by editing the application's command line using the standard
+
−KDE desktop functionality.
+
−
+
−
+
−2) System installation
+
−----------------------
+
−
+
−The Isabelle distribution is available both as traditional source-only
+
−tar.gz archives, and as binary packages (currently only RPM for
+
−Linux/x86).  In any case, the resulting Isabelle installation always
+
−contains the full sources, thus any part of the system be recompiled
+
−later, too.
+
−
+
−
+
−2a) Binary installation
+
−----------------------
+
−
+
−Ready-to-go RPM packages are provided for the ML compiler and runtime
+
−system, the Isabelle sources, and some major object-logics.  These
+
−packages should work on any major Linux/x86 platform based on RPM
+
−package management.
+
−
+
−A minimal installation would work like this (executed as root):
+
−
+
−  rpm -i --prefix /usr/share polyml.i386.rpm
+
−  rpm -i --prefix /usr/share isabelle.rpm
+
−  rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
+
−
+
−Note that installed RPMs may be removed like this:
+
−
+
−  rpm -e isabelle-HOL isabelle polyml
+
−
+
−The install prefix given above may be changed.  By default the ML
+
−system (and other contributed packages) are expected in either of the
+
−following three locations:
+
−
+
−  1) [ISABELLE_HOME]/contrib
+
−  2) [ISABELLE_HOME]/..
+
−  3) /usr/share
+
−  4) /usr/local
+
−
+
−This may be changed further by editing [ISABELLE_HOME]/etc/settings
+
−manually.
+
−
+
−Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
+
−Isabelle as platform independent sources.  Precompiled object-logics
+
−are provided for convenience.
+
−
+
−
+
−Recompiling logics
+
−------------------
+
−
+
−Some people prefer to be able to reconstruct the full system from the
+
−sources, rather than installing precompiled packages blindly.  We do
+
−not provide source RPMs, yet any parts of Isabelle may be recompiled
+
−after installation of the main isabelle.rpm package (which contains
+
−only sources anyway).
+
−
+
−Assuming proper configuration of the underlying ML system, Isabelle
+
−object-logics may be recompiled like this:
+
−
+
−  [ISABELLE_HOME]/build HOL FOL
+
−
+
−
+
−Source installation
+
−-------------------
+
−
+
−Traditional tar.gz archives are provided for the full Isabelle sources
+
−and documentation as well.  Make sure your ML system (e.g. Poly/ML
+
−etc.) has already been installed properly; then proceed as follows.
+
−
+
−* Unpacking the archives.  After unpacking the Isabelle distribution
+
−archives (using tar and gzip) you are left with some directory
+
−IsabelleYY-X.
+
−
+
−* Auto configuration.  There are some minor adaptions to be made of
+
−the Isabelle distribution to your system environment (locations of
+
−bash and perl).  Simply do it like this:
+
−
+
−  cd [ISABELLE_HOME]
+
−  ./configure
+
−
+
−Note that this does not store any references to [ISABELLE_HOME].  You
+
−may safely move the system later, without having to run ./configure
+
−again.
+
−
+
−* ML system settings and compilation.  Before actual compilation you
+
−have to tell Isabelle about your Standard ML system.  These settings
+
−reside in ./etc/settings, which may be also overridden by
+
−~/isabelle/etc/settings. There are already various sample
+
−configurations in ./etc/settings commented out.
+
−
+
−To build the core Isabelle/Pure and the default object-logic, just
+
−type
+
−
+
−  ./build
+
−
+
−More object-logics can be made in a similar fashion:
+
−
+
−  ./build FOL HOL
+
−
+
−Explicit make targets may be given as follows:
+
−
+
−  ./build -m HOL-Real HOL
+
−
+
−After successful compilation you are ready to run the system, see 1)
+
−above for more information.
+
−
+
−
+
−$Id$