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