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