7 chapter {* The Isabelle system environment *}
10 This manual describes Isabelle together with related tools and user
11 interfaces as seen from an outside (system oriented) view. See also
12 the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
13 and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
14 actual Isabelle commands and related functions.
16 \medskip The Isabelle system environment emerges from a few general
21 \item The \emph{Isabelle settings} mechanism provides environment
22 variables to all Isabelle programs (including tools and user
25 \item The \emph{raw Isabelle process} (@{executable_ref isabelle} or
26 @{executable_ref "isabelle-process"}) runs logic sessions either
27 interactively or in batch mode. In particular, this view abstracts
28 over the invocation of the actual ML system to be used. Regular
29 users rarely need to care about the low-level process.
31 \item The \emph{Isabelle tools wrapper} (@{executable_ref isatool})
32 provides a generic startup environment Isabelle related utilities,
33 user interfaces etc. Such tools automatically benefit from the
36 \item The \emph{Isabelle interface wrapper} (@{executable_ref
37 Isabelle} or @{executable_ref "isabelle-interface"}) provides some
38 abstraction over the actual user interface to be used. The de-facto
39 standard interface for Isabelle is Proof~General
46 section {* Isabelle settings \label{sec:settings} *}
49 The Isabelle system heavily depends on the \emph{settings
50 mechanism}\indexbold{settings}. Essentially, this is a statically
51 scoped collection of environment variables, such as @{setting
52 ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}. These
53 variables are \emph{not} intended to be set directly from the shell,
54 though. Isabelle employs a somewhat more sophisticated scheme of
55 \emph{settings files} --- one for site-wide defaults, another for
56 additional user-specific modifications. With all configuration
57 variables in at most two places, this scheme is more maintainable
58 and user-friendly than global shell environment variables.
60 In particular, we avoid the typical situation where prospective
61 users of a software package are told to put several things into
62 their shell startup scripts, before being able to actually run the
63 program. Isabelle requires none such administrative chores of its
64 end-users --- the executables can be invoked straight away.
65 Occasionally, users would still want to put the @{"file"
66 "$ISABELLE_HOME/bin"} directory into their shell's search path, but
71 subsection {* Building the environment *}
74 Whenever any of the Isabelle executables is run, their settings
75 environment is put together as follows.
79 \item The special variable @{setting_def ISABELLE_HOME} is
80 determined automatically from the location of the binary that has
83 You should not try to set @{setting ISABELLE_HOME} manually. Also
84 note that the Isabelle executables either have to be run from their
85 original location in the distribution directory, or via the
86 executable objects created by the @{tool install} utility. Symbolic
87 links are admissible, but a plain copy of the @{"file"
88 "$ISABELLE_HOME/bin"} files will not work!
90 \item The file @{"file" "$ISABELLE_HOME/etc/settings"} ist run as a
91 @{executable_ref bash} shell script with the auto-export option for
94 This file holds a rather long list of shell variable assigments,
95 thus providing the site-wide default settings. The Isabelle
96 distribution already contains a global settings file with sensible
97 defaults for most variables. When installing the system, only a few
98 of these may have to be adapted (probably @{setting ML_SYSTEM}
101 \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
102 exists) is run in the same way as the site default settings. Note
103 that the variable @{setting ISABELLE_HOME_USER} has already been set
104 before --- usually to @{verbatim "~/isabelle"}.
106 Thus individual users may override the site-wide defaults. See also
107 file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
108 distribution. Typically, a user settings file would contain only a
109 few lines, just the assigments that are really changed. One should
110 definitely \emph{not} start with a full copy the basic @{"file"
111 "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
112 maintainance problems later, when the Isabelle installation is
113 updated or changed otherwise.
117 Since settings files are regular GNU @{executable_def bash} scripts,
118 one may use complex shell commands, such as @{verbatim "if"} or
119 @{verbatim "case"} statements to set variables depending on the
120 system architecture or other environment variables. Such advanced
121 features should be added only with great care, though. In
122 particular, external environment references should be kept at a
125 \medskip A few variables are somewhat special:
129 \item @{setting_def ISABELLE} and @{setting_def ISATOOL} are set
130 automatically to the absolute path names of the @{executable
131 "isabelle-process"} and @{executable isatool} executables,
134 \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
135 the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
136 the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
141 \medskip Note that the settings environment may be inspected with
142 the Isabelle tool @{tool getenv}. This might help to figure out the
143 effect of complex settings scripts.
147 subsection{* Common variables *}
150 This is a reference of common Isabelle settings variables. Note that
151 the list is somewhat open-ended. Third-party utilities or interfaces
152 may add their own selection. Variables that are special in some
153 sense are marked with @{text "\<^sup>*"}.
157 \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
158 location of the top-level Isabelle distribution directory. This is
159 automatically determined from the Isabelle executable that has been
160 invoked. Do not attempt to set @{setting ISABELLE_HOME} yourself
163 \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
164 counterpart of @{setting ISABELLE_HOME}. The default value is
165 @{verbatim "~/isabelle"}, under rare circumstances this may be
166 changed in the global setting file. Typically, the @{setting
167 ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
168 some extend. In particular, site-wide defaults may be overridden by
169 a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
171 \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting
172 ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path
173 names of the @{executable "isabelle-process"} and @{executable
174 isatool} executables, respectively. Thus other tools and scripts
175 need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is
176 on the current search path of the shell.
178 \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
179 to the name of this Isabelle distribution, e.g.\ ``@{verbatim
182 \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
183 @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
184 ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
185 to be used for Isabelle. There is only a fixed set of admissable
186 @{setting ML_SYSTEM} names (see the @{"file"
187 "$ISABELLE_HOME/etc/settings"} file of the distribution).
189 The actual compiler binary will be run from the directory @{setting
190 ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
191 command line. The optional @{setting ML_PLATFORM} may specify the
192 binary format of ML heap images, which is useful for cross-platform
193 installations. The value of @{setting ML_IDENTIFIER} is
194 automatically obtained by composing the values of @{setting
195 ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
197 \item[@{setting_def ISABELLE_PATH}] is a list of directories
198 (separated by colons) where Isabelle logic images may reside. When
199 looking up heaps files, the value of @{setting ML_IDENTIFIER} is
200 appended to each component internally.
202 \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
203 directory where output heap files should be stored by default. The
204 ML system and Isabelle version identifier is appended here, too.
206 \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
207 theory browser information (HTML text, graph data, and printable
208 documents) is stored (see also \secref{sec:info}). The default
209 value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
211 \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
212 load if none is given explicitely by the user. The default value is
215 \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
216 line editor for the @{tool_ref tty} interface.
218 \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
219 to the command line of any @{tool_ref usedir} invocation. This
220 typically contains compilation options for object-logics --- @{tool
221 usedir} is the basic utility for managing logic sessions (cf.\ the
222 @{verbatim IsaMakefile}s in the distribution).
224 \item[@{setting_def ISABELLE_FILE_IDENT}] specifies a shell command
225 for producing a source file identification, based on the actual
226 content instead of the full physical path and date stamp (which is
227 the default). A typical identification would produce a ``digest'' of
228 the text, using a cryptographic hash function like SHA-1, for
231 \item[@{setting_def ISABELLE_LATEX}, @{setting_def
232 ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
233 ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
234 document preparation (see also \secref{sec:tool-latex}).
236 \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
237 directories that are scanned by @{executable isatool} for external
238 utility programs (see also \secref{sec:isatool}).
240 \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
241 directories with documentation files.
243 \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
244 document format, typically @{verbatim dvi} or @{verbatim pdf}.
246 \item[@{setting_def DVI_VIEWER}] specifies the command to be used
247 for displaying @{verbatim dvi} files.
249 \item[@{setting_def PDF_VIEWER}] specifies the command to be used
250 for displaying @{verbatim pdf} files.
252 \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
253 spool command, which is expected to accept @{verbatim ps} files.
255 \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
256 prefix from which any running @{executable "isabelle-process"}
257 derives an individual directory for temporary files. The default is
258 somewhere in @{verbatim "/tmp"}.
260 \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
261 specifies the actual user interface that the capital @{executable
262 Isabelle} or @{executable "isabelle-interface"} should invoke. See
263 \secref{sec:interface} for more details.
269 section {* The raw Isabelle process *}
272 The @{executable_def isabelle} (or @{executable_def
273 "isabelle-process"}) executable runs bare-bones Isabelle logic
274 sessions --- either interactively or in batch mode. It provides an
275 abstraction over the underlying ML system, and over the actual heap
276 file locations. Its usage is:
279 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
282 -C tell ML system to copy output image
283 -I startup Isar interaction mode
284 -P startup Proof General interaction mode
285 -S secure mode -- disallow critical operations
286 -W OUTPUT startup process wrapper, with messages going to OUTPUT stream
287 -X startup PGIP interaction mode
288 -c tell ML system to compress output image
289 -e MLTEXT pass MLTEXT to the ML session
290 -f pass 'Session.finish();' to the ML session
291 -m MODE add print mode for output
292 -q non-interactive session
293 -r open heap file read-only
294 -u pass 'use"ROOT.ML";' to the ML session
295 -w reset write permissions on OUTPUT
297 INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
298 These are either names to be searched in the Isabelle path, or
299 actual file names (containing at least one /).
300 If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
303 Input files without path specifications are looked up in the
304 @{setting ISABELLE_PATH} setting, which may consist of multiple
305 components separated by colons --- these are tried in the given
306 order with the value of @{setting ML_IDENTIFIER} appended
307 internally. In a similar way, base names are relative to the
308 directory specified by @{setting ISABELLE_OUTPUT}. In any case,
309 actual file locations may also be given by including at least one
310 slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
311 refer to the current directory).
315 subsubsection {* Options *}
318 If the input heap file does not have write permission bits set, or
319 the @{verbatim "-r"} option is given explicitely, then the session
320 started will be read-only. That is, the ML world cannot be
321 committed back into the image file. Otherwise, a writable session
322 enables commits into either the input file, or into another output
323 heap file (if that is given as the second argument on the command
326 The read-write state of sessions is determined at startup only, it
327 cannot be changed intermediately. Also note that heap images may
328 require considerable amounts of disk space (approximately
329 50--200~MB). Users are responsible for themselves to dispose their
330 heap files when they are no longer needed.
332 \medskip The @{verbatim "-w"} option makes the output heap file
333 read-only after terminating. Thus subsequent invocations cause the
334 logic image to be read-only automatically.
336 \medskip The @{verbatim "-c"} option tells the underlying ML system
337 to compress the output heap (fully transparently). On Poly/ML for
338 example, the image is garbage collected and all stored values are
339 maximally shared, resulting in up to @{text "50%"} less disk space
342 \medskip The @{verbatim "-C"} option tells the ML system to produce
343 a completely self-contained output image, probably including a copy
344 of the ML runtime system itself.
346 \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
347 passed to the Isabelle session from the command line. Multiple
348 @{verbatim "-e"}'s are evaluated in the given order. Strange things
349 may happen when errorneous ML code is provided. Also make sure that
350 the ML commands are terminated properly by semicolon.
352 \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
353 "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
354 The @{verbatim "-f"} option passes ``@{verbatim
355 "Session.finish();"}'', which is intended mainly for administrative
358 \medskip The @{verbatim "-m"} option adds identifiers of print modes
359 to be made active for this session. Typically, this is used by some
360 user interface, e.g.\ to enable output of proper mathematical
363 \medskip Isabelle normally enters an interactive top-level loop
364 (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
365 option inhibits interaction, thus providing a pure batch mode
368 \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
369 interaction mode on startup, instead of the primitive ML top-level.
370 The @{verbatim "-P"} option configures the top-level loop for
371 interaction with the Proof General user interface, and the
372 @{verbatim "-X"} option enables XML-based PGIP communication. The
373 @{verbatim "-W"} option makes Isabelle enter a special process
374 wrapper for interaction via an external program; the protocol is a
375 stripped-down version of Proof General the interaction mode, see
376 also @{"file" "~~/src/Pure/Tools/isabelle_process.ML"} and @{"file"
377 "~~/src/Pure/Tools/isabelle_process.scala"}.
379 \medskip The @{verbatim "-S"} option makes the Isabelle process more
380 secure by disabling some critical operations, notably runtime
381 compilation and evaluation of ML source code.
385 subsubsection {* Examples *}
388 Run an interactive session of the default object-logic (as specified
389 by the @{setting ISABELLE_LOGIC} setting) like this:
394 Usually @{setting ISABELLE_LOGIC} refers to one of the standard
395 logic images, which are read-only by default. A writable session
396 --- based on @{verbatim FOL}, but output to @{verbatim Foo} (in the
397 directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
398 may be invoked as follows:
400 isabelle-process FOL Foo
402 Ending this session normally (e.g.\ by typing control-D) dumps the
403 whole ML system state into @{verbatim Foo}. Be prepared for several
406 The @{verbatim Foo} session may be continued later (still in
411 A read-only @{verbatim Foo} session may be started by:
413 isabelle-process -r Foo
416 \medskip Note that manual session management like this does
417 \emph{not} provide proper setup for theory presentation. This would
418 require the @{tool usedir} utility.
420 \bigskip The next example demonstrates batch execution of Isabelle.
421 We retrieve the @{verbatim FOL} theory value from the theory loader
424 isabelle-process -e 'theory "FOL";' -q -r FOL
426 Note that the output text will be interspersed with additional junk
427 messages by the ML runtime environment. The @{verbatim "-W"} option
428 allows to communicate with the Isabelle process via an external
429 program in a more robust fashion.
433 section {* The Isabelle tools wrapper \label{sec:isatool} *}
436 All Isabelle related tools and interfaces are called via a common
437 wrapper --- @{executable isatool}:
440 Usage: isatool TOOL [ARGS ...]
442 Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
443 for more specific help.
447 browser - Isabelle graph browser
451 In principle, Isabelle tools are ordinary executable scripts that
452 are run within the Isabelle settings environment, see
453 \secref{sec:settings}. The set of available tools is collected by
454 @{executable isatool} from the directories listed in the @{setting
455 ISABELLE_TOOLS} setting. Do not try to call the scripts directly
456 from the shell. Neither should you add the tool directories to your
461 subsubsection {* Examples *}
464 Show the list of available documentation of the current Isabelle
465 installation like this:
471 View a certain document as follows:
476 Create an Isabelle session derived from HOL (see also
477 \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
479 isatool mkdir HOL Test && isatool make
481 Note that @{verbatim "isatool mkdir"} is usually only invoked once;
482 existing sessions (including document output etc.) are then updated
483 by @{verbatim "isatool make"} alone.
487 section {* The Isabelle interface wrapper \label{sec:interface} *}
490 Isabelle is a generic theorem prover, even w.r.t.\ its user
491 interface. The @{executable_def Isabelle} (or @{executable_def
492 "isabelle-interface"}) executable provides a uniform way for
493 end-users to invoke a certain interface; which one to start is
494 determined by the @{setting_ref ISABELLE_INTERFACE} setting
495 variable, which should give a full path specification to the actual
498 Presently, the most prominent Isabelle interface is Proof
499 General~\cite{proofgeneral}\index{user interface!Proof General}.
500 The Proof General distribution includes an interface wrapper script
501 for the regular Isar toplevel, see @{verbatim
502 "ProofGeneral/isar/interface"}. The canonical settings for
503 Isabelle/Isar are as follows:
506 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
507 PROOFGENERAL_OPTIONS=""
510 Thus @{executable Isabelle} would automatically invoke Emacs with
511 proper setup of the Proof General Lisp packages. There are some
512 options available, such as @{verbatim "-l"} for passing the logic
513 image to be used by default, or @{verbatim "-m"} to tune the
516 \medskip Note that the world may be also seen the other way round:
517 Emacs may be started first (with proper setup of Proof General
518 mode), and @{executable "isabelle-process"} run from within. This
519 requires further Emacs Lisp configuration, see the Proof General
520 documentation \cite{proofgeneral} for more information.