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