neuper@37871: WN1900721 copy from Isabelle2009-1
neuper@37871: !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
neuper@37871: 
neuper@37871: Isabelle installation notes
neuper@37871: ===========================
neuper@37871: 
neuper@37871: 1) System installation
neuper@37871: ----------------------
neuper@37871: 
neuper@37871: The Isabelle distribution includes both complete sources and
neuper@37871: precompiled binary packages for common Unix-like platforms.
neuper@37871: 
neuper@37871: 
neuper@37871: Quick installation
neuper@37871: ------------------
neuper@37871: 
neuper@37871: Ready-to-go packages are provided for the ML compiler and runtime
neuper@37871: system, the Isabelle sources, and some major object-logics.  A minimal
neuper@37871: site installation of Isabelle on Linux/x86 works like this:
neuper@37871: 
neuper@37871:   tar -C /usr/local -xzf Isabelle.tar.gz
neuper@37871:   tar -C /usr/local -xzf polyml.tar.gz
neuper@37871:   tar -C /usr/local -xzf HOL_x86-linux.tar.gz
neuper@37871: 
neuper@37871: The install prefix given above may be changed as appropriate; there is
neuper@37871: no need to install into a system directory like /usr/local at all.  By
neuper@37871: default the ML system (and other contributed packages) are expected in
neuper@37871: any of the following locations:
neuper@37871: 
neuper@37871:   1) [ISABELLE_HOME]/contrib
neuper@37871:   2) [ISABELLE_HOME]/..
neuper@37871:   4) /usr/local
neuper@37871:   3) /usr/share
neuper@37871:   5) /opt
neuper@37871: 
neuper@37871: This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
neuper@37871: 
neuper@37871: The installation may be finished as follows:
neuper@37871: 
neuper@37871:   cd [ISABELLE_HOME]
neuper@37871:   ./bin/isabelle install -p /usr/local/bin
neuper@37871: 
neuper@37871: The install utility creates global references to the present Isabelle
neuper@37871: installation, enabling users to invoke the Isabelle executables
neuper@37871: without explicit path names.  This is the only place where a static
neuper@37871: reference to [ISABELLE_HOME] is created; thus isabelle install has to
neuper@37871: be run again whenever the Isabelle distribution is moved later.
neuper@37871: 
neuper@37871: 
neuper@37871: Compiling logics
neuper@37871: ----------------
neuper@37871: 
neuper@37871: The Isabelle.tar.gz archive already contains all Isabelle sources (and
neuper@37871: documentation).  Precompiled object-logics are provided for
neuper@37871: convenience.
neuper@37871: 
neuper@37871: Assuming proper configuration of the underlying ML system
neuper@37871: (cf. Isabelle's etc/settings), further object-logics may be compiled
neuper@37871: like this:
neuper@37871: 
neuper@37871:   [ISABELLE_HOME]/build FOL
neuper@37871: 
neuper@37871: Special object-logic targets may be specified as follows:
neuper@37871: 
neuper@37871:   [ISABELLE_HOME]/build -m HOL-Algebra HOL
neuper@37871: 
neuper@37871: 
neuper@37871: 2) User installation
neuper@37871: --------------------
neuper@37871: 
neuper@37871: Running the Isabelle binaries
neuper@37871: -----------------------------
neuper@37871: 
neuper@37871: Users may invoke the main Isabelle binaries (isabelle and
neuper@37871: isabelle-process) directly from their location within the distribution
neuper@37871: directory [ISABELLE_HOME] like this:
neuper@37871: 
neuper@37871:   [ISABELLE_HOME]/bin/isabelle tty -l HOL
neuper@37871: 
neuper@37871: This starts an interactive Isabelle session within the current text
neuper@37871: terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
neuper@37871: PATH.  An alternative is to create global references to the Isabelle
neuper@37871: executables as follows:
neuper@37871: 
neuper@37871:   [ISABELLE_HOME]/bin/isabelle install -p ~/bin
neuper@37871: 
neuper@37871: Note that the site-wide Isabelle installation may already provide
neuper@37871: Isabelle executables in some global bin directory (such as
neuper@37871: /usr/local/bin).