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