1 theory Basics |
|
2 imports Base |
|
3 begin |
|
4 |
|
5 chapter {* The Isabelle system environment *} |
|
6 |
|
7 text {* This manual describes Isabelle together with related tools and |
|
8 user interfaces as seen from a system oriented view. See also the |
|
9 \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for |
|
10 the actual Isabelle input language and related concepts, and |
|
11 \emph{The Isabelle/Isar Implementation |
|
12 Manual}~\cite{isabelle-implementation} for the main concepts of the |
|
13 underlying implementation in Isabelle/ML. |
|
14 |
|
15 \medskip The Isabelle system environment provides the following |
|
16 basic infrastructure to integrate tools smoothly. |
|
17 |
|
18 \begin{enumerate} |
|
19 |
|
20 \item The \emph{Isabelle settings} mechanism provides process |
|
21 environment variables to all Isabelle executables (including tools |
|
22 and user interfaces). |
|
23 |
|
24 \item The raw \emph{Isabelle process} (@{executable_ref |
|
25 "isabelle-process"}) runs logic sessions either interactively or in |
|
26 batch mode. In particular, this view abstracts over the invocation |
|
27 of the actual ML system to be used. Regular users rarely need to |
|
28 care about the low-level process. |
|
29 |
|
30 \item The main \emph{Isabelle tool wrapper} (@{executable_ref |
|
31 isabelle}) provides a generic startup environment Isabelle related |
|
32 utilities, user interfaces etc. Such tools automatically benefit |
|
33 from the settings mechanism. |
|
34 |
|
35 \end{enumerate} |
|
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 clearly defined places, this scheme is more |
|
51 maintainable and user-friendly than global shell environment |
|
52 variables. |
|
53 |
|
54 In particular, we avoid the typical situation where prospective |
|
55 users of a software package are told to put several things into |
|
56 their shell startup scripts, before being able to actually run the |
|
57 program. Isabelle requires none such administrative chores of its |
|
58 end-users --- the executables can be invoked straight away. |
|
59 Occasionally, users would still want to put the @{file |
|
60 "$ISABELLE_HOME/bin"} directory into their shell's search path, but |
|
61 this is not required. |
|
62 *} |
|
63 |
|
64 |
|
65 subsection {* Bootstrapping the environment \label{sec:boot} *} |
|
66 |
|
67 text {* Isabelle executables need to be run within a proper settings |
|
68 environment. This is bootstrapped as described below, on the first |
|
69 invocation of one of the outer wrapper scripts (such as |
|
70 @{executable_ref isabelle}). This happens only once for each |
|
71 process tree, i.e.\ the environment is passed to subprocesses |
|
72 according to regular Unix conventions. |
|
73 |
|
74 \begin{enumerate} |
|
75 |
|
76 \item The special variable @{setting_def ISABELLE_HOME} is |
|
77 determined automatically from the location of the binary that has |
|
78 been run. |
|
79 |
|
80 You should not try to set @{setting ISABELLE_HOME} manually. Also |
|
81 note that the Isabelle executables either have to be run from their |
|
82 original location in the distribution directory, or via the |
|
83 executable objects created by the @{tool install} tool. Symbolic |
|
84 links are admissible, but a plain copy of the @{file |
|
85 "$ISABELLE_HOME/bin"} files will not work! |
|
86 |
|
87 \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a |
|
88 @{executable_ref bash} shell script with the auto-export option for |
|
89 variables enabled. |
|
90 |
|
91 This file holds a rather long list of shell variable assigments, |
|
92 thus providing the site-wide default settings. The Isabelle |
|
93 distribution already contains a global settings file with sensible |
|
94 defaults for most variables. When installing the system, only a few |
|
95 of these may have to be adapted (probably @{setting ML_SYSTEM} |
|
96 etc.). |
|
97 |
|
98 \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it |
|
99 exists) is run in the same way as the site default settings. Note |
|
100 that the variable @{setting ISABELLE_HOME_USER} has already been set |
|
101 before --- usually to something like @{verbatim |
|
102 "$USER_HOME/.isabelle/IsabelleXXXX"}. |
|
103 |
|
104 Thus individual users may override the site-wide defaults. See also |
|
105 file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the |
|
106 distribution. Typically, a user settings file would contain only a |
|
107 few lines, just the assigments that are really changed. One should |
|
108 definitely \emph{not} start with a full copy the basic @{file |
|
109 "$ISABELLE_HOME/etc/settings"}. This could cause very annoying |
|
110 maintainance problems later, when the Isabelle installation is |
|
111 updated or changed otherwise. |
|
112 |
|
113 \end{enumerate} |
|
114 |
|
115 Since settings files are regular GNU @{executable_def bash} scripts, |
|
116 one may use complex shell commands, such as @{verbatim "if"} or |
|
117 @{verbatim "case"} statements to set variables depending on the |
|
118 system architecture or other environment variables. Such advanced |
|
119 features should be added only with great care, though. In |
|
120 particular, external environment references should be kept at a |
|
121 minimum. |
|
122 |
|
123 \medskip A few variables are somewhat special: |
|
124 |
|
125 \begin{itemize} |
|
126 |
|
127 \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set |
|
128 automatically to the absolute path names of the @{executable |
|
129 "isabelle-process"} and @{executable isabelle} executables, |
|
130 respectively. |
|
131 |
|
132 \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of |
|
133 the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and |
|
134 the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically |
|
135 to its value. |
|
136 |
|
137 \end{itemize} |
|
138 |
|
139 \medskip Note that the settings environment may be inspected with |
|
140 the @{tool getenv} tool. This might help to figure out the effect |
|
141 of complex settings scripts. *} |
|
142 |
|
143 |
|
144 subsection {* Common variables *} |
|
145 |
|
146 text {* |
|
147 This is a reference of common Isabelle settings variables. Note that |
|
148 the list is somewhat open-ended. Third-party utilities or interfaces |
|
149 may add their own selection. Variables that are special in some |
|
150 sense are marked with @{text "\<^sup>*"}. |
|
151 |
|
152 \begin{description} |
|
153 |
|
154 \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform |
|
155 user home directory. On Unix systems this is usually the same as |
|
156 @{setting HOME}, but on Windows it is the regular home directory of |
|
157 the user, not the one of within the Cygwin root |
|
158 file-system.\footnote{Cygwin itself offers another choice whether |
|
159 its HOME should point to the \texttt{/home} directory tree or the |
|
160 Windows user home.} |
|
161 |
|
162 \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the |
|
163 top-level Isabelle distribution directory. This is automatically |
|
164 determined from the Isabelle executable that has been invoked. Do |
|
165 not attempt to set @{setting ISABELLE_HOME} yourself 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 relative to @{verbatim "$USER_HOME/.isabelle"}, under rare |
|
170 circumstances this may be changed in the global setting file. |
|
171 Typically, the @{setting ISABELLE_HOME_USER} directory mimics |
|
172 @{setting ISABELLE_HOME} to some extend. In particular, site-wide |
|
173 defaults may be overridden by a private @{verbatim |
|
174 "$ISABELLE_HOME_USER/etc/settings"}. |
|
175 |
|
176 \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically |
|
177 set to a symbolic identifier for the underlying hardware and |
|
178 operating system. The Isabelle platform identification always |
|
179 refers to the 32 bit variant, even this is a 64 bit machine. Note |
|
180 that the ML or Java runtime may have a different idea, depending on |
|
181 which binaries are actually run. |
|
182 |
|
183 \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to |
|
184 @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant |
|
185 on a platform that supports this; the value is empty for 32 bit. |
|
186 Note that the following bash expression (including the quotes) |
|
187 prefers the 64 bit platform, if that is available: |
|
188 |
|
189 @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""} |
|
190 |
|
191 \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting |
|
192 ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path |
|
193 names of the @{executable "isabelle-process"} and @{executable |
|
194 isabelle} executables, respectively. Thus other tools and scripts |
|
195 need not assume that the @{file "$ISABELLE_HOME/bin"} directory is |
|
196 on the current search path of the shell. |
|
197 |
|
198 \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers |
|
199 to the name of this Isabelle distribution, e.g.\ ``@{verbatim |
|
200 Isabelle2012}''. |
|
201 |
|
202 \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, |
|
203 @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def |
|
204 ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system |
|
205 to be used for Isabelle. There is only a fixed set of admissable |
|
206 @{setting ML_SYSTEM} names (see the @{file |
|
207 "$ISABELLE_HOME/etc/settings"} file of the distribution). |
|
208 |
|
209 The actual compiler binary will be run from the directory @{setting |
|
210 ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the |
|
211 command line. The optional @{setting ML_PLATFORM} may specify the |
|
212 binary format of ML heap images, which is useful for cross-platform |
|
213 installations. The value of @{setting ML_IDENTIFIER} is |
|
214 automatically obtained by composing the values of @{setting |
|
215 ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values. |
|
216 |
|
217 \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK |
|
218 (Java Development Kit) installation with @{verbatim javac} and |
|
219 @{verbatim jar} executables. This is essential for Isabelle/Scala |
|
220 and other JVM-based tools to work properly. Note that conventional |
|
221 @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime |
|
222 Environment), not JDK. |
|
223 |
|
224 \item[@{setting_def ISABELLE_PATH}] is a list of directories |
|
225 (separated by colons) where Isabelle logic images may reside. When |
|
226 looking up heaps files, the value of @{setting ML_IDENTIFIER} is |
|
227 appended to each component internally. |
|
228 |
|
229 \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a |
|
230 directory where output heap files should be stored by default. The |
|
231 ML system and Isabelle version identifier is appended here, too. |
|
232 |
|
233 \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where |
|
234 theory browser information (HTML text, graph data, and printable |
|
235 documents) is stored (see also \secref{sec:info}). The default |
|
236 value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}. |
|
237 |
|
238 \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to |
|
239 load if none is given explicitely by the user. The default value is |
|
240 @{verbatim HOL}. |
|
241 |
|
242 \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default |
|
243 line editor for the @{tool_ref tty} interface. |
|
244 |
|
245 \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed |
|
246 to the command line of any @{tool_ref usedir} invocation. This |
|
247 typically contains compilation options for object-logics --- @{tool |
|
248 usedir} is the basic tool for managing logic sessions (cf.\ the |
|
249 @{verbatim IsaMakefile}s in the distribution). |
|
250 |
|
251 \item[@{setting_def ISABELLE_LATEX}, @{setting_def |
|
252 ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def |
|
253 ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle |
|
254 document preparation (see also \secref{sec:tool-latex}). |
|
255 |
|
256 \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of |
|
257 directories that are scanned by @{executable isabelle} for external |
|
258 utility programs (see also \secref{sec:isabelle-tool}). |
|
259 |
|
260 \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of |
|
261 directories with documentation files. |
|
262 |
|
263 \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred |
|
264 document format, typically @{verbatim dvi} or @{verbatim pdf}. |
|
265 |
|
266 \item[@{setting_def DVI_VIEWER}] specifies the command to be used |
|
267 for displaying @{verbatim dvi} files. |
|
268 |
|
269 \item[@{setting_def PDF_VIEWER}] specifies the command to be used |
|
270 for displaying @{verbatim pdf} files. |
|
271 |
|
272 \item[@{setting_def PRINT_COMMAND}] specifies the standard printer |
|
273 spool command, which is expected to accept @{verbatim ps} files. |
|
274 |
|
275 \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the |
|
276 prefix from which any running @{executable "isabelle-process"} |
|
277 derives an individual directory for temporary files. The default is |
|
278 somewhere in @{verbatim "/tmp"}. |
|
279 |
|
280 \end{description} |
|
281 *} |
|
282 |
|
283 |
|
284 subsection {* Additional components \label{sec:components} *} |
|
285 |
|
286 text {* Any directory may be registered as an explicit \emph{Isabelle |
|
287 component}. The general layout conventions are that of the main |
|
288 Isabelle distribution itself, and the following two files (both |
|
289 optional) have a special meaning: |
|
290 |
|
291 \begin{itemize} |
|
292 |
|
293 \item @{verbatim "etc/settings"} holds additional settings that are |
|
294 initialized when bootstrapping the overall Isabelle environment, |
|
295 cf.\ \secref{sec:boot}. As usual, the content is interpreted as a |
|
296 @{verbatim bash} script. It may refer to the component's enclosing |
|
297 directory via the @{verbatim "COMPONENT"} shell variable. |
|
298 |
|
299 For example, the following setting allows to refer to files within |
|
300 the component later on, without having to hardwire absolute paths: |
|
301 |
|
302 \begin{ttbox} |
|
303 MY_COMPONENT_HOME="$COMPONENT" |
|
304 \end{ttbox} |
|
305 |
|
306 Components can also add to existing Isabelle settings such as |
|
307 @{setting_def ISABELLE_TOOLS}, in order to provide |
|
308 component-specific tools that can be invoked by end-users. For |
|
309 example: |
|
310 |
|
311 \begin{ttbox} |
|
312 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" |
|
313 \end{ttbox} |
|
314 |
|
315 \item @{verbatim "etc/components"} holds a list of further |
|
316 sub-components of the same structure. The directory specifications |
|
317 given here can be either absolute (with leading @{verbatim "/"}) or |
|
318 relative to the component's main directory. |
|
319 |
|
320 \end{itemize} |
|
321 |
|
322 The root of component initialization is @{setting ISABELLE_HOME} |
|
323 itself. After initializing all of its sub-components recursively, |
|
324 @{setting ISABELLE_HOME_USER} is included in the same manner (if |
|
325 that directory exists). This allows to install private components |
|
326 via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is |
|
327 often more convenient to do that programmatically via the |
|
328 \verb,init_component, shell function in the \verb,etc/settings, |
|
329 script of \verb,$ISABELLE_HOME_USER, (or any other component |
|
330 directory). For example: |
|
331 \begin{ttbox} |
|
332 init_component "$HOME/screwdriver-2.0" |
|
333 \end{ttbox} |
|
334 |
|
335 This is tolerant wrt.\ missing component directories, but might |
|
336 produce a warning. |
|
337 |
|
338 \medskip More complex situations may be addressed by initializing |
|
339 components listed in a given catalog file, relatively to some base |
|
340 directory: |
|
341 |
|
342 \begin{ttbox} |
|
343 init_components "$HOME/my_component_store" "some_catalog_file" |
|
344 \end{ttbox} |
|
345 |
|
346 The component directories listed in the catalog file are treated as |
|
347 relative to the given base directory. |
|
348 |
|
349 See also \secref{sec:tool-components} for some tool-support for |
|
350 resolving components that are formally initialized but not installed |
|
351 yet. |
|
352 *} |
|
353 |
|
354 |
|
355 section {* The raw Isabelle process *} |
|
356 |
|
357 text {* |
|
358 The @{executable_def "isabelle-process"} executable runs bare-bones |
|
359 Isabelle logic sessions --- either interactively or in batch mode. |
|
360 It provides an abstraction over the underlying ML system, and over |
|
361 the actual heap file locations. Its usage is: |
|
362 |
|
363 \begin{ttbox} |
|
364 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT] |
|
365 |
|
366 Options are: |
|
367 -I startup Isar interaction mode |
|
368 -P startup Proof General interaction mode |
|
369 -S secure mode -- disallow critical operations |
|
370 -T ADDR startup process wrapper, with socket address |
|
371 -W IN:OUT startup process wrapper, with input/output fifos |
|
372 -X startup PGIP interaction mode |
|
373 -e MLTEXT pass MLTEXT to the ML session |
|
374 -f pass 'Session.finish();' to the ML session |
|
375 -m MODE add print mode for output |
|
376 -q non-interactive session |
|
377 -r open heap file read-only |
|
378 -u pass 'use"ROOT.ML";' to the ML session |
|
379 -w reset write permissions on OUTPUT |
|
380 |
|
381 INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps. |
|
382 These are either names to be searched in the Isabelle path, or |
|
383 actual file names (containing at least one /). |
|
384 If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system. |
|
385 \end{ttbox} |
|
386 |
|
387 Input files without path specifications are looked up in the |
|
388 @{setting ISABELLE_PATH} setting, which may consist of multiple |
|
389 components separated by colons --- these are tried in the given |
|
390 order with the value of @{setting ML_IDENTIFIER} appended |
|
391 internally. In a similar way, base names are relative to the |
|
392 directory specified by @{setting ISABELLE_OUTPUT}. In any case, |
|
393 actual file locations may also be given by including at least one |
|
394 slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to |
|
395 refer to the current directory). |
|
396 *} |
|
397 |
|
398 |
|
399 subsubsection {* Options *} |
|
400 |
|
401 text {* |
|
402 If the input heap file does not have write permission bits set, or |
|
403 the @{verbatim "-r"} option is given explicitely, then the session |
|
404 started will be read-only. That is, the ML world cannot be |
|
405 committed back into the image file. Otherwise, a writable session |
|
406 enables commits into either the input file, or into another output |
|
407 heap file (if that is given as the second argument on the command |
|
408 line). |
|
409 |
|
410 The read-write state of sessions is determined at startup only, it |
|
411 cannot be changed intermediately. Also note that heap images may |
|
412 require considerable amounts of disk space (approximately |
|
413 50--200~MB). Users are responsible for themselves to dispose their |
|
414 heap files when they are no longer needed. |
|
415 |
|
416 \medskip The @{verbatim "-w"} option makes the output heap file |
|
417 read-only after terminating. Thus subsequent invocations cause the |
|
418 logic image to be read-only automatically. |
|
419 |
|
420 \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be |
|
421 passed to the Isabelle session from the command line. Multiple |
|
422 @{verbatim "-e"}'s are evaluated in the given order. Strange things |
|
423 may happen when errorneous ML code is provided. Also make sure that |
|
424 the ML commands are terminated properly by semicolon. |
|
425 |
|
426 \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim |
|
427 "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session. |
|
428 The @{verbatim "-f"} option passes ``@{verbatim |
|
429 "Session.finish();"}'', which is intended mainly for administrative |
|
430 purposes. |
|
431 |
|
432 \medskip The @{verbatim "-m"} option adds identifiers of print modes |
|
433 to be made active for this session. Typically, this is used by some |
|
434 user interface, e.g.\ to enable output of proper mathematical |
|
435 symbols. |
|
436 |
|
437 \medskip Isabelle normally enters an interactive top-level loop |
|
438 (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"} |
|
439 option inhibits interaction, thus providing a pure batch mode |
|
440 facility. |
|
441 |
|
442 \medskip The @{verbatim "-I"} option makes Isabelle enter Isar |
|
443 interaction mode on startup, instead of the primitive ML top-level. |
|
444 The @{verbatim "-P"} option configures the top-level loop for |
|
445 interaction with the Proof General user interface, and the |
|
446 @{verbatim "-X"} option enables XML-based PGIP communication. |
|
447 |
|
448 \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes |
|
449 Isabelle enter a special process wrapper for interaction via the |
|
450 Isabelle/Scala layer, see also @{file |
|
451 "~~/src/Pure/System/isabelle_process.scala"}. The protocol between |
|
452 the ML and JVM process is private to the implementation. |
|
453 |
|
454 \medskip The @{verbatim "-S"} option makes the Isabelle process more |
|
455 secure by disabling some critical operations, notably runtime |
|
456 compilation and evaluation of ML source code. |
|
457 *} |
|
458 |
|
459 |
|
460 subsubsection {* Examples *} |
|
461 |
|
462 text {* |
|
463 Run an interactive session of the default object-logic (as specified |
|
464 by the @{setting ISABELLE_LOGIC} setting) like this: |
|
465 \begin{ttbox} |
|
466 isabelle-process |
|
467 \end{ttbox} |
|
468 |
|
469 Usually @{setting ISABELLE_LOGIC} refers to one of the standard |
|
470 logic images, which are read-only by default. A writable session |
|
471 --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the |
|
472 directory specified by the @{setting ISABELLE_OUTPUT} setting) --- |
|
473 may be invoked as follows: |
|
474 \begin{ttbox} |
|
475 isabelle-process HOL Test |
|
476 \end{ttbox} |
|
477 Ending this session normally (e.g.\ by typing control-D) dumps the |
|
478 whole ML system state into @{verbatim Test} (be prepared for more |
|
479 than 100\,MB): |
|
480 |
|
481 The @{verbatim Test} session may be continued later (still in |
|
482 writable state) by: |
|
483 \begin{ttbox} |
|
484 isabelle-process Test |
|
485 \end{ttbox} |
|
486 A read-only @{verbatim Test} session may be started by: |
|
487 \begin{ttbox} |
|
488 isabelle-process -r Test |
|
489 \end{ttbox} |
|
490 |
|
491 \medskip Note that manual session management like this does |
|
492 \emph{not} provide proper setup for theory presentation. This would |
|
493 require @{tool usedir}. |
|
494 |
|
495 \bigskip The next example demonstrates batch execution of Isabelle. |
|
496 We retrieve the @{verbatim Main} theory value from the theory loader |
|
497 within ML (observe the delicate quoting rules for the Bash shell |
|
498 vs.\ ML): |
|
499 \begin{ttbox} |
|
500 isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL |
|
501 \end{ttbox} |
|
502 Note that the output text will be interspersed with additional junk |
|
503 messages by the ML runtime environment. The @{verbatim "-W"} option |
|
504 allows to communicate with the Isabelle process via an external |
|
505 program in a more robust fashion. |
|
506 *} |
|
507 |
|
508 |
|
509 section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *} |
|
510 |
|
511 text {* |
|
512 All Isabelle related tools and interfaces are called via a common |
|
513 wrapper --- @{executable isabelle}: |
|
514 |
|
515 \begin{ttbox} |
|
516 Usage: isabelle TOOL [ARGS ...] |
|
517 |
|
518 Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. |
|
519 |
|
520 Available tools: |
|
521 \dots |
|
522 \end{ttbox} |
|
523 |
|
524 In principle, Isabelle tools are ordinary executable scripts that |
|
525 are run within the Isabelle settings environment, see |
|
526 \secref{sec:settings}. The set of available tools is collected by |
|
527 @{executable isabelle} from the directories listed in the @{setting |
|
528 ISABELLE_TOOLS} setting. Do not try to call the scripts directly |
|
529 from the shell. Neither should you add the tool directories to your |
|
530 shell's search path! |
|
531 *} |
|
532 |
|
533 |
|
534 subsubsection {* Examples *} |
|
535 |
|
536 text {* Show the list of available documentation of the Isabelle |
|
537 distribution: |
|
538 |
|
539 \begin{ttbox} |
|
540 isabelle doc |
|
541 \end{ttbox} |
|
542 |
|
543 View a certain document as follows: |
|
544 \begin{ttbox} |
|
545 isabelle doc system |
|
546 \end{ttbox} |
|
547 |
|
548 Query the Isabelle settings environment: |
|
549 \begin{ttbox} |
|
550 isabelle getenv ISABELLE_HOME_USER |
|
551 \end{ttbox} |
|
552 *} |
|
553 |
|
554 end |
|