--- a/doc-src/System/basics.tex Mon Sep 15 16:40:53 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,450 +0,0 @@
-
-% $Id$
-
-\chapter{The Isabelle system environment}
-
-This manual describes Isabelle together with related tools and user interfaces
-as seen from an outside (system oriented) view. See also the
-\emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} and the
-\emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the actual Isabelle
-commands and related functions.
-
-\medskip The Isabelle system environment emerges from a few general concepts.
-\begin{itemize}
-\item The \emph{Isabelle settings mechanism} provides environment variables to
- all Isabelle programs (including tools and user interfaces).
-\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}) provides a generic
- startup platform for Isabelle related utilities. Thus tools automatically
- benefit from the settings mechanism.
-\item The raw \emph{Isabelle process} (\ttindex{isabelle} or
- \texttt{isabelle-process}) runs logic sessions either interactively or in
- batch mode. In particular, this view abstracts over the invocation of the
- actual {\ML} system to be used.
-\item The \emph{Isabelle interface wrapper} (\ttindex{Isabelle} or
- \texttt{isabelle-interface}) provides some abstraction over the actual user
- interface to be used. The de-facto standard interface for Isabelle is
- Proof~General \cite{proofgeneral}.
-\end{itemize}
-
-\medskip The beginning user would probably just run the default user interface
-(by invoking the capital \texttt{Isabelle}). This assumes that the system has
-already been installed, of course. In case you have to do this yourself, see
-the \ttindex{INSTALL} file in the top-level directory of the distribution of
-how to proceed; binary packages for various system components are available as
-well.
-
-
-\section{Isabelle settings} \label{sec:settings}
-
-The Isabelle system heavily depends on the \emph{settings
- mechanism}\indexbold{settings}. Essentially, this is a statically scoped
-collection of environment variables, such as \texttt{ISABELLE_HOME},
-\texttt{ML_SYSTEM}, \texttt{ML_HOME}. These variables are \emph{not} intended
-to be set directly from the shell, though. Isabelle employs a somewhat more
-sophisticated scheme of \emph{settings files} --- one for site-wide defaults,
-another for additional user-specific modifications. With all configuration
-variables in at most two places, this scheme is more maintainable and
-user-friendly than global shell environment variables.
-
-In particular, we avoid the typical situation where prospective users of a
-software package are told to put several things into their shell startup
-scripts, before being able to actually run the program. Isabelle requires none
-such administrative chores of its end-users --- the executables can be invoked
-straight away.\footnote{Occasionally, users would still want to put the
- Isabelle \texttt{bin} directory into their shell's search path, but this is
- not required.}
-
-
-\subsection{Building the environment}
-
-Whenever any of the Isabelle executables is run, their settings environment is
-put together as follows.
-
-\begin{enumerate}
-\item The special variable \settdx{ISABELLE_HOME} is determined automatically
- from the location of the binary that has been run.
-
- You should not try to set \texttt{ISABELLE_HOME} manually. Also note that
- the Isabelle executables either have to be run from their original location
- in the distribution directory, or via the executable objects created by the
- \texttt{install} utility (see \S\ref{sec:tool-install}). Just doing a plain
- copy of the \texttt{bin} files will not work!
-
-\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
- with the auto-export option for variables enabled.
-
- This file holds a rather long list of shell variable assigments, thus
- providing the site-wide default settings. The Isabelle distribution already
- contains a global settings file with sensible defaults for most variables.
- When installing the system, only a few of these may have to be adapted
- (probably \texttt{ML_SYSTEM} etc.).
-
-\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
- run in the same way as the site default settings. Note that the variable
- \texttt{ISABELLE_HOME_USER} has already been set before --- usually to
- \texttt{\~\relax/isabelle}.
-
- Thus individual users may override the site-wide defaults. See also file
- \texttt{etc/user-settings.sample} in the distribution. Typically, a user
- settings file would contain only a few lines, just the assigments that are
- really changed. One should definitely \emph{not} start with a full copy the
- basic \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very annoying
- maintainance problems later, when the Isabelle installation is updated or
- changed otherwise.
-
-\end{enumerate}
-
-Note that settings files are actually full GNU bash scripts. So one may use
-complex shell commands, such as \texttt{if} or \texttt{case} statements to set
-variables depending on the system architecture or other environment variables.
-Such advanced features should be added only with great care, though. In
-particular, external environment references should be kept at a minimum.
-
-\medskip A few variables are somewhat special:
-\begin{itemize}
-\item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to the
- absolute path names of the \texttt{isabelle-process} and \texttt{isatool}
- executables, respectively.
-
-\item \settdx{ISABELLE_OUTPUT} will have the identifiers of the
- Isabelle distribution (cf.\ \texttt{ISABELLE_IDENTIFIER}) and the
- {\ML} system (cf.\ \texttt{ML_IDENTIFIER}) appended automatically to
- its value.
-\end{itemize}
-
-\medskip The Isabelle settings scheme is conceptually simple, but not
-completely trivial. For debugging purposes, the resulting environment may be
-inspected with the \texttt{getenv} utility, see \S\ref{sec:tool-getenv}.
-
-
-\subsection{Common variables}
-
-This is a reference of common Isabelle settings variables. Note that the list
-is somewhat open-ended. Third-party utilities or interfaces may add their own
-selection. Variables that are special in some sense are marked with *.
-
-\begin{description}
-\item[\settdx{ISABELLE_HOME}*] is the location of the top-level Isabelle
- distribution directory. This is automatically determined from the Isabelle
- executable that has been invoked. Do not attempt to set
- \texttt{ISABELLE_HOME} yourself from the shell.
-
-\item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of
- \texttt{ISABELLE_HOME}. The default value is \texttt{\~\relax/isabelle},
- under rare circumstances this may be changed in the global setting file.
- Typically, the \texttt{ISABELLE_HOME_USER} directory mimics
- \texttt{ISABELLE_HOME} to some extend. In particular, site-wide defaults may
- be overridden by a private \texttt{etc/settings}.
-
-\item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to the full
- path names of the \texttt{isabelle-process} and \texttt{isatool}
- executables, respectively. Thus other tools and scripts need not assume
- that the Isabelle \texttt{bin} directory is on the current search path of
- the shell.
-
-\item[\settdx{ISABELLE_IDENTIFIER}*] refers to the name of this
- Isabelle distribution, e.g.\ ``\texttt{Isabelle2007}''.
-
-\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
- \settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
- system to be used for Isabelle. There is only a fixed set of admissable
- \texttt{ML_SYSTEM} names (see the \texttt{etc/settings} file of the
- distribution).
-
- The actual compiler binary will be run from the directory \texttt{ML_HOME},
- with \texttt{ML_OPTIONS} as first arguments on the command line. The
- optional \texttt{ML_PLATFORM} may specify the binary format of ML heap
- images, which is useful for cross-platform installations. The value of
- \texttt{ML_IDENTIFIER} is automatically obtained by composing the values of
- \texttt{ML_SYSTEM}, \texttt{ML_PLATFORM} and the Isabelle version values.
-
-\item[\settdx{ISABELLE_PATH}] is a list of directories (separated by colons)
- where Isabelle logic images may reside. When looking up heaps files, the
- value of \texttt{ML_IDENTIFIER} is appended to each component internally.
-
-\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should
- be stored by default. The {\ML} system and Isabelle version identifier is
- appended here, too.
-
-\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory browser
- information (HTML text, graph data, and printable documents) is stored (see
- also \S\ref{sec:info}). The default value is
- \texttt{\$ISABELLE_HOME_USER/browser_info}.
-
-\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is
- given explicitely by the user. The default value is \texttt{HOL}.
-
-\item[\settdx{ISABELLE_LINE_EDITOR}] specifies the default line editor
- for \texttt{isatool tty} (see also \S\ref{sec:tool-tty}).
-
-\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command
- line of any \texttt{isatool usedir} invocation (see also
- \S\ref{sec:tool-usedir}). This typically contains compilation options for
- object-logics --- \texttt{usedir} is the basic utility for managing logic
- sessions (cf.\ the \texttt{IsaMakefile}s in the distribution).
-
-\item[\settdx{ISABELLE_FILE_IDENT}] specifies a shell command for
- producing a source file identification, based on the actual content
- instead of the full physical path and date stamp (which is the
- default). A typical identification would produce a ``digest'' of the
- text, using a cryptographic hash function like SHA-1, for example.
-
-\item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX},
- \settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related
- tools for Isabelle document preparation (see also \S\ref{sec:tool-latex}).
-
-\item[\settdx{ISABELLE_TOOLS}] is a colon separated list of directories that
- are scanned by \texttt{isatool} for external utility programs (see also
- \S\ref{sec:isatool}).
-
-\item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories with
- documentation files.
-
-\item[\settdx{ISABELLE_DOC_FORMAT}] specifies the preferred document format,
- typically \texttt{dvi} or \texttt{pdf}.
-
-\item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying
- \texttt{dvi} files.
-
-\item[\settdx{PDF_VIEWER}] specifies the command to be used for displaying
- \texttt{pdf} files.
-
-\item[\settdx{PRINT_COMMAND}] specifies the standard printer spool command,
- which is expected to accept \texttt{ps} files.
-
-\item[\settdx{ISABELLE_TMP_PREFIX}*] is the prefix from which any running
- \texttt{isabelle} process derives an individual directory for temporary
- files. The default is somewhere in \texttt{/tmp}.
-
-\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the actual
- user interface that the capital \texttt{Isabelle} or
- \texttt{isabelle-interface} should invoke. See \S\ref{sec:interface} for
- more details.
-
-\end{description}
-
-
-\section{The Isabelle tools wrapper} \label{sec:isatool}
-
-All Isabelle related utilities are called via a common wrapper ---
-\ttindex{isatool}:
-\begin{ttbox}
-Usage: isatool TOOL [ARGS ...]
-
- Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
- for more specific help.
-
- Available tools are:
-
- browser - Isabelle graph browser
- \dots
-\end{ttbox}
-In principle, Isabelle tools are ordinary executable scripts that are run
-within the Isabelle settings environment, see \S\ref{sec:settings}. The set
-of available tools is collected by \texttt{isatool} from the directories
-listed in the \texttt{ISABELLE_TOOLS} setting. Do not try to call the scripts
-directly from the shell. Neither should you add the tool directories to your
-shell's search path!
-
-
-\subsubsection*{Examples}
-
-Show the list of available documentation of the current Isabelle installation
-like this:
-\begin{ttbox}
- isatool doc
-\end{ttbox}
-
-View a certain document as follows:
-\begin{ttbox}
- isatool doc isar-ref
-\end{ttbox}
-
-Create an Isabelle session derived from HOL (see also \S\ref{sec:tool-mkdir}
-and \S\ref{sec:tool-make}):
-\begin{ttbox}
- isatool mkdir HOL Test && isatool make
-\end{ttbox}
-Note that \texttt{isatool mkdir} is usually only invoked once; existing
-sessions (including document output etc.) are then updated by \texttt{isatool
- make} alone.
-
-
-\section{The raw Isabelle process}
-
-The \ttindex{isabelle} (or \ttindex{isabelle-process}) executable runs
-bare-bones Isabelle logic sessions --- either interactively or in batch mode.
-It provides an abstraction over the underlying {\ML} system, and over the
-actual heap file locations. Its usage is:
-\begin{ttbox}
-Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
-
- Options are:
- -C tell ML system to copy output image
- -I startup Isar interaction mode
- -P startup Proof General interaction mode
- -S secure mode -- disallow critical operations
- -W startup process wrapper (interaction via external program)
- -X startup PGIP interaction mode
- -c tell ML system to compress output image
- -e MLTEXT pass MLTEXT to the ML session
- -f pass 'Session.finish();' to the ML session
- -m MODE add print mode for output
- -q non-interactive session
- -r open heap file read-only
- -u pass 'use"ROOT.ML";' to the ML session
- -w reset write permissions on OUTPUT
-
- INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
- These are either names to be searched in the Isabelle path, or
- actual file names (containing at least one /).
- If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
-\end{ttbox}
-Input files without path specifications are looked up in the
-\texttt{ISABELLE_PATH} setting, which may consist of multiple components
-separated by colons --- these are tried in the given order with the value of
-\texttt{ML_IDENTIFIER} appended internally. In a similar way, base names are
-relative to the directory specified by \texttt{ISABELLE_OUTPUT}. In any case,
-actual file locations may also be given by including at least one slash
-(\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
-directory).
-
-
-\subsection*{Options}
-
-If the input heap file does not have write permission bits set, or the
-\texttt{-r} option is given explicitely, then the session started will be
-read-only. That is, the {\ML} world cannot be committed back into the image
-file. Otherwise, a writable session enables commits into either the input
-file, or into another output heap file (if that is given as the second
-argument on the command line).
-
-The read-write state of sessions is determined at startup only, it cannot be
-changed intermediately. Also note that heap images may require considerable
-amounts of disk space (approximately 40--80~MB). Users are responsible for
-themselves to dispose their heap files when they are no longer needed.
-
-\medskip The \texttt{-w} option makes the output heap file read-only after
-terminating. Thus subsequent invocations cause the logic image to be
-read-only automatically.
-
-\medskip The \texttt{-c} option tells the underlying ML system to compress the
-output heap (fully transparently). On Poly/ML for example, the image is
-garbage collected and all stored values are maximally shared, resulting in up
-to 50\% less disk space consumption.
-
-\medskip The \texttt{-C} option tells the ML system to produce a completely
-self-contained output image, probably including a copy of the ML runtime
-system itself.
-
-\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
-the Isabelle session from the command line. Multiple \texttt{-e}'s are
-evaluated in the given order. Strange things may happen when errorneous {\ML}
-code is provided. Also make sure that the {\ML} commands are terminated
-properly by semicolon.
-
-\medskip The \texttt{-u} option is a shortcut for \texttt{-e} passing
-``\texttt{use"ROOT.ML";}'' to the {\ML} session. The \texttt{-f} option
-passes ``\texttt{Session.finish();}'', which is intended mainly for
-administrative purposes.
-
-\medskip The \texttt{-m} option adds identifiers of print modes to be made
-active for this session. Typically, this is used by some user interface, e.g.\
-to enable output of proper mathematical symbols.
-
-\medskip Isabelle normally enters an interactive top-level loop (after
-processing the \texttt{-e} texts). The \texttt{-q} option inhibits
-interaction, thus providing a pure batch mode facility.
-
-\medskip The \texttt{-I} option makes Isabelle enter Isar interaction
-mode on startup, instead of the primitive {\ML} top-level. The
-\texttt{-P} option configures the top-level loop for interaction with
-the Proof~General user interface, and the \texttt{-X} option enables
-XML-based PGIP communication. The \texttt{-W} option makes Isabelle
-enter a special process wrapper for interaction via an external
-program; the protocol is a stripped-down version of Proof~General the
-interaction mode.
-
-\medskip The \texttt{-S} option makes the Isabelle process more secure
-by disabling some critical operations, notably runtime compilation and
-evaluation of ML source code.
-
-
-\subsection*{Examples}
-
-Run an interactive session of the default object-logic (as specified
-by the \texttt{ISABELLE_LOGIC} setting) like this:
-\begin{ttbox}
-isabelle
-\end{ttbox}
-Usually \texttt{ISABELLE_LOGIC} refers to one of the standard logic
-images, which are read-only by default. A writable session --- based
-on \texttt{FOL}, but output to \texttt{Foo} (in the directory
-specified by the \texttt{ISABELLE_OUTPUT} setting) --- may be invoked
-as follows:
-\begin{ttbox}
-isabelle FOL Foo
-\end{ttbox}
-Ending this session normally (e.g.\ by typing control-D) dumps the whole {\ML}
-system state into \texttt{Foo}. Be prepared for several tens of megabytes.
-
-The \texttt{Foo} session may be continued later (still in writable
-state) by:
-\begin{ttbox}
-isabelle Foo
-\end{ttbox}
-A read-only \texttt{Foo} session may be started by:
-\begin{ttbox}
-isabelle -r Foo
-\end{ttbox}
-
-\medskip Note that manual session management like this does \emph{not} provide
-proper setup for theory presentation. This would require the \texttt{usedir}
-utility, see \S\ref{sec:tool-usedir}.
-
-\bigskip The next example demonstrates batch execution of Isabelle. We print a
-certain theorem of \texttt{FOL}:
-\begin{ttbox}
-isabelle -e "prth allE;" -q -r FOL
-\end{ttbox}
-Note that the output text will be interspersed with additional junk messages
-by the {\ML} runtime environment.
-
-
-\section{The Isabelle interface wrapper}\label{sec:interface}
-
-Isabelle is a generic theorem prover, even w.r.t.\ its user interface. The
-\ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
-uniform way for end-users to invoke a certain interface; which one to start is
-determined by the \settdx{ISABELLE_INTERFACE} setting variable, which should
-give a full path specification to the actual executable. Also note that the
-\texttt{install} utility provides some options to install desktop environment
-icons (see \S\ref{sec:tool-install}).
-
-Presently, the most prominent Isabelle interface is
-Proof~General~\cite{proofgeneral}\index{user interface!Proof General}. There
-are separate versions for the raw ML top-level and the proper Isabelle/Isar
-interpreter loop. The Proof~General distribution includes separate interface
-wrapper scripts (in \texttt{ProofGeneral/isa} and \texttt{ProofGeneral/isar})
-for either of these. The canonical settings for Isabelle/Isar are as follows:
-\begin{ttbox}
-ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
-PROOFGENERAL_OPTIONS=""
-\end{ttbox}
-Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
-the Proof~General Lisp packages. There are some options available, such as
-\texttt{-l} for passing the logic image to be used by default, or \texttt{-m}
-to tune the standard print mode. The \texttt{-I} option allows to switch
-between the Isar and ML view, independently of the interface script being
-used.
-
-\medskip Note that the world may be also seen the other way round: Emacs may
-be started first (with proper setup of Proof~General mode), and
-\texttt{isabelle} run from within. This requires further Emacs Lisp
-configuration, see the Proof~General documentation \cite{proofgeneral} for
-more information.
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "system"
-%%% End: