doc-src/System/Thy/document/Basics.tex

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

%
\begin{isabellebody}%
\def\isabellecontext{Basics}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Basics\isanewline
\isakeyword{imports}\ Base\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 a system oriented view.  See also the
  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
  the actual Isabelle input language and related concepts, and
  \emph{The Isabelle/Isar Implementation
  Manual}~\cite{isabelle-implementation} for the main concepts of the
  underlying implementation in Isabelle/ML.

  \medskip The Isabelle system environment provides the following
  basic infrastructure to integrate tools smoothly.

  \begin{enumerate}

  \item The \emph{Isabelle settings} mechanism provides process
  environment variables to all Isabelle executables (including tools
  and user interfaces).

  \item The raw \emph{Isabelle process} (\indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\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 main \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.

  \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{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}, \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\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 clearly defined 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 \verb|$ISABELLE_HOME/bin| directory into their shell's search path, but
  this is not required.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Bootstrapping the environment \label{sec:boot}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle executables need to be run within a proper settings
  environment.  This is bootstrapped as described below, on the first
  invocation of one of the outer wrapper scripts (such as
  \indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}).  This happens only once for each
  process tree, i.e.\ the environment is passed to subprocesses
  according to regular Unix conventions.

  \begin{enumerate}

  \item The special variable \indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\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{\isaliteral{5F}{\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 \verb|$ISABELLE_HOME/bin| files will not work!

  \item The file \verb|$ISABELLE_HOME/etc/settings| is 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{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} has already been set
  before --- usually to something like \verb|$USER_HOME/.isabelle/IsabelleXXXX|.
  
  Thus individual users may override the site-wide defaults.  See also
  file \verb|$ISABELLE_HOME/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 \verb|$ISABELLE_HOME/etc/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{\isaliteral{5F}{\isacharunderscore}}PROCESS}}}}} and \indexdef{}{setting}{ISABELLE\_TOOL}\hypertarget{setting.ISABELLE-TOOL}{\hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOL}}}}} are set
  automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\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{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} will have the identifiers of
  the Isabelle distribution (cf.\ \hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}) and
  the ML system (cf.\ \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\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{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}.

  \begin{description}

  \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the cross-platform
  user home directory.  On Unix systems this is usually the same as
  \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home directory of
  the user, not the one of within the Cygwin root
  file-system.\footnote{Cygwin itself offers another choice whether
  its HOME should point to the \texttt{/home} directory tree or the
  Windows user home.}

 \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}}] is the user-specific
  counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}. The default value is
  relative to \verb|$USER_HOME/.isabelle|, under rare
  circumstances this may be changed in the global setting file.
  Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} directory mimics
  \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\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\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is automatically
  set to a symbolic identifier for the underlying hardware and
  operating system.  The Isabelle platform identification always
  refers to the 32 bit variant, even this is a 64 bit machine.  Note
  that the ML or Java runtime may have a different idea, depending on
  which binaries are actually run.

  \item[\indexdef{}{setting}{ISABELLE\_PLATFORM64}\hypertarget{setting.ISABELLE-PLATFORM64}{\hyperlink{setting.ISABELLE-PLATFORM64}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PLATFORM{\isadigit{6}}{\isadigit{4}}}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is similar to
  \hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} but refers to the proper 64 bit variant
  on a platform that supports this; the value is empty for 32 bit.
  Note that the following bash expression (including the quotes)
  prefers the 64 bit platform, if that is available:

  \verb|"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"|

  \item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PROCESS}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOL}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] are automatically set to the full path
  names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively.  Thus other tools and scripts
  need not assume that the \verb|$ISABELLE_HOME/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{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] refers
  to the name of this Isabelle distribution, e.g.\ ``\verb|Isabelle2012|''.

  \item[\indexdef{}{setting}{ML\_SYSTEM}\hypertarget{setting.ML-SYSTEM}{\hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}}, \indexdef{}{setting}{ML\_HOME}\hypertarget{setting.ML-HOME}{\hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}HOME}}}}},
  \indexdef{}{setting}{ML\_OPTIONS}\hypertarget{setting.ML-OPTIONS}{\hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}, \indexdef{}{setting}{ML\_PLATFORM}\hypertarget{setting.ML-PLATFORM}{\hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}}, \indexdef{}{setting}{ML\_IDENTIFIER}\hypertarget{setting.ML-IDENTIFIER}{\hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\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{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \verb|$ISABELLE_HOME/etc/settings| file of the distribution).
  
  The actual compiler binary will be run from the directory \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, with \hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} as first arguments on the
  command line.  The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} is
  automatically obtained by composing the values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}, \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} and the Isabelle version values.

  \item[\indexdef{}{setting}{ISABELLE\_JDK\_HOME}\hypertarget{setting.ISABELLE-JDK-HOME}{\hyperlink{setting.ISABELLE-JDK-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}JDK{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}] needs to point to a full JDK
  (Java Development Kit) installation with \verb|javac| and
  \verb|jar| executables.  This is essential for Isabelle/Scala
  and other JVM-based tools to work properly.  Note that conventional
  \verb|JAVA_HOME| usually points to the JRE (Java Runtime
  Environment), not JDK.
  
  \item[\indexdef{}{setting}{ISABELLE\_PATH}\hypertarget{setting.ISABELLE-PATH}{\hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\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{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}LINE{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\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\_LATEX}\hypertarget{setting.ISABELLE-LATEX}{\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LATEX}}}}}, \indexdef{}{setting}{ISABELLE\_PDFLATEX}\hypertarget{setting.ISABELLE-PDFLATEX}{\hyperlink{setting.ISABELLE-PDFLATEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PDFLATEX}}}}}, \indexdef{}{setting}{ISABELLE\_BIBTEX}\hypertarget{setting.ISABELLE-BIBTEX}{\hyperlink{setting.ISABELLE-BIBTEX}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BIBTEX}}}}}, \indexdef{}{setting}{ISABELLE\_DVIPS}\hypertarget{setting.ISABELLE-DVIPS}{\hyperlink{setting.ISABELLE-DVIPS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}DOC{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\isacharunderscore}}TMP{\isaliteral{5F}{\isacharunderscore}}PREFIX}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the
  prefix from which any running \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}
  derives an individual directory for temporary files.  The default is
  somewhere in \verb|/tmp|.
  
  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Additional components \label{sec:components}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Any directory may be registered as an explicit \emph{Isabelle
  component}.  The general layout conventions are that of the main
  Isabelle distribution itself, and the following two files (both
  optional) have a special meaning:

  \begin{itemize}

  \item \verb|etc/settings| holds additional settings that are
  initialized when bootstrapping the overall Isabelle environment,
  cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
  \verb|bash| script.  It may refer to the component's enclosing
  directory via the \verb|COMPONENT| shell variable.

  For example, the following setting allows to refer to files within
  the component later on, without having to hardwire absolute paths:

  \begin{ttbox}
  MY_COMPONENT_HOME="$COMPONENT"
  \end{ttbox}

  Components can also add to existing Isabelle settings such as
  \indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOLS}}}}}, in order to provide
  component-specific tools that can be invoked by end-users.  For
  example:

  \begin{ttbox}
  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
  \end{ttbox}

  \item \verb|etc/components| holds a list of further
  sub-components of the same structure.  The directory specifications
  given here can be either absolute (with leading \verb|/|) or
  relative to the component's main directory.

  \end{itemize}

  The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
  itself.  After initializing all of its sub-components recursively,
  \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
  that directory exists).  This allows to install private components
  via \verb|$ISABELLE_HOME_USER/etc/components|, although it is
  often more convenient to do that programmatically via the
  \verb,init_component, shell function in the \verb,etc/settings,
  script of \verb,$ISABELLE_HOME_USER, (or any other component
  directory).  For example:
  \begin{verbatim}
  if [ -d "$HOME/screwdriver-2.0" ]
  then
    init_component "$HOME/screwdriver-2.0"
  else
  \end{verbatim}%
\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{\isaliteral{2D}{\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:
    -I           startup Isar interaction mode
    -P           startup Proof General interaction mode
    -S           secure mode -- disallow critical operations
    -T ADDR      startup process wrapper, with socket address
    -W IN:OUT    startup process wrapper, with input/output fifos
    -X           startup PGIP interaction mode
    -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{\isaliteral{5F}{\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{\isaliteral{5F}{\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{\isaliteral{5F}{\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 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.

  \medskip The \verb|-T| or \verb|-W| option makes
  Isabelle enter a special process wrapper for interaction via the
  Isabelle/Scala layer, see also \verb|~~/src/Pure/System/isabelle_process.scala|.  The protocol between
  the ML and JVM process is private to the implementation.

  \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{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}} setting) like this:
\begin{ttbox}
isabelle-process
\end{ttbox}

  Usually \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}} refers to one of the standard
  logic images, which are read-only by default.  A writable session
  --- based on \verb|HOL|, but output to \verb|Test| (in the
  directory specified by the \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} setting) ---
  may be invoked as follows:
\begin{ttbox}
isabelle-process HOL Test
\end{ttbox}
  Ending this session normally (e.g.\ by typing control-D) dumps the
  whole ML system state into \verb|Test| (be prepared for more
  than 100\,MB):

  The \verb|Test| session may be continued later (still in
  writable state) by:
\begin{ttbox}
isabelle-process Test
\end{ttbox}
  A read-only \verb|Test| session may be started by:
\begin{ttbox}
isabelle-process -r Test
\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|Main| theory value from the theory loader
  within ML (observe the delicate quoting rules for the Bash shell
  vs.\ ML):
\begin{ttbox}
isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
\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 tool NAME with ARGS; pass "-?" for tool 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{\isaliteral{5F}{\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 system
\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%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: