--- a/doc-src/System/Makefile Mon Sep 15 16:40:53 2008 +0200
+++ b/doc-src/System/Makefile Mon Sep 15 16:42:00 2008 +0200
@@ -12,7 +12,7 @@
include ../Makefile.in
NAME = system
-FILES = system.tex basics.tex misc.tex present.tex symbols.tex \
+FILES = system.tex Thy/document/Basics.tex misc.tex present.tex symbols.tex \
../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
OUTPUT = syms.tex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/Thy/Basics.thy Mon Sep 15 16:42:00 2008 +0200
@@ -0,0 +1,527 @@
+(* $Id$ *)
+
+theory Basics
+imports Pure
+begin
+
+chapter {* The Isabelle system environment *}
+
+text {*
+ 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} (@{executable_def isatool})
+ provides a generic startup platform for Isabelle related utilities.
+ Thus tools automatically benefit from the settings mechanism.
+
+ \item The raw \emph{Isabelle process} (@{executable_def isabelle} or
+ @{executable_def "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} (@{executable_def
+ Isabelle} or @{executable_def "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 @{executable Isabelle}). This
+ assumes that the system has already been installed, of course. In
+ case you have to do this yourself, see the @{verbatim 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} *}
+
+text {*
+ The Isabelle system heavily depends on the \emph{settings
+ mechanism}\indexbold{settings}. Essentially, this is a statically
+ scoped collection of environment variables, such as @{setting
+ ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting 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.
+ Occasionally, users would still want to put the Isabelle @{verbatim
+ bin} directory into their shell's search path, but this is not
+ required.
+*}
+
+
+subsection {* Building the environment *}
+
+text {*
+ Whenever any of the Isabelle executables is run, their settings
+ environment is put together as follows.
+
+ \begin{enumerate}
+
+ \item The special variable @{setting_def ISABELLE_HOME} is
+ determined automatically from the location of the binary that has
+ been run.
+
+ You should not try to set @{setting 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 @{tool install} utility (see
+ \secref{sec:tool-install}). Just doing a plain copy of the
+ @{verbatim bin} files will not work!
+
+ \item The file @{verbatim "$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 @{setting ML_SYSTEM}
+ etc.).
+
+ \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
+ exists) is run in the same way as the site default settings. Note
+ that the variable @{setting ISABELLE_HOME_USER} has already been set
+ before --- usually to @{verbatim "~/isabelle"}.
+
+ Thus individual users may override the site-wide defaults. See also
+ file @{verbatim "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 @{verbatim
+ "$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 @{verbatim "if"} or
+ @{verbatim "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 @{setting_def ISABELLE} and @{setting_def ISATOOL} are set
+ automatically to the absolute path names of the @{executable
+ "isabelle-process"} and @{executable isatool} executables,
+ respectively.
+
+ \item @{setting_def ISABELLE_OUTPUT} will have the identifiers of
+ the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
+ the ML system (cf.\ @{setting 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 @{tool getenv} utility, see
+ \secref{sec:tool-getenv}.
+*}
+
+
+subsection{* Common variables *}
+
+text {*
+ 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 @{text "\<^sup>*"}.
+
+ \begin{description}
+
+ \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] 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 @{setting ISABELLE_HOME} yourself
+ from the shell.
+
+ \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
+ counterpart of @{setting ISABELLE_HOME}. The default value is
+ @{verbatim "~/isabelle"}, under rare circumstances this may be
+ changed in the global setting file. Typically, the @{setting
+ ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
+ some extend. In particular, site-wide defaults may be overridden by
+ a private @{verbatim "etc/settings"}.
+
+ \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting
+ ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path
+ names of the @{executable "isabelle-process"} and @{executable
+ isatool} executables, respectively. Thus other tools and scripts
+ need not assume that the Isabelle @{verbatim bin} directory is on
+ the current search path of the shell.
+
+ \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
+ to the name of this Isabelle distribution, e.g.\ ``@{verbatim
+ Isabelle2008}''.
+
+ \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
+ @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
+ ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
+ to be used for Isabelle. There is only a fixed set of admissable
+ @{setting ML_SYSTEM} names (see the @{verbatim "etc/settings"} file
+ of the distribution).
+
+ The actual compiler binary will be run from the directory @{setting
+ ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
+ command line. The optional @{setting ML_PLATFORM} may specify the
+ binary format of ML heap images, which is useful for cross-platform
+ installations. The value of @{setting ML_IDENTIFIER} is
+ automatically obtained by composing the values of @{setting
+ ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
+
+ \item[@{setting_def ISABELLE_PATH}] is a list of directories
+ (separated by colons) where Isabelle logic images may reside. When
+ looking up heaps files, the value of @{setting ML_IDENTIFIER} is
+ appended to each component internally.
+
+ \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
+ directory where output heap files should be stored by default. The
+ ML system and Isabelle version identifier is appended here, too.
+
+ \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
+ theory browser information (HTML text, graph data, and printable
+ documents) is stored (see also \secref{sec:info}). The default
+ value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
+
+ \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
+ load if none is given explicitely by the user. The default value is
+ @{verbatim HOL}.
+
+ \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
+ line editor for @{verbatim "isatool tty"} (see also
+ \secref{sec:tool-tty}).
+
+ \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
+ to the command line of any @{verbatim "isatool usedir"} invocation
+ (see also \secref{sec:tool-usedir}). This typically contains
+ compilation options for object-logics --- @{tool usedir} is the
+ basic utility for managing logic sessions (cf.\ the @{verbatim
+ IsaMakefile}s in the distribution).
+
+ \item[@{setting_def 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[@{setting_def ISABELLE_LATEX}, @{setting_def
+ ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
+ ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
+ document preparation (see also \secref{sec:tool-latex}).
+
+ \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
+ directories that are scanned by @{executable isatool} for external
+ utility programs (see also \secref{sec:isatool}).
+
+ \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
+ directories with documentation files.
+
+ \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
+ document format, typically @{verbatim dvi} or @{verbatim pdf}.
+
+ \item[@{setting_def DVI_VIEWER}] specifies the command to be used
+ for displaying @{verbatim dvi} files.
+
+ \item[@{setting_def PDF_VIEWER}] specifies the command to be used
+ for displaying @{verbatim pdf} files.
+
+ \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
+ spool command, which is expected to accept @{verbatim ps} files.
+
+ \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
+ prefix from which any running @{executable isabelle} process derives
+ an individual directory for temporary files. The default is
+ somewhere in @{verbatim "/tmp"}.
+
+ \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
+ specifies the actual user interface that the capital @{executable
+ Isabelle} or @{executable "isabelle-interface"} should invoke. See
+ \secref{sec:interface} for more details.
+
+ \end{description}
+*}
+
+
+section {* The Isabelle tools wrapper \label{sec:isatool} *}
+
+text {*
+ 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
+ \secref{sec:settings}. The set of available tools is collected by
+ @{executable isatool} from the directories listed in the @{setting
+ 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 *}
+
+text {*
+ 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
+ \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
+\begin{ttbox}
+ isatool mkdir HOL Test && isatool make
+\end{ttbox}
+ Note that @{verbatim "isatool mkdir"} is usually only invoked once;
+ existing sessions (including document output etc.) are then updated
+ by @{verbatim "isatool make"} alone.
+*}
+
+
+section {* The raw Isabelle process *}
+
+text {*
+ The @{executable_ref isabelle} (or @{executable_ref
+ "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 OUTPUT startup process wrapper, with messages going to OUTPUT stream
+ -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
+ @{setting ISABELLE_PATH} setting, which may consist of multiple
+ components separated by colons --- these are tried in the given
+ order with the value of @{setting ML_IDENTIFIER} appended
+ internally. In a similar way, base names are relative to the
+ directory specified by @{setting ISABELLE_OUTPUT}. In any case,
+ actual file locations may also be given by including at least one
+ slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
+ refer to the current directory).
+*}
+
+
+subsection {* Options *}
+
+text {*
+ If the input heap file does not have write permission bits set, or
+ the @{verbatim "-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
+ 50--200~MB). Users are responsible for themselves to dispose their
+ heap files when they are no longer needed.
+
+ \medskip The @{verbatim "-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 @{verbatim "-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 @{text "50%"} less disk space
+ consumption.
+
+ \medskip The @{verbatim "-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 @{verbatim "-e"} option, arbitrary ML code may be
+ passed to the Isabelle session from the command line. Multiple
+ @{verbatim "-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 @{verbatim "-u"} option is a shortcut for @{verbatim
+ "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
+ The @{verbatim "-f"} option passes ``@{verbatim "Session.finish ();"}'',
+ which is intended mainly for administrative purposes.
+
+ \medskip The @{verbatim "-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 @{verbatim "-e"} texts). The @{verbatim "-q"}
+ option inhibits interaction, thus providing a pure batch mode
+ facility.
+
+ \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
+ interaction mode on startup, instead of the primitive ML top-level.
+ The @{verbatim "-P"} option configures the top-level loop for
+ interaction with the Proof General user interface, and the
+ @{verbatim "-X"} option enables XML-based PGIP communication. The
+ @{verbatim "-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 @{verbatim "-S"} option makes the Isabelle process more
+ secure by disabling some critical operations, notably runtime
+ compilation and evaluation of ML source code.
+*}
+
+
+subsection {* Examples *}
+
+text {*
+ Run an interactive session of the default object-logic (as specified
+ by the @{setting ISABELLE_LOGIC} setting) like this:
+\begin{ttbox}
+isabelle
+\end{ttbox}
+
+ Usually @{setting ISABELLE_LOGIC} refers to one of the standard
+ logic images, which are read-only by default. A writable session
+ --- based on @{verbatim FOL}, but output to @{verbatim Foo} (in the
+ directory specified by the @{verbatim 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 @{verbatim Foo}. Be prepared for several
+ tens of megabytes.
+
+ The @{verbatim Foo} session may be continued later (still in
+ writable state) by:
+\begin{ttbox}
+isabelle Foo
+\end{ttbox}
+ A read-only @{verbatim 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 @{tool usedir} utility, see \secref{sec:tool-usedir}.
+
+ \bigskip The next example demonstrates batch execution of
+ Isabelle. We print a certain theorem of @{verbatim 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} *}
+
+text {*
+ Isabelle is a generic theorem prover, even w.r.t.\ its user
+ interface. The @{executable_ref Isabelle} (or @{executable_ref
+ "isabelle-interface"}) executable provides a uniform way for
+ end-users to invoke a certain interface; which one to start is
+ determined by the @{setting_ref ISABELLE_INTERFACE} setting
+ variable, which should give a full path specification to the actual
+ executable. Also note that the @{tool install} utility provides
+ some options to install desktop environment icons (see
+ \secref{sec:tool-install}).
+
+ Presently, the most prominent Isabelle interface is Proof
+ General~\cite{proofgeneral}\index{user interface!Proof General}.
+ The Proof General distribution includes an interface wrapper script
+ for the regular Isar toplevel, see @{verbatim
+ "ProofGeneral/isar/interface"}. The canonical settings for
+ Isabelle/Isar are as follows:
+
+\begin{ttbox}
+ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
+PROOFGENERAL_OPTIONS=""
+\end{ttbox}
+
+ Thus @{executable Isabelle} would automatically invoke Emacs with
+ proper setup of the Proof General Lisp packages. There are some
+ options available, such as @{verbatim "-l"} for passing the logic
+ image to be used by default, or @{verbatim "-m"} to tune the
+ standard print mode. The @{verbatim "-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 @{executable isabelle} run from within. This requires
+ further Emacs Lisp configuration, see the Proof General
+ documentation \cite{proofgeneral} for more information.
+*}
+
+end
--- 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: