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