INSTALL

* Isar/Pure: fixed 'token_translation' command;

+
−
+
−Isabelle installation notes
+
−===========================
+
−
+
−1) System installation
+
−----------------------
+
−
+
−The Isabelle distribution includes both complete sources and
+
−precompiled binary packages for common Unix platforms.
+
−
+
−
+
−Quick installation
+
−------------------
+
−
+
−Ready-to-go packages are provided for the ML compiler and runtime
+
−system, the Isabelle sources, and some major object-logics.  A minimal
+
−site installation of Isabelle on Linux/x86 works like this:
+
−
+
−  tar -C /usr/local -xzf Isabelle.tar.gz
+
−  tar -C /usr/local -xzf polyml_base.tar.gz
+
−  tar -C /usr/local -xzf polyml_x86-linux.tar.gz
+
−  tar -C /usr/local -xzf HOL_x86-linux.tar.gz
+
−
+
−The install prefix given above may be changed as appropriate.  By
+
−default the ML system (and other contributed packages) are expected in
+
−any of the following locations:
+
−
+
−  1) [ISABELLE_HOME]/contrib
+
−  2) [ISABELLE_HOME]/..
+
−  3) /usr/share
+
−  4) /usr/local
+
−  5) /opt
+
−
+
−This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
+
−
+
−The installation may be finished as follows:
+
−
+
−  cd [ISABELLE_HOME]
+
−  ./configure
+
−  ./bin/isatool install -p /usr/local/bin
+
−
+
−Note that the configure script is only required for systems that do
+
−not have bash and perl in the canonical places (/bin/bash and
+
−/usr/bin/perl).
+
−
+
−The install utility creates global references to the present Isabelle
+
−installation, enabling users to invoke the Isabelle executables
+
−without explicit path names.  Incidently, this is the only place where
+
−a static reference to [ISABELLE_HOME] is created; thus isatool install
+
−has to be run again whenever the Isabelle distribution is moved later.
+
−
+
−
+
−Compiling logics
+
−----------------
+
−
+
−The Isabelle.tar.gz archive already contains all Isabelle sources (and
+
−documentation). Precompiled object-logics are provided for
+
−convenience.
+
−
+
−Assuming proper configuration of the underlying ML system
+
−(cf. Isabelle's etc/settings), further object-logics may be compiled
+
−like this:
+
−
+
−  [ISABELLE_HOME]/build FOL
+
−
+
−Special object-logic targets may be specified as follows:
+
−
+
−  [ISABELLE_HOME]/build -m HOL-Real HOL
+
−
+
−
+
−2) User installation
+
−--------------------
+
−
+
−Running the Isabelle binaries
+
−-----------------------------
+
−
+
−Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
+
−directly from their location within the distribution directory
+
−[ISABELLE_HOME] like this:
+
−
+
−  [ISABELLE_HOME]/bin/isabelle HOL
+
−
+
−This starts an interactive Isabelle session within the current text
+
−terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
+
−PATH.  An alternative is to create global references to the Isabelle
+
−executables as follows:
+
−
+
−  [ISABELLE_HOME]/bin/isatool install -p ~/bin
+
−
+
−Note that the site-wide Isabelle installation may already provide
+
−Isabelle executables in some global bin directory (such as
+
−/usr/local/bin).
+
−
+
−
+
−Isabelle as KDE application
+
−---------------------------
+
−
+
−Users may install an Isabelle application icon on the KDE 2 desktop as
+
−follows (version 1 may be specified as well):
+
−
+
−  [ISABELLE_HOME]/bin/isatool install -k 2
+
−
+
−Clicking on Isabelle will invoke the interface wrapper script (capital
+
−Isabelle), which is usually configured to run Proof General (cf. the
+
−ISABELLE_INTERFACE setting).  Additional options may be passed to
+
−Isabelle by editing the application's command line using the standard
+
−KDE properties editing facilities.
+
−
+
−
+
−$Id$