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