author wenzelm
Wed Sep 21 22:18:17 2011 +0200 (2011-09-21)
changeset 45028 d608dd8cd409
parent 43564 9864182c6bad
child 47661 012a887997f3
permissions -rw-r--r--
alternative Socket_Channel;
use BinIO for fifos uniformly;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Basics}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Basics\isanewline
    12 \isakeyword{imports}\ Base\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{The Isabelle system environment%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 This manual describes Isabelle together with related tools and user
    27   interfaces as seen from a system oriented view.  See also the
    28   \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
    29   the actual Isabelle input language and related concepts.
    31   \medskip The Isabelle system environment provides the following
    32   basic infrastructure to integrate tools smoothly.
    34   \begin{enumerate}
    36   \item The \emph{Isabelle settings} mechanism provides process
    37   environment variables to all Isabelle executables (including tools
    38   and user interfaces).
    40   \item The \emph{raw 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
    41   batch mode.  In particular, this view abstracts over the invocation
    42   of the actual ML system to be used.  Regular users rarely need to
    43   care about the low-level process.
    45   \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}})
    46   provides a generic startup environment Isabelle related utilities,
    47   user interfaces etc.  Such tools automatically benefit from the
    48   settings mechanism.
    50   \end{enumerate}%
    51 \end{isamarkuptext}%
    52 \isamarkuptrue%
    53 %
    54 \isamarkupsection{Isabelle settings \label{sec:settings}%
    55 }
    56 \isamarkuptrue%
    57 %
    58 \begin{isamarkuptext}%
    59 The Isabelle system heavily depends on the \emph{settings
    60   mechanism}\indexbold{settings}.  Essentially, this is a statically
    61   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
    62   variables are \emph{not} intended to be set directly from the shell,
    63   though.  Isabelle employs a somewhat more sophisticated scheme of
    64   \emph{settings files} --- one for site-wide defaults, another for
    65   additional user-specific modifications.  With all configuration
    66   variables in at most two places, this scheme is more maintainable
    67   and user-friendly than global shell environment variables.
    69   In particular, we avoid the typical situation where prospective
    70   users of a software package are told to put several things into
    71   their shell startup scripts, before being able to actually run the
    72   program. Isabelle requires none such administrative chores of its
    73   end-users --- the executables can be invoked straight away.
    74   Occasionally, users would still want to put the \verb|$ISABELLE_HOME/bin| directory into their shell's search path, but
    75   this is not required.%
    76 \end{isamarkuptext}%
    77 \isamarkuptrue%
    78 %
    79 \isamarkupsubsection{Bootstrapping the environment \label{sec:boot}%
    80 }
    81 \isamarkuptrue%
    82 %
    83 \begin{isamarkuptext}%
    84 Isabelle executables need to be run within a proper settings
    85   environment.  This is bootstrapped as described below, on the first
    86   invocation of one of the outer wrapper scripts (such as
    87   \indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}).  This happens only once for each
    88   process tree, i.e.\ the environment is passed to subprocesses
    89   according to regular Unix conventions.
    91   \begin{enumerate}
    93   \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
    94   determined automatically from the location of the binary that has
    95   been run.
    97   You should not try to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} manually. Also
    98   note that the Isabelle executables either have to be run from their
    99   original location in the distribution directory, or via the
   100   executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility.  Symbolic
   101   links are admissible, but a plain copy of the \verb|$ISABELLE_HOME/bin| files will not work!
   103   \item The file \verb|$ISABELLE_HOME/etc/settings| is run as a
   104   \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for
   105   variables enabled.
   107   This file holds a rather long list of shell variable assigments,
   108   thus providing the site-wide default settings.  The Isabelle
   109   distribution already contains a global settings file with sensible
   110   defaults for most variables.  When installing the system, only a few
   111   of these may have to be adapted (probably \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}
   112   etc.).
   114   \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
   115   exists) is run in the same way as the site default settings. Note
   116   that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} has already been set
   117   before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
   119   Thus individual users may override the site-wide defaults.  See also
   120   file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the
   121   distribution.  Typically, a user settings file would contain only a
   122   few lines, just the assigments that are really changed.  One should
   123   definitely \emph{not} start with a full copy the basic \verb|$ISABELLE_HOME/etc/settings|. This could cause very annoying
   124   maintainance problems later, when the Isabelle installation is
   125   updated or changed otherwise.
   127   \end{enumerate}
   129   Since settings files are regular GNU \indexdef{}{executable}{bash}\hypertarget{executable.bash}{\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}}} scripts,
   130   one may use complex shell commands, such as \verb|if| or
   131   \verb|case| statements to set variables depending on the
   132   system architecture or other environment variables.  Such advanced
   133   features should be added only with great care, though. In
   134   particular, external environment references should be kept at a
   135   minimum.
   137   \medskip A few variables are somewhat special:
   139   \begin{itemize}
   141   \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
   142   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,
   143   respectively.
   145   \item \indexref{}{setting}{ISABELLE\_OUTPUT}\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} will have the identifiers of
   146   the Isabelle distribution (cf.\ \hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}) and
   147   the ML system (cf.\ \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}) appended automatically
   148   to its value.
   150   \end{itemize}
   152   \medskip Note that the settings environment may be inspected with
   153   the Isabelle tool \hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}.  This might help to figure out the
   154   effect of complex settings scripts.%
   155 \end{isamarkuptext}%
   156 \isamarkuptrue%
   157 %
   158 \isamarkupsubsection{Common variables%
   159 }
   160 \isamarkuptrue%
   161 %
   162 \begin{isamarkuptext}%
   163 This is a reference of common Isabelle settings variables. Note that
   164   the list is somewhat open-ended. Third-party utilities or interfaces
   165   may add their own selection. Variables that are special in some
   166   sense are marked with \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}.
   168   \begin{description}
   170   \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
   171   location of the top-level Isabelle distribution directory. This is
   172   automatically determined from the Isabelle executable that has been
   173   invoked.  Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} yourself
   174   from the shell!
   176   \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
   177   counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}. The default value is
   178   relative to \verb|$HOME/.isabelle|, under rare circumstances
   179   this may be changed in the global setting file.  Typically, the
   180   \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
   181   be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
   183   \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
   184   set to a symbolic identifier for the underlying hardware and
   185   operating system.  The Isabelle platform identification always
   186   refers to the 32 bit variant, even this is a 64 bit machine.  Note
   187   that the ML or Java runtime may have a different idea, depending on
   188   which binaries are actually run.
   190   \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
   191   \hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} but refers to the proper 64 bit variant
   192   on a platform that supports this; the value is empty for 32 bit.
   194   \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
   195   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
   196   need not assume that the \verb|$ISABELLE_HOME/bin| directory is
   197   on the current search path of the shell.
   199   \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
   200   to the name of this Isabelle distribution, e.g.\ ``\verb|Isabelle2011|''.
   202   \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}}}}},
   203   \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
   204   to be used for Isabelle.  There is only a fixed set of admissable
   205   \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \verb|$ISABELLE_HOME/etc/settings| file of the distribution).
   207   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
   208   command line.  The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} may specify the
   209   binary format of ML heap images, which is useful for cross-platform
   210   installations.  The value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} is
   211   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.
   213   \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
   214   (separated by colons) where Isabelle logic images may reside.  When
   215   looking up heaps files, the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} is
   216   appended to each component internally.
   218   \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
   219   directory where output heap files should be stored by default. The
   220   ML system and Isabelle version identifier is appended here, too.
   222   \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
   223   theory browser information (HTML text, graph data, and printable
   224   documents) is stored (see also \secref{sec:info}).  The default
   225   value is \verb|$ISABELLE_HOME_USER/browser_info|.
   227   \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
   228   load if none is given explicitely by the user.  The default value is
   229   \verb|HOL|.
   231   \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
   232   line editor for the \indexref{}{tool}{tty}\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}} interface.
   234   \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
   235   to the command line of any \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} invocation. This
   236   typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the
   237   \verb|IsaMakefile|s in the distribution).
   239   \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
   240   document preparation (see also \secref{sec:tool-latex}).
   242   \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
   243   directories that are scanned by \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} for external
   244   utility programs (see also \secref{sec:isabelle-tool}).
   246   \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
   247   directories with documentation files.
   249   \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
   250   document format, typically \verb|dvi| or \verb|pdf|.
   252   \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
   253   for displaying \verb|dvi| files.
   255   \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
   256   for displaying \verb|pdf| files.
   258   \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
   259   spool command, which is expected to accept \verb|ps| files.
   261   \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
   262   prefix from which any running \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}
   263   derives an individual directory for temporary files.  The default is
   264   somewhere in \verb|/tmp|.
   266   \end{description}%
   267 \end{isamarkuptext}%
   268 \isamarkuptrue%
   269 %
   270 \isamarkupsubsection{Additional components \label{sec:components}%
   271 }
   272 \isamarkuptrue%
   273 %
   274 \begin{isamarkuptext}%
   275 Any directory may be registered as an explicit \emph{Isabelle
   276   component}.  The general layout conventions are that of the main
   277   Isabelle distribution itself, and the following two files (both
   278   optional) have a special meaning:
   280   \begin{itemize}
   282   \item \verb|etc/settings| holds additional settings that are
   283   initialized when bootstrapping the overall Isabelle environment,
   284   cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
   285   \verb|bash| script.  It may refer to the component's enclosing
   286   directory via the \verb|COMPONENT| shell variable.
   288   For example, the following setting allows to refer to files within
   289   the component later on, without having to hardwire absolute paths:
   291   \begin{ttbox}
   293   \end{ttbox}
   295   Components can also add to existing Isabelle settings such as
   296   \indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOLS}}}}}, in order to provide
   297   component-specific tools that can be invoked by end-users.  For
   298   example:
   300   \begin{ttbox}
   302   \end{ttbox}
   304   \item \verb|etc/components| holds a list of further
   305   sub-components of the same structure.  The directory specifications
   306   given here can be either absolute (with leading \verb|/|) or
   307   relative to the component's main directory.
   309   \end{itemize}
   311   The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
   312   itself.  After initializing all of its sub-components recursively,
   313   \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
   314   that directory exists).  This allows to install private components
   315   via \verb|$ISABELLE_HOME_USER/etc/components|, although it is
   316   often more convenient to do that programmatically via the
   317   \verb,init_component, shell function in the \verb,etc/settings,
   318   script of \verb,$ISABELLE_HOME_USER, (or any other component
   319   directory).  For example:
   320   \begin{verbatim}
   321   if [ -d "$HOME/screwdriver-2.0" ]
   322   then
   323     init_component "$HOME/screwdriver-2.0"
   324   else
   325   \end{verbatim}%
   326 \end{isamarkuptext}%
   327 \isamarkuptrue%
   328 %
   329 \isamarkupsection{The raw Isabelle process%
   330 }
   331 \isamarkuptrue%
   332 %
   333 \begin{isamarkuptext}%
   334 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
   335   Isabelle logic sessions --- either interactively or in batch mode.
   336   It provides an abstraction over the underlying ML system, and over
   337   the actual heap file locations.  Its usage is:
   339 \begin{ttbox}
   340 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
   342   Options are:
   343     -I           startup Isar interaction mode
   344     -P           startup Proof General interaction mode
   345     -S           secure mode -- disallow critical operations
   346     -T ADDR      startup process wrapper, with socket address
   347     -W IN:OUT    startup process wrapper, with input/output fifos
   348     -X           startup PGIP interaction mode
   349     -e MLTEXT    pass MLTEXT to the ML session
   350     -f           pass 'Session.finish();' to the ML session
   351     -m MODE      add print mode for output
   352     -q           non-interactive session
   353     -r           open heap file read-only
   354     -u           pass 'use"ROOT.ML";' to the ML session
   355     -w           reset write permissions on OUTPUT
   357   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
   358   These are either names to be searched in the Isabelle path, or
   359   actual file names (containing at least one /).
   360   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   361 \end{ttbox}
   363   Input files without path specifications are looked up in the
   364   \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}} setting, which may consist of multiple
   365   components separated by colons --- these are tried in the given
   366   order with the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} appended
   367   internally.  In a similar way, base names are relative to the
   368   directory specified by \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}}.  In any case,
   369   actual file locations may also be given by including at least one
   370   slash (\verb|/|) in the name (hint: use \verb|./| to
   371   refer to the current directory).%
   372 \end{isamarkuptext}%
   373 \isamarkuptrue%
   374 %
   375 \isamarkupsubsubsection{Options%
   376 }
   377 \isamarkuptrue%
   378 %
   379 \begin{isamarkuptext}%
   380 If the input heap file does not have write permission bits set, or
   381   the \verb|-r| option is given explicitely, then the session
   382   started will be read-only.  That is, the ML world cannot be
   383   committed back into the image file.  Otherwise, a writable session
   384   enables commits into either the input file, or into another output
   385   heap file (if that is given as the second argument on the command
   386   line).
   388   The read-write state of sessions is determined at startup only, it
   389   cannot be changed intermediately. Also note that heap images may
   390   require considerable amounts of disk space (approximately
   391   50--200~MB). Users are responsible for themselves to dispose their
   392   heap files when they are no longer needed.
   394   \medskip The \verb|-w| option makes the output heap file
   395   read-only after terminating.  Thus subsequent invocations cause the
   396   logic image to be read-only automatically.
   398   \medskip Using the \verb|-e| option, arbitrary ML code may be
   399   passed to the Isabelle session from the command line. Multiple
   400   \verb|-e|'s are evaluated in the given order. Strange things
   401   may happen when errorneous ML code is provided. Also make sure that
   402   the ML commands are terminated properly by semicolon.
   404   \medskip The \verb|-u| option is a shortcut for \verb|-e| passing ``\verb|use "ROOT.ML";|'' to the ML session.
   405   The \verb|-f| option passes ``\verb|Session.finish();|'', which is intended mainly for administrative
   406   purposes.
   408   \medskip The \verb|-m| option adds identifiers of print modes
   409   to be made active for this session. Typically, this is used by some
   410   user interface, e.g.\ to enable output of proper mathematical
   411   symbols.
   413   \medskip Isabelle normally enters an interactive top-level loop
   414   (after processing the \verb|-e| texts). The \verb|-q|
   415   option inhibits interaction, thus providing a pure batch mode
   416   facility.
   418   \medskip The \verb|-I| option makes Isabelle enter Isar
   419   interaction mode on startup, instead of the primitive ML top-level.
   420   The \verb|-P| option configures the top-level loop for
   421   interaction with the Proof General user interface, and the
   422   \verb|-X| option enables XML-based PGIP communication.
   424   \medskip The \verb|-T| or \verb|-W| option makes
   425   Isabelle enter a special process wrapper for interaction via the
   426   Isabelle/Scala layer, see also \verb|~~/src/Pure/System/isabelle_process.scala|.  The protocol between
   427   the ML and JVM process is private to the implementation.
   429   \medskip The \verb|-S| option makes the Isabelle process more
   430   secure by disabling some critical operations, notably runtime
   431   compilation and evaluation of ML source code.%
   432 \end{isamarkuptext}%
   433 \isamarkuptrue%
   434 %
   435 \isamarkupsubsubsection{Examples%
   436 }
   437 \isamarkuptrue%
   438 %
   439 \begin{isamarkuptext}%
   440 Run an interactive session of the default object-logic (as specified
   441   by the \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}} setting) like this:
   442 \begin{ttbox}
   443 isabelle-process
   444 \end{ttbox}
   446   Usually \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}LOGIC}}}} refers to one of the standard
   447   logic images, which are read-only by default.  A writable session
   448   --- based on \verb|FOL|, but output to \verb|Foo| (in the
   449   directory specified by the \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} setting) ---
   450   may be invoked as follows:
   451 \begin{ttbox}
   452 isabelle-process FOL Foo
   453 \end{ttbox}
   454   Ending this session normally (e.g.\ by typing control-D) dumps the
   455   whole ML system state into \verb|Foo|. Be prepared for several
   456   tens of megabytes.
   458   The \verb|Foo| session may be continued later (still in
   459   writable state) by:
   460 \begin{ttbox}
   461 isabelle-process Foo
   462 \end{ttbox}
   463   A read-only \verb|Foo| session may be started by:
   464 \begin{ttbox}
   465 isabelle-process -r Foo
   466 \end{ttbox}
   468   \medskip Note that manual session management like this does
   469   \emph{not} provide proper setup for theory presentation.  This would
   470   require the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
   472   \bigskip The next example demonstrates batch execution of Isabelle.
   473   We retrieve the \verb|FOL| theory value from the theory loader
   474   within ML:
   475 \begin{ttbox}
   476 isabelle-process -e 'theory "FOL";' -q -r FOL
   477 \end{ttbox}
   478   Note that the output text will be interspersed with additional junk
   479   messages by the ML runtime environment.  The \verb|-W| option
   480   allows to communicate with the Isabelle process via an external
   481   program in a more robust fashion.%
   482 \end{isamarkuptext}%
   483 \isamarkuptrue%
   484 %
   485 \isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}%
   486 }
   487 \isamarkuptrue%
   488 %
   489 \begin{isamarkuptext}%
   490 All Isabelle related tools and interfaces are called via a common
   491   wrapper --- \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}:
   493 \begin{ttbox}
   494 Usage: isabelle TOOL [ARGS ...]
   496   Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   498   Available tools are:
   500     browser - Isabelle graph browser
   501     \dots
   502 \end{ttbox}
   504   In principle, Isabelle tools are ordinary executable scripts that
   505   are run within the Isabelle settings environment, see
   506   \secref{sec:settings}.  The set of available tools is collected by
   507   \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
   508   from the shell.  Neither should you add the tool directories to your
   509   shell's search path!%
   510 \end{isamarkuptext}%
   511 \isamarkuptrue%
   512 %
   513 \isamarkupsubsubsection{Examples%
   514 }
   515 \isamarkuptrue%
   516 %
   517 \begin{isamarkuptext}%
   518 Show the list of available documentation of the current Isabelle
   519   installation like this:
   521 \begin{ttbox}
   522   isabelle doc
   523 \end{ttbox}
   525   View a certain document as follows:
   526 \begin{ttbox}
   527   isabelle doc isar-ref
   528 \end{ttbox}
   530   Create an Isabelle session derived from HOL (see also
   531   \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
   532 \begin{ttbox}
   533   isabelle mkdir HOL Test && isabelle make
   534 \end{ttbox}
   535   Note that \verb|isabelle mkdir| is usually only invoked once;
   536   existing sessions (including document output etc.) are then updated
   537   by \verb|isabelle make| alone.%
   538 \end{isamarkuptext}%
   539 \isamarkuptrue%
   540 %
   541 \isadelimtheory
   542 %
   543 \endisadelimtheory
   544 %
   545 \isatagtheory
   546 \isacommand{end}\isamarkupfalse%
   547 %
   548 \endisatagtheory
   549 {\isafoldtheory}%
   550 %
   551 \isadelimtheory
   552 %
   553 \endisadelimtheory
   554 \end{isabellebody}%
   555 %%% Local Variables:
   556 %%% mode: latex
   557 %%% TeX-master: "root"
   558 %%% End: