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$