3 \def\isabellecontext{Basics}%
12 \isacommand{theory}\isamarkupfalse%
14 \isakeyword{imports}\ Pure\isanewline
23 \isamarkupchapter{The Isabelle system environment%
27 \begin{isamarkuptext}%
28 This manual describes Isabelle together with related tools and user
29 interfaces as seen from an outside (system oriented) view. See also
30 the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
31 and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
32 actual Isabelle commands and related functions.
34 \medskip The Isabelle system environment emerges from a few general
39 \item The \emph{Isabelle settings} mechanism provides environment
40 variables to all Isabelle programs (including tools and user
43 \item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} or
44 \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) runs logic sessions either
45 interactively or in batch mode. In particular, this view abstracts
46 over the invocation of the actual ML system to be used. Regular
47 users rarely need to care about the low-level process.
49 \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isatool}\hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}})
50 provides a generic startup environment Isabelle related utilities,
51 user interfaces etc. Such tools automatically benefit from the
54 \item The \emph{Isabelle interface wrapper} (\indexref{}{executable}{Isabelle}\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} or \indexref{}{executable}{isabelle-interface}\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}) provides some
55 abstraction over the actual user interface to be used. The de-facto
56 standard interface for Isabelle is Proof~General
63 \isamarkupsection{Isabelle settings \label{sec:settings}%
67 \begin{isamarkuptext}%
68 The Isabelle system heavily depends on the \emph{settings
69 mechanism}\indexbold{settings}. Essentially, this is a statically
70 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
71 variables are \emph{not} intended to be set directly from the shell,
72 though. Isabelle employs a somewhat more sophisticated scheme of
73 \emph{settings files} --- one for site-wide defaults, another for
74 additional user-specific modifications. With all configuration
75 variables in at most two places, this scheme is more maintainable
76 and user-friendly than global shell environment variables.
78 In particular, we avoid the typical situation where prospective
79 users of a software package are told to put several things into
80 their shell startup scripts, before being able to actually run the
81 program. Isabelle requires none such administrative chores of its
82 end-users --- the executables can be invoked straight away.
83 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
84 this is not required.%
88 \isamarkupsubsection{Building the environment%
92 \begin{isamarkuptext}%
93 Whenever any of the Isabelle executables is run, their settings
94 environment is put together as follows.
98 \item The special variable \indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}} is
99 determined automatically from the location of the binary that has
102 You should not try to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} manually. Also
103 note that the Isabelle executables either have to be run from their
104 original location in the distribution directory, or via the
105 executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility. Symbolic
106 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!
108 \item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} ist run as a
109 \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for
112 This file holds a rather long list of shell variable assigments,
113 thus providing the site-wide default settings. The Isabelle
114 distribution already contains a global settings file with sensible
115 defaults for most variables. When installing the system, only a few
116 of these may have to be adapted (probably \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}
119 \item The file \hyperlink{file.$ISABELLE-HOME-USER/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER{\isacharslash}etc{\isacharslash}settings}}}} (if it
120 exists) is run in the same way as the site default settings. Note
121 that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
122 before --- usually to \verb|~/isabelle|.
124 Thus individual users may override the site-wide defaults. See also
125 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
126 distribution. Typically, a user settings file would contain only a
127 few lines, just the assigments that are really changed. One should
128 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
129 maintainance problems later, when the Isabelle installation is
130 updated or changed otherwise.
134 Since settings files are regular GNU \indexdef{}{executable}{bash}\hypertarget{executable.bash}{\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}}} scripts,
135 one may use complex shell commands, such as \verb|if| or
136 \verb|case| statements to set variables depending on the
137 system architecture or other environment variables. Such advanced
138 features should be added only with great care, though. In
139 particular, external environment references should be kept at a
142 \medskip A few variables are somewhat special:
146 \item \indexdef{}{setting}{ISABELLE}\hypertarget{setting.ISABELLE}{\hyperlink{setting.ISABELLE}{\mbox{\isa{\isatt{ISABELLE}}}}} and \indexdef{}{setting}{ISATOOL}\hypertarget{setting.ISATOOL}{\hyperlink{setting.ISATOOL}{\mbox{\isa{\isatt{ISATOOL}}}}} are set
147 automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables,
150 \item \indexref{}{setting}{ISABELLE\_OUTPUT}\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} will have the identifiers of
151 the Isabelle distribution (cf.\ \hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}) and
152 the ML system (cf.\ \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}) appended automatically
157 \medskip Note that the settings environment may be inspected with
158 the Isabelle tool \hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}. This might help to figure out the
159 effect of complex settings scripts.%
163 \isamarkupsubsection{Common variables%
167 \begin{isamarkuptext}%
168 This is a reference of common Isabelle settings variables. Note that
169 the list is somewhat open-ended. Third-party utilities or interfaces
170 may add their own selection. Variables that are special in some
171 sense are marked with \isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}.
175 \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
176 location of the top-level Isabelle distribution directory. This is
177 automatically determined from the Isabelle executable that has been
178 invoked. Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} yourself
181 \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
182 counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
183 \verb|~/isabelle|, under rare circumstances this may be
184 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
185 some extend. In particular, site-wide defaults may be overridden by
186 a private \hyperlink{file.$ISABELLE-HOME-USER/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER{\isacharslash}etc{\isacharslash}settings}}}}.
188 \item[\indexdef{}{setting}{ISABELLE}\hypertarget{setting.ISABELLE}{\hyperlink{setting.ISABELLE}{\mbox{\isa{\isatt{ISABELLE}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISATOOL}{\mbox{\isa{\isatt{ISATOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
189 names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables, respectively. Thus other tools and scripts
190 need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
191 on the current search path of the shell.
193 \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
194 to the name of this Isabelle distribution, e.g.\ ``\verb|Isabelle2008|''.
196 \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}}}}},
197 \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
198 to be used for Isabelle. There is only a fixed set of admissable
199 \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).
201 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
202 command line. The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} may specify the
203 binary format of ML heap images, which is useful for cross-platform
204 installations. The value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is
205 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.
207 \item[\indexdef{}{setting}{ISABELLE\_PATH}\hypertarget{setting.ISABELLE-PATH}{\hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}}}] is a list of directories
208 (separated by colons) where Isabelle logic images may reside. When
209 looking up heaps files, the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is
210 appended to each component internally.
212 \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
213 directory where output heap files should be stored by default. The
214 ML system and Isabelle version identifier is appended here, too.
216 \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
217 theory browser information (HTML text, graph data, and printable
218 documents) is stored (see also \secref{sec:info}). The default
219 value is \verb|$ISABELLE_HOME_USER/browser_info|.
221 \item[\indexdef{}{setting}{ISABELLE\_LOGIC}\hypertarget{setting.ISABELLE-LOGIC}{\hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}}}] specifies the default logic to
222 load if none is given explicitely by the user. The default value is
225 \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
226 line editor for the \indexref{}{tool}{tty}\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}} interface.
228 \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
229 to the command line of any \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} invocation. This
230 typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the
231 \verb|IsaMakefile|s in the distribution).
233 \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
234 for producing a source file identification, based on the actual
235 content instead of the full physical path and date stamp (which is
236 the default). A typical identification would produce a ``digest'' of
237 the text, using a cryptographic hash function like SHA-1, for
240 \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
241 document preparation (see also \secref{sec:tool-latex}).
243 \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
244 directories that are scanned by \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} for external
245 utility programs (see also \secref{sec:isatool}).
247 \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
248 directories with documentation files.
250 \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
251 document format, typically \verb|dvi| or \verb|pdf|.
253 \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
254 for displaying \verb|dvi| files.
256 \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
257 for displaying \verb|pdf| files.
259 \item[\indexdef{}{setting}{PRINT\_COMMAND}\hypertarget{setting.PRINT-COMMAND}{\hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isacharunderscore}COMMAND}}}}}] specifies the standard printer
260 spool command, which is expected to accept \verb|ps| files.
262 \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
263 prefix from which any running \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}
264 derives an individual directory for temporary files. The default is
265 somewhere in \verb|/tmp|.
267 \item[\indexdef{}{setting}{ISABELLE\_INTERFACE}\hypertarget{setting.ISABELLE-INTERFACE}{\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}}}] is an identifier that
268 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
269 \secref{sec:interface} for more details.
275 \isamarkupsection{The raw Isabelle process%
279 \begin{isamarkuptext}%
280 The \indexdef{}{executable}{isabelle}\hypertarget{executable.isabelle}{\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}} (or \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}}) executable runs bare-bones Isabelle logic
281 sessions --- either interactively or in batch mode. It provides an
282 abstraction over the underlying ML system, and over the actual heap
283 file locations. Its usage is:
286 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
289 -C tell ML system to copy output image
290 -I startup Isar interaction mode
291 -P startup Proof General interaction mode
292 -S secure mode -- disallow critical operations
293 -W OUTPUT startup process wrapper, with messages going to OUTPUT stream
294 -X startup PGIP interaction mode
295 -c tell ML system to compress output image
296 -e MLTEXT pass MLTEXT to the ML session
297 -f pass 'Session.finish();' to the ML session
298 -m MODE add print mode for output
299 -q non-interactive session
300 -r open heap file read-only
301 -u pass 'use"ROOT.ML";' to the ML session
302 -w reset write permissions on OUTPUT
304 INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
305 These are either names to be searched in the Isabelle path, or
306 actual file names (containing at least one /).
307 If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
310 Input files without path specifications are looked up in the
311 \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}} setting, which may consist of multiple
312 components separated by colons --- these are tried in the given
313 order with the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} appended
314 internally. In a similar way, base names are relative to the
315 directory specified by \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}. In any case,
316 actual file locations may also be given by including at least one
317 slash (\verb|/|) in the name (hint: use \verb|./| to
318 refer to the current directory).%
322 \isamarkupsubsubsection{Options%
326 \begin{isamarkuptext}%
327 If the input heap file does not have write permission bits set, or
328 the \verb|-r| option is given explicitely, then the session
329 started will be read-only. That is, the ML world cannot be
330 committed back into the image file. Otherwise, a writable session
331 enables commits into either the input file, or into another output
332 heap file (if that is given as the second argument on the command
335 The read-write state of sessions is determined at startup only, it
336 cannot be changed intermediately. Also note that heap images may
337 require considerable amounts of disk space (approximately
338 50--200~MB). Users are responsible for themselves to dispose their
339 heap files when they are no longer needed.
341 \medskip The \verb|-w| option makes the output heap file
342 read-only after terminating. Thus subsequent invocations cause the
343 logic image to be read-only automatically.
345 \medskip The \verb|-c| option tells the underlying ML system
346 to compress the output heap (fully transparently). On Poly/ML for
347 example, the image is garbage collected and all stored values are
348 maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
351 \medskip The \verb|-C| option tells the ML system to produce
352 a completely self-contained output image, probably including a copy
353 of the ML runtime system itself.
355 \medskip Using the \verb|-e| option, arbitrary ML code may be
356 passed to the Isabelle session from the command line. Multiple
357 \verb|-e|'s are evaluated in the given order. Strange things
358 may happen when errorneous ML code is provided. Also make sure that
359 the ML commands are terminated properly by semicolon.
361 \medskip The \verb|-u| option is a shortcut for \verb|-e| passing ``\verb|use "ROOT.ML";|'' to the ML session.
362 The \verb|-f| option passes ``\verb|Session.finish();|'', which is intended mainly for administrative
365 \medskip The \verb|-m| option adds identifiers of print modes
366 to be made active for this session. Typically, this is used by some
367 user interface, e.g.\ to enable output of proper mathematical
370 \medskip Isabelle normally enters an interactive top-level loop
371 (after processing the \verb|-e| texts). The \verb|-q|
372 option inhibits interaction, thus providing a pure batch mode
375 \medskip The \verb|-I| option makes Isabelle enter Isar
376 interaction mode on startup, instead of the primitive ML top-level.
377 The \verb|-P| option configures the top-level loop for
378 interaction with the Proof General user interface, and the
379 \verb|-X| option enables XML-based PGIP communication. The
380 \verb|-W| option makes Isabelle enter a special process
381 wrapper for interaction via an external program; the protocol is a
382 stripped-down version of Proof General the interaction mode, see
383 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}}}}.
385 \medskip The \verb|-S| option makes the Isabelle process more
386 secure by disabling some critical operations, notably runtime
387 compilation and evaluation of ML source code.%
391 \isamarkupsubsubsection{Examples%
395 \begin{isamarkuptext}%
396 Run an interactive session of the default object-logic (as specified
397 by the \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} setting) like this:
402 Usually \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} refers to one of the standard
403 logic images, which are read-only by default. A writable session
404 --- based on \verb|FOL|, but output to \verb|Foo| (in the
405 directory specified by the \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} setting) ---
406 may be invoked as follows:
408 isabelle-process FOL Foo
410 Ending this session normally (e.g.\ by typing control-D) dumps the
411 whole ML system state into \verb|Foo|. Be prepared for several
414 The \verb|Foo| session may be continued later (still in
419 A read-only \verb|Foo| session may be started by:
421 isabelle-process -r Foo
424 \medskip Note that manual session management like this does
425 \emph{not} provide proper setup for theory presentation. This would
426 require the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
428 \bigskip The next example demonstrates batch execution of Isabelle.
429 We retrieve the \verb|FOL| theory value from the theory loader
432 isabelle-process -e 'theory "FOL";' -q -r FOL
434 Note that the output text will be interspersed with additional junk
435 messages by the ML runtime environment. The \verb|-W| option
436 allows to communicate with the Isabelle process via an external
437 program in a more robust fashion.%
441 \isamarkupsection{The Isabelle tools wrapper \label{sec:isatool}%
445 \begin{isamarkuptext}%
446 All Isabelle related tools and interfaces are called via a common
447 wrapper --- \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}}:
450 Usage: isatool TOOL [ARGS ...]
452 Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
453 for more specific help.
457 browser - Isabelle graph browser
461 In principle, Isabelle tools are ordinary executable scripts that
462 are run within the Isabelle settings environment, see
463 \secref{sec:settings}. The set of available tools is collected by
464 \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} 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
465 from the shell. Neither should you add the tool directories to your
466 shell's search path!%
470 \isamarkupsubsubsection{Examples%
474 \begin{isamarkuptext}%
475 Show the list of available documentation of the current Isabelle
476 installation like this:
482 View a certain document as follows:
487 Create an Isabelle session derived from HOL (see also
488 \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
490 isatool mkdir HOL Test && isatool make
492 Note that \verb|isatool mkdir| is usually only invoked once;
493 existing sessions (including document output etc.) are then updated
494 by \verb|isatool make| alone.%
498 \isamarkupsection{The Isabelle interface wrapper \label{sec:interface}%
502 \begin{isamarkuptext}%
503 Isabelle is a generic theorem prover, even w.r.t.\ its user
504 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
505 end-users to invoke a certain interface; which one to start is
506 determined by the \indexref{}{setting}{ISABELLE\_INTERFACE}\hyperlink{setting.ISABELLE-INTERFACE}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}INTERFACE}}}} setting
507 variable, which should give a full path specification to the actual
510 Presently, the most prominent Isabelle interface is Proof
511 General~\cite{proofgeneral}\index{user interface!Proof General}.
512 The Proof General distribution includes an interface wrapper script
513 for the regular Isar toplevel, see \verb|ProofGeneral/isar/interface|. The canonical settings for
514 Isabelle/Isar are as follows:
517 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
518 PROOFGENERAL_OPTIONS=""
521 Thus \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} would automatically invoke Emacs with
522 proper setup of the Proof General Lisp packages. There are some
523 options available, such as \verb|-l| for passing the logic
524 image to be used by default, or \verb|-m| to tune the
527 \medskip Note that the world may be also seen the other way round:
528 Emacs may be started first (with proper setup of Proof General
529 mode), and \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} run from within. This
530 requires further Emacs Lisp configuration, see the Proof General
531 documentation \cite{proofgeneral} for more information.%
540 \isacommand{end}\isamarkupfalse%
551 %%% TeX-master: "root"