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
26 "isabelle-process"}) runs logic sessions either interactively or in
27 batch mode. In particular, this view abstracts over the invocation
28 of the actual ML system to be used. Regular users rarely need to
29 care about the low-level process.
31 \item The \emph{Isabelle tools wrapper} (@{executable_ref isabelle})
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-interface"}) provides some abstraction over the actual
38 user interface to be used. The de-facto standard interface for
39 Isabelle is Proof~General \cite{proofgeneral}.
45 section {* Isabelle settings \label{sec:settings} *}
48 The Isabelle system heavily depends on the \emph{settings
49 mechanism}\indexbold{settings}. Essentially, this is a statically
50 scoped collection of environment variables, such as @{setting
51 ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}. These
52 variables are \emph{not} intended to be set directly from the shell,
53 though. Isabelle employs a somewhat more sophisticated scheme of
54 \emph{settings files} --- one for site-wide defaults, another for
55 additional user-specific modifications. With all configuration
56 variables in at most two places, this scheme is more maintainable
57 and user-friendly than global shell environment variables.
59 In particular, we avoid the typical situation where prospective
60 users of a software package are told to put several things into
61 their shell startup scripts, before being able to actually run the
62 program. Isabelle requires none such administrative chores of its
63 end-users --- the executables can be invoked straight away.
64 Occasionally, users would still want to put the @{"file"
65 "$ISABELLE_HOME/bin"} directory into their shell's search path, but
70 subsection {* Building the environment *}
73 Whenever any of the Isabelle executables is run, their settings
74 environment is put together as follows.
78 \item The special variable @{setting_def ISABELLE_HOME} is
79 determined automatically from the location of the binary that has
82 You should not try to set @{setting ISABELLE_HOME} manually. Also
83 note that the Isabelle executables either have to be run from their
84 original location in the distribution directory, or via the
85 executable objects created by the @{tool install} utility. Symbolic
86 links are admissible, but a plain copy of the @{"file"
87 "$ISABELLE_HOME/bin"} files will not work!
89 \item The file @{"file" "$ISABELLE_HOME/etc/settings"} ist run as a
90 @{executable_ref bash} shell script with the auto-export option for
93 This file holds a rather long list of shell variable assigments,
94 thus providing the site-wide default settings. The Isabelle
95 distribution already contains a global settings file with sensible
96 defaults for most variables. When installing the system, only a few
97 of these may have to be adapted (probably @{setting ML_SYSTEM}
100 \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
101 exists) is run in the same way as the site default settings. Note
102 that the variable @{setting ISABELLE_HOME_USER} has already been set
103 before --- usually to @{verbatim "~/isabelle"}.
105 Thus individual users may override the site-wide defaults. See also
106 file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
107 distribution. Typically, a user settings file would contain only a
108 few lines, just the assigments that are really changed. One should
109 definitely \emph{not} start with a full copy the basic @{"file"
110 "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
111 maintainance problems later, when the Isabelle installation is
112 updated or changed otherwise.
116 Since settings files are regular GNU @{executable_def bash} scripts,
117 one may use complex shell commands, such as @{verbatim "if"} or
118 @{verbatim "case"} statements to set variables depending on the
119 system architecture or other environment variables. Such advanced
120 features should be added only with great care, though. In
121 particular, external environment references should be kept at a
124 \medskip A few variables are somewhat special:
128 \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
129 automatically to the absolute path names of the @{executable
130 "isabelle-process"} and @{executable isabelle} executables,
133 \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
134 the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
135 the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
140 \medskip Note that the settings environment may be inspected with
141 the Isabelle tool @{tool getenv}. This might help to figure out the
142 effect of complex settings scripts.
146 subsection{* Common variables *}
149 This is a reference of common Isabelle settings variables. Note that
150 the list is somewhat open-ended. Third-party utilities or interfaces
151 may add their own selection. Variables that are special in some
152 sense are marked with @{text "\<^sup>*"}.
156 \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
157 location of the top-level Isabelle distribution directory. This is
158 automatically determined from the Isabelle executable that has been
159 invoked. Do not attempt to set @{setting ISABELLE_HOME} yourself
162 \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
163 counterpart of @{setting ISABELLE_HOME}. The default value is
164 @{verbatim "~/isabelle"}, under rare circumstances this may be
165 changed in the global setting file. Typically, the @{setting
166 ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
167 some extend. In particular, site-wide defaults may be overridden by
168 a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
170 \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
171 ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
172 names of the @{executable "isabelle-process"} and @{executable
173 isabelle} executables, respectively. Thus other tools and scripts
174 need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is
175 on the current search path of the shell.
177 \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
178 to the name of this Isabelle distribution, e.g.\ ``@{verbatim
181 \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
182 @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
183 ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
184 to be used for Isabelle. There is only a fixed set of admissable
185 @{setting ML_SYSTEM} names (see the @{"file"
186 "$ISABELLE_HOME/etc/settings"} file of the distribution).
188 The actual compiler binary will be run from the directory @{setting
189 ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
190 command line. The optional @{setting ML_PLATFORM} may specify the
191 binary format of ML heap images, which is useful for cross-platform
192 installations. The value of @{setting ML_IDENTIFIER} is
193 automatically obtained by composing the values of @{setting
194 ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
196 \item[@{setting_def ISABELLE_PATH}] is a list of directories
197 (separated by colons) where Isabelle logic images may reside. When
198 looking up heaps files, the value of @{setting ML_IDENTIFIER} is
199 appended to each component internally.
201 \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
202 directory where output heap files should be stored by default. The
203 ML system and Isabelle version identifier is appended here, too.
205 \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
206 theory browser information (HTML text, graph data, and printable
207 documents) is stored (see also \secref{sec:info}). The default
208 value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
210 \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
211 load if none is given explicitely by the user. The default value is
214 \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
215 line editor for the @{tool_ref tty} interface.
217 \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
218 to the command line of any @{tool_ref usedir} invocation. This
219 typically contains compilation options for object-logics --- @{tool
220 usedir} is the basic utility for managing logic sessions (cf.\ the
221 @{verbatim IsaMakefile}s in the distribution).
223 \item[@{setting_def ISABELLE_FILE_IDENT}] specifies a shell command
224 for producing a source file identification, based on the actual
225 content instead of the full physical path and date stamp (which is
226 the default). A typical identification would produce a ``digest'' of
227 the text, using a cryptographic hash function like SHA-1, for
230 \item[@{setting_def ISABELLE_LATEX}, @{setting_def
231 ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
232 ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
233 document preparation (see also \secref{sec:tool-latex}).
235 \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
236 directories that are scanned by @{executable isabelle} for external
237 utility programs (see also \secref{sec:isabelle-tool}).
239 \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
240 directories with documentation files.
242 \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
243 document format, typically @{verbatim dvi} or @{verbatim pdf}.
245 \item[@{setting_def DVI_VIEWER}] specifies the command to be used
246 for displaying @{verbatim dvi} files.
248 \item[@{setting_def PDF_VIEWER}] specifies the command to be used
249 for displaying @{verbatim pdf} files.
251 \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
252 spool command, which is expected to accept @{verbatim ps} files.
254 \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
255 prefix from which any running @{executable "isabelle-process"}
256 derives an individual directory for temporary files. The default is
257 somewhere in @{verbatim "/tmp"}.
259 \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
260 specifies the actual user interface that the capital @{executable
261 Isabelle} or @{executable "isabelle-interface"} should invoke. See
262 \secref{sec:interface} for more details.
268 section {* The raw Isabelle process *}
271 The @{executable_def "isabelle-process"} executable runs bare-bones
272 Isabelle logic sessions --- either interactively or in batch mode.
273 It provides an abstraction over the underlying ML system, and over
274 the actual heap file locations. Its usage is:
277 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
280 -C tell ML system to copy output image
281 -I startup Isar interaction mode
282 -P startup Proof General interaction mode
283 -S secure mode -- disallow critical operations
284 -W OUTPUT startup process wrapper, with messages going to OUTPUT stream
285 -X startup PGIP interaction mode
286 -c tell ML system to compress output image
287 -e MLTEXT pass MLTEXT to the ML session
288 -f pass 'Session.finish();' to the ML session
289 -m MODE add print mode for output
290 -q non-interactive session
291 -r open heap file read-only
292 -u pass 'use"ROOT.ML";' to the ML session
293 -w reset write permissions on OUTPUT
295 INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
296 These are either names to be searched in the Isabelle path, or
297 actual file names (containing at least one /).
298 If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
301 Input files without path specifications are looked up in the
302 @{setting ISABELLE_PATH} setting, which may consist of multiple
303 components separated by colons --- these are tried in the given
304 order with the value of @{setting ML_IDENTIFIER} appended
305 internally. In a similar way, base names are relative to the
306 directory specified by @{setting ISABELLE_OUTPUT}. In any case,
307 actual file locations may also be given by including at least one
308 slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
309 refer to the current directory).
313 subsubsection {* Options *}
316 If the input heap file does not have write permission bits set, or
317 the @{verbatim "-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 @{verbatim "-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 @{verbatim "-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 @{text "50%"} less disk space
340 \medskip The @{verbatim "-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 @{verbatim "-e"} option, arbitrary ML code may be
345 passed to the Isabelle session from the command line. Multiple
346 @{verbatim "-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 @{verbatim "-u"} option is a shortcut for @{verbatim
351 "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
352 The @{verbatim "-f"} option passes ``@{verbatim
353 "Session.finish();"}'', which is intended mainly for administrative
356 \medskip The @{verbatim "-m"} option adds identifiers of print modes
357 to be made active for this session. Typically, this is used by some
358 user interface, e.g.\ to enable output of proper mathematical
361 \medskip Isabelle normally enters an interactive top-level loop
362 (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
363 option inhibits interaction, thus providing a pure batch mode
366 \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
367 interaction mode on startup, instead of the primitive ML top-level.
368 The @{verbatim "-P"} option configures the top-level loop for
369 interaction with the Proof General user interface, and the
370 @{verbatim "-X"} option enables XML-based PGIP communication. The
371 @{verbatim "-W"} option makes Isabelle enter a special process
372 wrapper for interaction via an external program; the protocol is a
373 stripped-down version of Proof General the interaction mode, see
374 also @{"file" "~~/src/Pure/Tools/isabelle_process.ML"} and @{"file"
375 "~~/src/Pure/Tools/isabelle_process.scala"}.
377 \medskip The @{verbatim "-S"} option makes the Isabelle process more
378 secure by disabling some critical operations, notably runtime
379 compilation and evaluation of ML source code.
383 subsubsection {* Examples *}
386 Run an interactive session of the default object-logic (as specified
387 by the @{setting ISABELLE_LOGIC} setting) like this:
392 Usually @{setting ISABELLE_LOGIC} refers to one of the standard
393 logic images, which are read-only by default. A writable session
394 --- based on @{verbatim FOL}, but output to @{verbatim Foo} (in the
395 directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
396 may be invoked as follows:
398 isabelle-process FOL Foo
400 Ending this session normally (e.g.\ by typing control-D) dumps the
401 whole ML system state into @{verbatim Foo}. Be prepared for several
404 The @{verbatim Foo} session may be continued later (still in
409 A read-only @{verbatim Foo} session may be started by:
411 isabelle-process -r Foo
414 \medskip Note that manual session management like this does
415 \emph{not} provide proper setup for theory presentation. This would
416 require the @{tool usedir} utility.
418 \bigskip The next example demonstrates batch execution of Isabelle.
419 We retrieve the @{verbatim FOL} theory value from the theory loader
422 isabelle-process -e 'theory "FOL";' -q -r FOL
424 Note that the output text will be interspersed with additional junk
425 messages by the ML runtime environment. The @{verbatim "-W"} option
426 allows to communicate with the Isabelle process via an external
427 program in a more robust fashion.
431 section {* The Isabelle tools wrapper \label{sec:isabelle-tool} *}
434 All Isabelle related tools and interfaces are called via a common
435 wrapper --- @{executable isabelle}:
438 Usage: isabelle TOOL [ARGS ...]
440 Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
444 browser - Isabelle graph browser
448 In principle, Isabelle tools are ordinary executable scripts that
449 are run within the Isabelle settings environment, see
450 \secref{sec:settings}. The set of available tools is collected by
451 @{executable isabelle} from the directories listed in the @{setting
452 ISABELLE_TOOLS} setting. Do not try to call the scripts directly
453 from the shell. Neither should you add the tool directories to your
458 subsubsection {* Examples *}
461 Show the list of available documentation of the current Isabelle
462 installation like this:
468 View a certain document as follows:
470 isabelle doc isar-ref
473 Create an Isabelle session derived from HOL (see also
474 \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
476 isabelle mkdir HOL Test && isabelle make
478 Note that @{verbatim "isabelle mkdir"} is usually only invoked once;
479 existing sessions (including document output etc.) are then updated
480 by @{verbatim "isabelle make"} alone.
484 section {* The Isabelle interface wrapper \label{sec:interface} *}
487 Isabelle is a generic theorem prover, even w.r.t.\ its user
488 interface. The @{executable_def Isabelle} (or @{executable_def
489 "isabelle-interface"}) executable provides a uniform way for
490 end-users to invoke a certain interface; which one to start is
491 determined by the @{setting_ref ISABELLE_INTERFACE} setting
492 variable, which should give a full path specification to the actual
495 Presently, the most prominent Isabelle interface is Proof
496 General~\cite{proofgeneral}\index{user interface!Proof General}.
497 The Proof General distribution includes an interface wrapper script
498 for the regular Isar toplevel, see @{verbatim
499 "ProofGeneral/isar/interface"}. The canonical settings for
500 Isabelle/Isar are as follows:
503 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
504 PROOFGENERAL_OPTIONS=""
507 Thus @{executable Isabelle} would automatically invoke Emacs with
508 proper setup of the Proof General Lisp packages. There are some
509 options available, such as @{verbatim "-l"} for passing the logic
510 image to be used by default, or @{verbatim "-m"} to tune the
513 \medskip Note that the world may be also seen the other way round:
514 Emacs may be started first (with proper setup of Proof General
515 mode), and @{executable "isabelle-process"} run from within. This
516 requires further Emacs Lisp configuration, see the Proof General
517 documentation \cite{proofgeneral} for more information.