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