%

 \begin{isabellebody}%

 \def\isabellecontext{Basics}%

 %

 \isadelimtheory

 \isanewline

 \isanewline

 %

 \endisadelimtheory

 %

 \isatagtheory

 \isacommand{theory}\isamarkupfalse%

 \ Basics\isanewline

 \isakeyword{imports}\ Pure\isanewline

 \isakeyword{begin}%

 \endisatagtheory

 {\isafoldtheory}%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 %

 \isamarkupchapter{The Isabelle system environment%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 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{enumerate}

   \item The \emph{Isabelle settings} mechanism provides environment

   variables to all Isabelle programs (including tools and user

   interfaces).

   \item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}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.  Regular users rarely need to

   care about the low-level process.

   \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}})

   provides a generic startup environment Isabelle related utilities,

   user interfaces etc.  Such tools automatically benefit from the

   settings mechanism.

   \item The \emph{Isabelle interface wrapper} (\indexref{}{executable}{isabelle-interface}\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}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{enumerate}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsection{Isabelle settings \label{sec:settings}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 The Isabelle system heavily depends on the \emph{settings

   mechanism}\indexbold{settings}.  Essentially, this is a statically

   scoped collection of environment variables, such as \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}, \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}, \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}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 \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory into their shell's search path, but

   this is not required.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsection{Building the environment%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 Whenever any of the Isabelle executables is run, their settings

   environment is put together as follows.

   \begin{enumerate}

   \item The special variable \indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}} is

   determined automatically from the location of the binary that has

   been run.

   You should not try to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}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 \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility.  Symbolic

   links are admissible, but a plain copy of the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} files will not work!

   \item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} ist run as a

   \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} 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 \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}

   etc.).

   \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it

   exists) is run in the same way as the site default settings. Note

   that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set

   before --- usually to \verb|~/isabelle|.

   Thus individual users may override the site-wide defaults.  See also

   file \hyperlink{file.$ISABELLE-HOME/etc/user-settings.sample}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}user{\isacharminus}settings{\isachardot}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 \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}}. This could cause very annoying

   maintainance problems later, when the Isabelle installation is

   updated or changed otherwise.

   \end{enumerate}

   Since settings files are regular GNU \indexdef{}{executable}{bash}\hypertarget{executable.bash}{\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}}} scripts,

   one may use complex shell commands, such as \verb|if| or

   \verb|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 \indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}} and \indexdef{}{setting}{ISABELLE\_TOOL}\hypertarget{setting.ISABELLE-TOOL}{\hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}} are set

   automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables,

   respectively.

   \item \indexref{}{setting}{ISABELLE\_OUTPUT}\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} will have the identifiers of

   the Isabelle distribution (cf.\ \hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}) and

   the ML system (cf.\ \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}) appended automatically

   to its value.

   \end{itemize}

   \medskip Note that the settings environment may be inspected with

   the Isabelle tool \hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}.  This might help to figure out the

   effect of complex settings scripts.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsection{Common variables%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 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 \isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}.

   \begin{description}

   \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] 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 \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} yourself

   from the shell!

   \item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}}}] is the user-specific

   counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is

   \verb|~/isabelle|, under rare circumstances this may be

   changed in the global setting file.  Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to

   some extend. In particular, site-wide defaults may be overridden by

   a private \verb|$ISABELLE_HOME_USER/etc/settings|.

   \item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path

   names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively.  Thus other tools and scripts

   need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is

   on the current search path of the shell.

   \item[\indexdef{}{setting}{ISABELLE\_IDENTIFIER}\hypertarget{setting.ISABELLE-IDENTIFIER}{\hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] refers

   to the name of this Isabelle distribution, e.g.\ ``\verb|Isabelle2008|''.

   \item[\indexdef{}{setting}{ML\_SYSTEM}\hypertarget{setting.ML-SYSTEM}{\hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}}, \indexdef{}{setting}{ML\_HOME}\hypertarget{setting.ML-HOME}{\hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}},

   \indexdef{}{setting}{ML\_OPTIONS}\hypertarget{setting.ML-OPTIONS}{\hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isacharunderscore}OPTIONS}}}}}, \indexdef{}{setting}{ML\_PLATFORM}\hypertarget{setting.ML-PLATFORM}{\hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}}}, \indexdef{}{setting}{ML\_IDENTIFIER}\hypertarget{setting.ML-IDENTIFIER}{\hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] specify the underlying ML system

   to be used for Isabelle.  There is only a fixed set of admissable

   \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}} names (see the \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} file of the distribution).

   The actual compiler binary will be run from the directory \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}, with \hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isacharunderscore}OPTIONS}}}} as first arguments on the

   command line.  The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} may specify the

   binary format of ML heap images, which is useful for cross-platform

   installations.  The value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is

   automatically obtained by composing the values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}, \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} and the Isabelle version values.

   \item[\indexdef{}{setting}{ISABELLE\_PATH}\hypertarget{setting.ISABELLE-PATH}{\hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}}}] is a list of directories

   (separated by colons) where Isabelle logic images may reside.  When

   looking up heaps files, the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is

   appended to each component internally.

   \item[\indexdef{}{setting}{ISABELLE\_OUTPUT}\hypertarget{setting.ISABELLE-OUTPUT}{\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is a

   directory where output heap files should be stored by default. The

   ML system and Isabelle version identifier is appended here, too.

   \item[\indexdef{}{setting}{ISABELLE\_BROWSER\_INFO}\hypertarget{setting.ISABELLE-BROWSER-INFO}{\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}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 \verb|$ISABELLE_HOME_USER/browser_info|.

   \item[\indexdef{}{setting}{ISABELLE\_LOGIC}\hypertarget{setting.ISABELLE-LOGIC}{\hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}}}] specifies the default logic to

   load if none is given explicitely by the user.  The default value is

   \verb|HOL|.

   \item[\indexdef{}{setting}{ISABELLE\_LINE\_EDITOR}\hypertarget{setting.ISABELLE-LINE-EDITOR}{\hyperlink{setting.ISABELLE-LINE-EDITOR}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LINE{\isacharunderscore}EDITOR}}}}}] specifies the default

   line editor for the \indexref{}{tool}{tty}\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}} interface.

   \item[\indexdef{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hypertarget{setting.ISABELLE-USEDIR-OPTIONS}{\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed

   to the command line of any \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} invocation. This

   typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the

   \verb|IsaMakefile|s in the distribution).

   \item[\indexdef{}{setting}{ISABELLE\_FILE\_IDENT}\hypertarget{setting.ISABELLE-FILE-IDENT}{\hyperlink{setting.ISABELLE-FILE-IDENT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}FILE{\isacharunderscore}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[\indexdef{}{setting}{ISABELLE\_LATEX}\hypertarget{setting.ISABELLE-LATEX}{\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}}}, \indexdef{}{setting}{ISABELLE\_PDFLATEX}\hypertarget{setting.ISABELLE-PDFLATEX}{\hyperlink{setting.ISABELLE-PDFLATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PDFLATEX}}}}}, \indexdef{}{setting}{ISABELLE\_BIBTEX}\hypertarget{setting.ISABELLE-BIBTEX}{\hyperlink{setting.ISABELLE-BIBTEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BIBTEX}}}}}, \indexdef{}{setting}{ISABELLE\_DVIPS}\hypertarget{setting.ISABELLE-DVIPS}{\hyperlink{setting.ISABELLE-DVIPS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DVIPS}}}}}] refer to {\LaTeX} related tools for Isabelle

   document preparation (see also \secref{sec:tool-latex}).

   \item[\indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}}}] is a colon separated list of

   directories that are scanned by \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} for external

   utility programs (see also \secref{sec:isabelle-tool}).

   \item[\indexdef{}{setting}{ISABELLE\_DOCS}\hypertarget{setting.ISABELLE-DOCS}{\hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOCS}}}}}] is a colon separated list of

   directories with documentation files.

   \item[\indexdef{}{setting}{ISABELLE\_DOC\_FORMAT}\hypertarget{setting.ISABELLE-DOC-FORMAT}{\hyperlink{setting.ISABELLE-DOC-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOC{\isacharunderscore}FORMAT}}}}}] specifies the preferred

   document format, typically \verb|dvi| or \verb|pdf|.

   \item[\indexdef{}{setting}{DVI\_VIEWER}\hypertarget{setting.DVI-VIEWER}{\hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isacharunderscore}VIEWER}}}}}] specifies the command to be used

   for displaying \verb|dvi| files.

   \item[\indexdef{}{setting}{PDF\_VIEWER}\hypertarget{setting.PDF-VIEWER}{\hyperlink{setting.PDF-VIEWER}{\mbox{\isa{\isatt{PDF{\isacharunderscore}VIEWER}}}}}] specifies the command to be used

   for displaying \verb|pdf| files.

   \item[\indexdef{}{setting}{PRINT\_COMMAND}\hypertarget{setting.PRINT-COMMAND}{\hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isacharunderscore}COMMAND}}}}}] specifies the standard printer

   spool command, which is expected to accept \verb|ps| files.

   \item[\indexdef{}{setting}{ISABELLE\_TMP\_PREFIX}\hypertarget{setting.ISABELLE-TMP-PREFIX}{\hyperlink{setting.ISABELLE-TMP-PREFIX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TMP{\isacharunderscore}PREFIX}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is the

   prefix from which any running \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}

   derives an individual directory for temporary files.  The default is

   somewhere in \verb|/tmp|.

   \item[\indexdef{}{setting}{ISABELLE\_INTERFACE}\hypertarget{setting.ISABELLE-INTERFACE}{\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}}}] is an identifier that

   specifies the actual user interface that the capital \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} or \hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}} should invoke.  See

   \secref{sec:interface} for more details.

   \end{description}%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsection{The raw Isabelle process%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 The \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}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-process [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

   \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}} setting, which may consist of multiple

   components separated by colons --- these are tried in the given

   order with the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} appended

   internally.  In a similar way, base names are relative to the

   directory specified by \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}.  In any case,

   actual file locations may also be given by including at least one

   slash (\verb|/|) in the name (hint: use \verb|./| to

   refer to the current directory).%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{Options%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 If the input heap file does not have write permission bits set, or

   the \verb|-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 \verb|-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 \verb|-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 \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space

   consumption.

   \medskip The \verb|-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 \verb|-e| option, arbitrary ML code may be

   passed to the Isabelle session from the command line. Multiple

   \verb|-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 \verb|-u| option is a shortcut for \verb|-e| passing ``\verb|use "ROOT.ML";|'' to the ML session.

   The \verb|-f| option passes ``\verb|Session.finish();|'', which is intended mainly for administrative

   purposes.

   \medskip The \verb|-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 \verb|-e| texts). The \verb|-q|

   option inhibits interaction, thus providing a pure batch mode

   facility.

   \medskip The \verb|-I| option makes Isabelle enter Isar

   interaction mode on startup, instead of the primitive ML top-level.

   The \verb|-P| option configures the top-level loop for

   interaction with the Proof General user interface, and the

   \verb|-X| option enables XML-based PGIP communication.  The

   \verb|-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, see

   also \hyperlink{file.~~/src/Pure/Tools/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Tools{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/Tools/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Tools{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}.

   \medskip The \verb|-S| option makes the Isabelle process more

   secure by disabling some critical operations, notably runtime

   compilation and evaluation of ML source code.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{Examples%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 Run an interactive session of the default object-logic (as specified

   by the \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} setting) like this:

 \begin{ttbox}

 isabelle-process

 \end{ttbox}

   Usually \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} refers to one of the standard

   logic images, which are read-only by default.  A writable session

   --- based on \verb|FOL|, but output to \verb|Foo| (in the

   directory specified by the \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} setting) ---

   may be invoked as follows:

 \begin{ttbox}

 isabelle-process FOL Foo

 \end{ttbox}

   Ending this session normally (e.g.\ by typing control-D) dumps the

   whole ML system state into \verb|Foo|. Be prepared for several

   tens of megabytes.

   The \verb|Foo| session may be continued later (still in

   writable state) by:

 \begin{ttbox}

 isabelle-process Foo

 \end{ttbox}

   A read-only \verb|Foo| session may be started by:

 \begin{ttbox}

 isabelle-process -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 \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.

   \bigskip The next example demonstrates batch execution of Isabelle.

   We retrieve the \verb|FOL| theory value from the theory loader

   within ML:

 \begin{ttbox}

 isabelle-process -e 'theory "FOL";' -q -r FOL

 \end{ttbox}

   Note that the output text will be interspersed with additional junk

   messages by the ML runtime environment.  The \verb|-W| option

   allows to communicate with the Isabelle process via an external

   program in a more robust fashion.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 All Isabelle related tools and interfaces are called via a common

   wrapper --- \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}:

 \begin{ttbox}

 Usage: isabelle 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

   \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} from the directories listed in the \hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}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!%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{Examples%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 Show the list of available documentation of the current Isabelle

   installation like this:

 \begin{ttbox}

   isabelle doc

 \end{ttbox}

   View a certain document as follows:

 \begin{ttbox}

   isabelle 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}

   isabelle mkdir HOL Test && isabelle make

 \end{ttbox}

   Note that \verb|isabelle mkdir| is usually only invoked once;

   existing sessions (including document output etc.) are then updated

   by \verb|isabelle make| alone.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsection{The Isabelle interface wrapper \label{sec:interface}%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 Isabelle is a generic theorem prover, even w.r.t.\ its user

   interface.  The \indexdef{}{executable}{Isabelle}\hypertarget{executable.Isabelle}{\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}} (or \indexdef{}{executable}{isabelle-interface}\hypertarget{executable.isabelle-interface}{\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}}) executable provides a uniform way for

   end-users to invoke a certain interface; which one to start is

   determined by the \indexref{}{setting}{ISABELLE\_INTERFACE}\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}} setting

   variable, which should give a full path specification to the actual

   executable.

   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 \verb|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 \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} would automatically invoke Emacs with

   proper setup of the Proof General Lisp packages.  There are some

   options available, such as \verb|-l| for passing the logic

   image to be used by default, or \verb|-m| to tune the

   standard print mode.

   \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 \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} run from within.  This

   requires further Emacs Lisp configuration, see the Proof General

   documentation \cite{proofgeneral} for more information.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 %

 \isatagtheory

 \isacommand{end}\isamarkupfalse%

 %

 \endisatagtheory

 {\isafoldtheory}%

 %

 \isadelimtheory

 %

 \endisadelimtheory

 \end{isabellebody}%

 %%% Local Variables:

 %%% mode: latex

 %%% TeX-master: "root"

 %%% End: