doc-src/System/Thy/document/Basics.tex
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.
    30 
    31   \medskip The Isabelle system environment provides the following
    32   basic infrastructure to integrate tools smoothly.
    33 
    34   \begin{enumerate}
    35 
    36   \item The \emph{Isabelle settings} mechanism provides process
    37   environment variables to all Isabelle executables (including tools
    38   and user interfaces).
    39 
    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.
    44 
    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.
    49 
    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.
    68 
    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.
    90 
    91   \begin{enumerate}
    92 
    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.
    96   
    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!
   102 
   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.
   106   
   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.).
   113   
   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|.
   118   
   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.
   126   
   127   \end{enumerate}
   128 
   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.
   136 
   137   \medskip A few variables are somewhat special:
   138 
   139   \begin{itemize}
   140 
   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.
   144   
   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.
   149 
   150   \end{itemize}
   151 
   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}}}.
   167 
   168   \begin{description}
   169 
   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!
   175   
   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|.
   182   
   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.
   189 
   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.
   193 
   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.
   198   
   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|''.
   201 
   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).
   206   
   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.
   212   
   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.
   217   
   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.
   221   
   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|.
   226   
   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|.
   230   
   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.
   233 
   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).
   238 
   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}).
   241   
   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}).
   245   
   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.
   248   
   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|.
   251   
   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.
   254   
   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.
   257   
   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.
   260   
   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|.
   265   
   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:
   279 
   280   \begin{itemize}
   281 
   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.
   287 
   288   For example, the following setting allows to refer to files within
   289   the component later on, without having to hardwire absolute paths:
   290 
   291   \begin{ttbox}
   292   MY_COMPONENT_HOME="$COMPONENT"
   293   \end{ttbox}
   294 
   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:
   299 
   300   \begin{ttbox}
   301   ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
   302   \end{ttbox}
   303 
   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.
   308 
   309   \end{itemize}
   310 
   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:
   338 
   339 \begin{ttbox}
   340 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
   341 
   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
   356 
   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}
   362 
   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).
   387 
   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.
   393 
   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.
   397 
   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.
   403 
   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.
   407 
   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.
   412 
   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.
   417 
   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.
   423 
   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.
   428 
   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}
   445 
   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.
   457 
   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}
   467 
   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.
   471 
   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}}}}:
   492 
   493 \begin{ttbox}
   494 Usage: isabelle TOOL [ARGS ...]
   495 
   496   Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   497 
   498   Available tools are:
   499 
   500     browser - Isabelle graph browser
   501     \dots
   502 \end{ttbox}
   503 
   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:
   520 
   521 \begin{ttbox}
   522   isabelle doc
   523 \end{ttbox}
   524 
   525   View a certain document as follows:
   526 \begin{ttbox}
   527   isabelle doc isar-ref
   528 \end{ttbox}
   529 
   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: