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_x86-linux.tar.gz
wenzelm@10081:   tar -C /usr/local -xzf HOL_x86-linux.tar.gz
wenzelm@10081: 
wenzelm@24797: The install prefix given above may be changed as appropriate; there is
wenzelm@24797: no need to install into a system directory like /usr/local at all.  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@17547:   4) /usr/local
wenzelm@10081:   3) /usr/share
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@28504:   ./bin/isabelle install -p /usr/local/bin
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@28504: without explicit path names.  This is the only place where a static
wenzelm@28504: reference to [ISABELLE_HOME] is created; thus isabelle install has to
wenzelm@28504: 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@17547: 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: 
wenzelm@17547:   [ISABELLE_HOME]/build -m HOL-Algebra 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@28504: Users may invoke the main Isabelle binaries (isabelle and
wenzelm@28504: isabelle-process) directly from their location within the distribution
wenzelm@28504: directory [ISABELLE_HOME] like this:
wenzelm@8809: 
wenzelm@28504:   [ISABELLE_HOME]/bin/isabelle-process 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@28504:   [ISABELLE_HOME]/bin/isabelle 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).