Merge.
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 a system oriented view. See also the
30 \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
31 the actual Isabelle input language and related concepts.
33 \medskip The Isabelle system environment provides the following
34 basic infrastructure to integrate tools smoothly.
38 \item The \emph{Isabelle settings} mechanism provides process
39 environment variables to all Isabelle executables (including tools
42 \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
43 batch mode. In particular, this view abstracts over the invocation
44 of the actual ML system to be used. Regular users rarely need to
45 care about the low-level process.
47 \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}})
48 provides a generic startup environment Isabelle related utilities,
49 user interfaces etc. Such tools automatically benefit from the
56 \isamarkupsection{Isabelle settings \label{sec:settings}%
60 \begin{isamarkuptext}%
61 The Isabelle system heavily depends on the \emph{settings
62 mechanism}\indexbold{settings}. Essentially, this is a statically
63 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
64 variables are \emph{not} intended to be set directly from the shell,
65 though. Isabelle employs a somewhat more sophisticated scheme of
66 \emph{settings files} --- one for site-wide defaults, another for
67 additional user-specific modifications. With all configuration
68 variables in at most two places, this scheme is more maintainable
69 and user-friendly than global shell environment variables.
71 In particular, we avoid the typical situation where prospective
72 users of a software package are told to put several things into
73 their shell startup scripts, before being able to actually run the
74 program. Isabelle requires none such administrative chores of its
75 end-users --- the executables can be invoked straight away.
76 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
77 this is not required.%
81 \isamarkupsubsection{Building the environment%
85 \begin{isamarkuptext}%
86 Whenever any of the Isabelle executables is run, their settings
87 environment is put together as follows.
91 \item The special variable \indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}} is
92 determined automatically from the location of the binary that has
95 You should not try to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} manually. Also
96 note that the Isabelle executables either have to be run from their
97 original location in the distribution directory, or via the
98 executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility. Symbolic
99 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!
101 \item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} ist run as a
102 \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for
105 This file holds a rather long list of shell variable assigments,
106 thus providing the site-wide default settings. The Isabelle
107 distribution already contains a global settings file with sensible
108 defaults for most variables. When installing the system, only a few
109 of these may have to be adapted (probably \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}
112 \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
113 exists) is run in the same way as the site default settings. Note
114 that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
115 before --- usually to \verb|~/.isabelle|.
117 Thus individual users may override the site-wide defaults. See also
118 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
119 distribution. Typically, a user settings file would contain only a
120 few lines, just the assigments that are really changed. One should
121 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
122 maintainance problems later, when the Isabelle installation is
123 updated or changed otherwise.
127 Since settings files are regular GNU \indexdef{}{executable}{bash}\hypertarget{executable.bash}{\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}}} scripts,
128 one may use complex shell commands, such as \verb|if| or
129 \verb|case| statements to set variables depending on the
130 system architecture or other environment variables. Such advanced
131 features should be added only with great care, though. In
132 particular, external environment references should be kept at a
135 \medskip A few variables are somewhat special:
139 \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
140 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,
143 \item \indexref{}{setting}{ISABELLE\_OUTPUT}\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} will have the identifiers of
144 the Isabelle distribution (cf.\ \hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}) and
145 the ML system (cf.\ \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}) appended automatically
150 \medskip Note that the settings environment may be inspected with
151 the Isabelle tool \hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}. This might help to figure out the
152 effect of complex settings scripts.%
156 \isamarkupsubsection{Common variables%
160 \begin{isamarkuptext}%
161 This is a reference of common Isabelle settings variables. Note that
162 the list is somewhat open-ended. Third-party utilities or interfaces
163 may add their own selection. Variables that are special in some
164 sense are marked with \isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}.
168 \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
169 location of the top-level Isabelle distribution directory. This is
170 automatically determined from the Isabelle executable that has been
171 invoked. Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} yourself
174 \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
175 counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
176 \verb|~/.isabelle|, under rare circumstances this may be
177 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
178 some extend. In particular, site-wide defaults may be overridden by
179 a private \verb|$ISABELLE_HOME_USER/etc/settings|.
181 \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
182 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
183 need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
184 on the current search path of the shell.
186 \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
187 to the name of this Isabelle distribution, e.g.\ ``\verb|Isabelle2008|''.
189 \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}}}}},
190 \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
191 to be used for Isabelle. There is only a fixed set of admissable
192 \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).
194 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
195 command line. The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} may specify the
196 binary format of ML heap images, which is useful for cross-platform
197 installations. The value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is
198 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.
200 \item[\indexdef{}{setting}{ISABELLE\_PATH}\hypertarget{setting.ISABELLE-PATH}{\hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}}}] is a list of directories
201 (separated by colons) where Isabelle logic images may reside. When
202 looking up heaps files, the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is
203 appended to each component internally.
205 \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
206 directory where output heap files should be stored by default. The
207 ML system and Isabelle version identifier is appended here, too.
209 \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
210 theory browser information (HTML text, graph data, and printable
211 documents) is stored (see also \secref{sec:info}). The default
212 value is \verb|$ISABELLE_HOME_USER/browser_info|.
214 \item[\indexdef{}{setting}{ISABELLE\_LOGIC}\hypertarget{setting.ISABELLE-LOGIC}{\hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}}}] specifies the default logic to
215 load if none is given explicitely by the user. The default value is
218 \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
219 line editor for the \indexref{}{tool}{tty}\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}} interface.
221 \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
222 to the command line of any \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} invocation. This
223 typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the
224 \verb|IsaMakefile|s in the distribution).
226 \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
227 for producing a source file identification, based on the actual
228 content instead of the full physical path and date stamp (which is
229 the default). A typical identification would produce a ``digest'' of
230 the text, using a cryptographic hash function like SHA-1, for
233 \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
234 document preparation (see also \secref{sec:tool-latex}).
236 \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
237 directories that are scanned by \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} for external
238 utility programs (see also \secref{sec:isabelle-tool}).
240 \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
241 directories with documentation files.
243 \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
244 document format, typically \verb|dvi| or \verb|pdf|.
246 \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
247 for displaying \verb|dvi| files.
249 \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
250 for displaying \verb|pdf| files.
252 \item[\indexdef{}{setting}{PRINT\_COMMAND}\hypertarget{setting.PRINT-COMMAND}{\hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isacharunderscore}COMMAND}}}}}] specifies the standard printer
253 spool command, which is expected to accept \verb|ps| files.
255 \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
256 prefix from which any running \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}
257 derives an individual directory for temporary files. The default is
258 somewhere in \verb|/tmp|.
264 \isamarkupsection{The raw Isabelle process%
268 \begin{isamarkuptext}%
269 The \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}} executable runs bare-bones
270 Isabelle logic sessions --- either interactively or in batch mode.
271 It provides an abstraction over the underlying ML system, and over
272 the actual heap file locations. Its usage is:
275 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
278 -C tell ML system to copy output image
279 -I startup Isar interaction mode
280 -P startup Proof General interaction mode
281 -S secure mode -- disallow critical operations
282 -W OUTPUT startup process wrapper, with messages going to OUTPUT stream
283 -X startup PGIP interaction mode
284 -c tell ML system to compress output image
285 -e MLTEXT pass MLTEXT to the ML session
286 -f pass 'Session.finish();' to the ML session
287 -m MODE add print mode for output
288 -q non-interactive session
289 -r open heap file read-only
290 -u pass 'use"ROOT.ML";' to the ML session
291 -w reset write permissions on OUTPUT
293 INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
294 These are either names to be searched in the Isabelle path, or
295 actual file names (containing at least one /).
296 If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
299 Input files without path specifications are looked up in the
300 \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}} setting, which may consist of multiple
301 components separated by colons --- these are tried in the given
302 order with the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} appended
303 internally. In a similar way, base names are relative to the
304 directory specified by \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}. In any case,
305 actual file locations may also be given by including at least one
306 slash (\verb|/|) in the name (hint: use \verb|./| to
307 refer to the current directory).%
311 \isamarkupsubsubsection{Options%
315 \begin{isamarkuptext}%
316 If the input heap file does not have write permission bits set, or
317 the \verb|-r| option is given explicitely, then the session
318 started will be read-only. That is, the ML world cannot be
319 committed back into the image file. Otherwise, a writable session
320 enables commits into either the input file, or into another output
321 heap file (if that is given as the second argument on the command
324 The read-write state of sessions is determined at startup only, it
325 cannot be changed intermediately. Also note that heap images may
326 require considerable amounts of disk space (approximately
327 50--200~MB). Users are responsible for themselves to dispose their
328 heap files when they are no longer needed.
330 \medskip The \verb|-w| option makes the output heap file
331 read-only after terminating. Thus subsequent invocations cause the
332 logic image to be read-only automatically.
334 \medskip The \verb|-c| option tells the underlying ML system
335 to compress the output heap (fully transparently). On Poly/ML for
336 example, the image is garbage collected and all stored values are
337 maximally shared, resulting in up to \isa{{\isachardoublequote}{\isadigit{5}}{\isadigit{0}}{\isacharpercent}{\isachardoublequote}} less disk space
340 \medskip The \verb|-C| option tells the ML system to produce
341 a completely self-contained output image, probably including a copy
342 of the ML runtime system itself.
344 \medskip Using the \verb|-e| option, arbitrary ML code may be
345 passed to the Isabelle session from the command line. Multiple
346 \verb|-e|'s are evaluated in the given order. Strange things
347 may happen when errorneous ML code is provided. Also make sure that
348 the ML commands are terminated properly by semicolon.
350 \medskip The \verb|-u| option is a shortcut for \verb|-e| passing ``\verb|use "ROOT.ML";|'' to the ML session.
351 The \verb|-f| option passes ``\verb|Session.finish();|'', which is intended mainly for administrative
354 \medskip The \verb|-m| option adds identifiers of print modes
355 to be made active for this session. Typically, this is used by some
356 user interface, e.g.\ to enable output of proper mathematical
359 \medskip Isabelle normally enters an interactive top-level loop
360 (after processing the \verb|-e| texts). The \verb|-q|
361 option inhibits interaction, thus providing a pure batch mode
364 \medskip The \verb|-I| option makes Isabelle enter Isar
365 interaction mode on startup, instead of the primitive ML top-level.
366 The \verb|-P| option configures the top-level loop for
367 interaction with the Proof General user interface, and the
368 \verb|-X| option enables XML-based PGIP communication. The
369 \verb|-W| option makes Isabelle enter a special process
370 wrapper for interaction via an external program; the protocol is a
371 stripped-down version of Proof General the interaction mode, see
372 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}}}}.
374 \medskip The \verb|-S| option makes the Isabelle process more
375 secure by disabling some critical operations, notably runtime
376 compilation and evaluation of ML source code.%
380 \isamarkupsubsubsection{Examples%
384 \begin{isamarkuptext}%
385 Run an interactive session of the default object-logic (as specified
386 by the \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} setting) like this:
391 Usually \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} refers to one of the standard
392 logic images, which are read-only by default. A writable session
393 --- based on \verb|FOL|, but output to \verb|Foo| (in the
394 directory specified by the \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} setting) ---
395 may be invoked as follows:
397 isabelle-process FOL Foo
399 Ending this session normally (e.g.\ by typing control-D) dumps the
400 whole ML system state into \verb|Foo|. Be prepared for several
403 The \verb|Foo| session may be continued later (still in
408 A read-only \verb|Foo| session may be started by:
410 isabelle-process -r Foo
413 \medskip Note that manual session management like this does
414 \emph{not} provide proper setup for theory presentation. This would
415 require the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
417 \bigskip The next example demonstrates batch execution of Isabelle.
418 We retrieve the \verb|FOL| theory value from the theory loader
421 isabelle-process -e 'theory "FOL";' -q -r FOL
423 Note that the output text will be interspersed with additional junk
424 messages by the ML runtime environment. The \verb|-W| option
425 allows to communicate with the Isabelle process via an external
426 program in a more robust fashion.%
430 \isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}%
434 \begin{isamarkuptext}%
435 All Isabelle related tools and interfaces are called via a common
436 wrapper --- \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}:
439 Usage: isabelle TOOL [ARGS ...]
441 Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
445 browser - Isabelle graph browser
449 In principle, Isabelle tools are ordinary executable scripts that
450 are run within the Isabelle settings environment, see
451 \secref{sec:settings}. The set of available tools is collected by
452 \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
453 from the shell. Neither should you add the tool directories to your
454 shell's search path!%
458 \isamarkupsubsubsection{Examples%
462 \begin{isamarkuptext}%
463 Show the list of available documentation of the current Isabelle
464 installation like this:
470 View a certain document as follows:
472 isabelle doc isar-ref
475 Create an Isabelle session derived from HOL (see also
476 \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
478 isabelle mkdir HOL Test && isabelle make
480 Note that \verb|isabelle mkdir| is usually only invoked once;
481 existing sessions (including document output etc.) are then updated
482 by \verb|isabelle make| alone.%
491 \isacommand{end}\isamarkupfalse%
502 %%% TeX-master: "root"