--- /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