author | wenzelm |
Thu, 03 Mar 2016 23:33:22 +0100 | |
changeset 62511 | 93fa1efc7219 |
parent 62506 | 860cd901ab43 |
child 62559 | 83e815849a91 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
28215 | 3 |
theory Basics |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
41955
diff
changeset
|
4 |
imports Base |
28215 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>The Isabelle system environment\<close> |
28215 | 8 |
|
61575 | 9 |
text \<open> |
10 |
This manual describes Isabelle together with related tools and user |
|
11 |
interfaces as seen from a system oriented view. See also the \<^emph>\<open>Isabelle/Isar |
|
12 |
Reference Manual\<close> @{cite "isabelle-isar-ref"} for the actual Isabelle input |
|
13 |
language and related concepts, and \<^emph>\<open>The Isabelle/Isar Implementation |
|
61477 | 14 |
Manual\<close> @{cite "isabelle-implementation"} for the main concepts of the |
47823 | 15 |
underlying implementation in Isabelle/ML. |
28215 | 16 |
|
61406 | 17 |
\<^medskip> |
61575 | 18 |
The Isabelle system environment provides the following basic infrastructure |
19 |
to integrate tools smoothly. |
|
28215 | 20 |
|
61575 | 21 |
\<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process environment variables |
22 |
to all Isabelle executables (including tools and user interfaces). |
|
28215 | 23 |
|
61575 | 24 |
\<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs |
25 |
logic sessions either interactively or in batch mode. In particular, this |
|
26 |
view abstracts over the invocation of the actual ML system to be used. |
|
27 |
Regular users rarely need to care about the low-level process. |
|
28215 | 28 |
|
61575 | 29 |
\<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a |
30 |
generic startup environment Isabelle related utilities, user interfaces etc. |
|
31 |
Such tools automatically benefit from the settings mechanism. |
|
58618 | 32 |
\<close> |
28215 | 33 |
|
34 |
||
58618 | 35 |
section \<open>Isabelle settings \label{sec:settings}\<close> |
28215 | 36 |
|
58618 | 37 |
text \<open> |
62013 | 38 |
The Isabelle system heavily depends on the \<^emph>\<open>settings mechanism\<close>. |
39 |
Essentially, this is a statically scoped collection of environment |
|
40 |
variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting |
|
41 |
ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the |
|
42 |
shell, though. Isabelle employs a somewhat more sophisticated scheme of |
|
43 |
\<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for additional |
|
44 |
user-specific modifications. With all configuration variables in clearly |
|
45 |
defined places, this scheme is more maintainable and user-friendly than |
|
46 |
global shell environment variables. |
|
28215 | 47 |
|
61575 | 48 |
In particular, we avoid the typical situation where prospective users of a |
49 |
software package are told to put several things into their shell startup |
|
50 |
scripts, before being able to actually run the program. Isabelle requires |
|
51 |
none such administrative chores of its end-users --- the executables can be |
|
52 |
invoked straight away. Occasionally, users would still want to put the |
|
53 |
@{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but |
|
28238 | 54 |
this is not required. |
58618 | 55 |
\<close> |
28215 | 56 |
|
57 |
||
58618 | 58 |
subsection \<open>Bootstrapping the environment \label{sec:boot}\<close> |
28215 | 59 |
|
61575 | 60 |
text \<open> |
61 |
Isabelle executables need to be run within a proper settings environment. |
|
62 |
This is bootstrapped as described below, on the first invocation of one of |
|
63 |
the outer wrapper scripts (such as @{executable_ref isabelle}). This happens |
|
64 |
only once for each process tree, i.e.\ the environment is passed to |
|
65 |
subprocesses according to regular Unix conventions. |
|
66 |
||
67 |
\<^enum> The special variable @{setting_def ISABELLE_HOME} is determined |
|
68 |
automatically from the location of the binary that has been run. |
|
28215 | 69 |
|
61575 | 70 |
You should not try to set @{setting ISABELLE_HOME} manually. Also note |
71 |
that the Isabelle executables either have to be run from their original |
|
72 |
location in the distribution directory, or via the executable objects |
|
73 |
created by the @{tool install} tool. Symbolic links are admissible, but a |
|
74 |
plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work! |
|
75 |
||
76 |
\<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a |
|
77 |
@{executable_ref bash} shell script with the auto-export option for |
|
78 |
variables enabled. |
|
28238 | 79 |
|
61575 | 80 |
This file holds a rather long list of shell variable assignments, thus |
81 |
providing the site-wide default settings. The Isabelle distribution |
|
82 |
already contains a global settings file with sensible defaults for most |
|
83 |
variables. When installing the system, only a few of these may have to be |
|
84 |
adapted (probably @{setting ML_SYSTEM} etc.). |
|
85 |
||
86 |
\<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it |
|
87 |
exists) is run in the same way as the site default settings. Note that the |
|
88 |
variable @{setting ISABELLE_HOME_USER} has already been set before --- |
|
89 |
usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>. |
|
61458 | 90 |
|
61575 | 91 |
Thus individual users may override the site-wide defaults. Typically, a |
92 |
user settings file contains only a few lines, with some assignments that |
|
93 |
are actually changed. Never copy the central @{file |
|
94 |
"$ISABELLE_HOME/etc/settings"} file! |
|
28215 | 95 |
|
61575 | 96 |
Since settings files are regular GNU @{executable_def bash} scripts, one may |
97 |
use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set |
|
98 |
variables depending on the system architecture or other environment |
|
99 |
variables. Such advanced features should be added only with great care, |
|
100 |
though. In particular, external environment references should be kept at a |
|
28215 | 101 |
minimum. |
102 |
||
61406 | 103 |
\<^medskip> |
104 |
A few variables are somewhat special: |
|
28215 | 105 |
|
61575 | 106 |
\<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set |
107 |
automatically to the absolute path names of the @{executable |
|
108 |
"isabelle_process"} and @{executable isabelle} executables, respectively. |
|
28215 | 109 |
|
61575 | 110 |
\<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle |
111 |
distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\ |
|
112 |
@{setting ML_IDENTIFIER}) appended automatically to its value. |
|
28215 | 113 |
|
61406 | 114 |
\<^medskip> |
61575 | 115 |
Note that the settings environment may be inspected with the @{tool getenv} |
116 |
tool. This might help to figure out the effect of complex settings scripts. |
|
117 |
\<close> |
|
28215 | 118 |
|
119 |
||
58618 | 120 |
subsection \<open>Common variables\<close> |
28215 | 121 |
|
58618 | 122 |
text \<open> |
61575 | 123 |
This is a reference of common Isabelle settings variables. Note that the |
124 |
list is somewhat open-ended. Third-party utilities or interfaces may add |
|
125 |
their own selection. Variables that are special in some sense are marked |
|
126 |
with \<open>\<^sup>*\<close>. |
|
28215 | 127 |
|
61575 | 128 |
\<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory. |
129 |
On Unix systems this is usually the same as @{setting HOME}, but on Windows |
|
130 |
it is the regular home directory of the user, not the one of within the |
|
131 |
Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its |
|
132 |
HOME should point to the @{file_unchecked "/home"} directory tree or the |
|
61572 | 133 |
Windows user home.\<close> |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
134 |
|
61575 | 135 |
\<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level |
136 |
Isabelle distribution directory. This is automatically determined from the |
|
137 |
Isabelle executable that has been invoked. Do not attempt to set @{setting |
|
138 |
ISABELLE_HOME} yourself from the shell! |
|
50182 | 139 |
|
61575 | 140 |
\<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of |
141 |
@{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked |
|
142 |
"$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the |
|
143 |
global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory |
|
144 |
mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide |
|
145 |
defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. |
|
146 |
||
147 |
\<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the |
|
148 |
general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that |
|
50182 | 149 |
platform-dependent tools usually need to refer to the more specific |
150 |
identification according to @{setting ISABELLE_PLATFORM}, @{setting |
|
151 |
ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}. |
|
152 |
||
61575 | 153 |
\<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic |
154 |
identifier for the underlying hardware and operating system. The Isabelle |
|
155 |
platform identification always refers to the 32 bit variant, even this is a |
|
156 |
64 bit machine. Note that the ML or Java runtime may have a different idea, |
|
157 |
depending on which binaries are actually run. |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
158 |
|
61575 | 159 |
\<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting |
160 |
ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform |
|
161 |
that supports this; the value is empty for 32 bit. Note that the following |
|
162 |
bash expression (including the quotes) prefers the 64 bit platform, if that |
|
163 |
is available: |
|
47823 | 164 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
165 |
@{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>} |
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
166 |
|
61575 | 167 |
\<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] are |
168 |
automatically set to the full path names of the @{executable |
|
169 |
"isabelle_process"} and @{executable isabelle} executables, respectively. |
|
170 |
Thus other tools and scripts need not assume that the @{file |
|
171 |
"$ISABELLE_HOME/bin"} directory is on the current search path of the shell. |
|
28215 | 172 |
|
61575 | 173 |
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this |
174 |
Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''. |
|
175 |
||
176 |
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def |
|
177 |
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>] |
|
178 |
specify the underlying ML system to be used for Isabelle. There is only a |
|
179 |
fixed set of admissable @{setting ML_SYSTEM} names (see the @{file |
|
28238 | 180 |
"$ISABELLE_HOME/etc/settings"} file of the distribution). |
61575 | 181 |
|
28215 | 182 |
The actual compiler binary will be run from the directory @{setting |
61575 | 183 |
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line. |
184 |
The optional @{setting ML_PLATFORM} may specify the binary format of ML heap |
|
185 |
images, which is useful for cross-platform installations. The value of |
|
186 |
@{setting ML_IDENTIFIER} is automatically obtained by composing the values |
|
187 |
of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version |
|
188 |
values. |
|
47823 | 189 |
|
61575 | 190 |
\<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java |
191 |
Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is |
|
192 |
essential for Isabelle/Scala and other JVM-based tools to work properly. |
|
193 |
Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime |
|
47823 | 194 |
Environment), not JDK. |
61575 | 195 |
|
196 |
\<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by |
|
197 |
colons) where Isabelle logic images may reside. When looking up heaps files, |
|
198 |
the value of @{setting ML_IDENTIFIER} is appended to each component |
|
199 |
internally. |
|
200 |
||
201 |
\<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files |
|
202 |
should be stored by default. The ML system and Isabelle version identifier |
|
203 |
is appended here, too. |
|
204 |
||
205 |
\<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory |
|
62013 | 206 |
browser information is stored as HTML and PDF (see also \secref{sec:info}). |
207 |
The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}. |
|
61575 | 208 |
|
209 |
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none |
|
210 |
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>. |
|
211 |
||
212 |
\<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the |
|
213 |
@{tool_ref console} interface. |
|
28215 | 214 |
|
61575 | 215 |
\<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, |
216 |
@{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle |
|
217 |
document preparation (see also \secref{sec:tool-latex}). |
|
218 |
||
219 |
\<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories |
|
220 |
that are scanned by @{executable isabelle} for external utility programs |
|
221 |
(see also \secref{sec:isabelle-tool}). |
|
50197
b385d134926d
eval PDF_VIEWER/DVI_VIEWER command line, which allows additional quotes for program name, for example;
wenzelm
parents:
50182
diff
changeset
|
222 |
|
61575 | 223 |
\<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories |
224 |
with documentation files. |
|
225 |
||
226 |
\<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying |
|
227 |
\<^verbatim>\<open>pdf\<close> files. |
|
54683
cf48ddc266e5
clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents:
52746
diff
changeset
|
228 |
|
61575 | 229 |
\<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying |
230 |
\<^verbatim>\<open>dvi\<close> files. |
|
231 |
||
232 |
\<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any |
|
233 |
running @{executable "isabelle_process"} derives an individual directory for |
|
234 |
temporary files. |
|
58618 | 235 |
\<close> |
28215 | 236 |
|
237 |
||
58618 | 238 |
subsection \<open>Additional components \label{sec:components}\<close> |
32323 | 239 |
|
61575 | 240 |
text \<open> |
241 |
Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The |
|
242 |
general layout conventions are that of the main Isabelle distribution |
|
243 |
itself, and the following two files (both optional) have a special meaning: |
|
32323 | 244 |
|
61575 | 245 |
\<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when |
246 |
bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As |
|
247 |
usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the |
|
248 |
component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable. |
|
32323 | 249 |
|
61575 | 250 |
For example, the following setting allows to refer to files within the |
251 |
component later on, without having to hardwire absolute paths: |
|
252 |
@{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>} |
|
32323 | 253 |
|
61575 | 254 |
Components can also add to existing Isabelle settings such as |
255 |
@{setting_def ISABELLE_TOOLS}, in order to provide component-specific |
|
256 |
tools that can be invoked by end-users. For example: |
|
257 |
@{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>} |
|
32323 | 258 |
|
61575 | 259 |
\<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same |
260 |
structure. The directory specifications given here can be either absolute |
|
261 |
(with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory. |
|
32323 | 262 |
|
61575 | 263 |
The root of component initialization is @{setting ISABELLE_HOME} itself. |
264 |
After initializing all of its sub-components recursively, @{setting |
|
265 |
ISABELLE_HOME_USER} is included in the same manner (if that directory |
|
266 |
exists). This allows to install private components via @{file_unchecked |
|
267 |
"$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient |
|
268 |
to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the |
|
269 |
\<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component |
|
270 |
directory). For example: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
271 |
@{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>} |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
272 |
|
61575 | 273 |
This is tolerant wrt.\ missing component directories, but might produce a |
274 |
warning. |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
275 |
|
61406 | 276 |
\<^medskip> |
61575 | 277 |
More complex situations may be addressed by initializing components listed |
278 |
in a given catalog file, relatively to some base directory: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
279 |
@{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>} |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
280 |
|
61575 | 281 |
The component directories listed in the catalog file are treated as relative |
282 |
to the given base directory. |
|
48844 | 283 |
|
61575 | 284 |
See also \secref{sec:tool-components} for some tool-support for resolving |
285 |
components that are formally initialized but not installed yet. |
|
58618 | 286 |
\<close> |
32323 | 287 |
|
288 |
||
58618 | 289 |
section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close> |
28215 | 290 |
|
58618 | 291 |
text \<open> |
61575 | 292 |
The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle |
293 |
logic sessions --- either interactively or in batch mode. It provides an |
|
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
294 |
abstraction over the underlying ML system and its saved heap files. Its |
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
295 |
usage is: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
296 |
@{verbatim [display] |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
297 |
\<open>Usage: isabelle_process [OPTIONS] [HEAP] |
28215 | 298 |
|
299 |
Options are: |
|
57581
74bbe9317aa4
provide explicit options file -- avoid multiple Scala/JVM invocation;
wenzelm
parents:
57439
diff
changeset
|
300 |
-O system options from given YXML file |
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
58846
diff
changeset
|
301 |
-P SOCKET startup process wrapper via TCP socket |
28215 | 302 |
-S secure mode -- disallow critical operations |
62506 | 303 |
-e ML_EXPR evaluate ML expression on startup |
304 |
-f ML_FILE evaluate ML file on startup |
|
28215 | 305 |
-m MODE add print mode for output |
52056 | 306 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
28215 | 307 |
-q non-interactive session |
308 |
||
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
309 |
If HEAP is a plain name (default "HOL"), it is searched in $ISABELLE_PATH; |
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
310 |
if it contains a slash, it is taken as literal file; if it is RAW_ML_SYSTEM, |
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
311 |
the initial ML heap is used.\<close>} |
28215 | 312 |
|
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
313 |
Heap files without path specifications are looked up in the @{setting |
61575 | 314 |
ISABELLE_PATH} setting, which may consist of multiple components separated |
315 |
by colons --- these are tried in the given order with the value of @{setting |
|
316 |
ML_IDENTIFIER} appended internally. In a similar way, base names are |
|
317 |
relative to the directory specified by @{setting ISABELLE_OUTPUT}. In any |
|
318 |
case, actual file locations may also be given by including at least one |
|
319 |
slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to refer to the current |
|
320 |
directory). |
|
58618 | 321 |
\<close> |
28215 | 322 |
|
323 |
||
58618 | 324 |
subsubsection \<open>Options\<close> |
28215 | 325 |
|
58618 | 326 |
text \<open> |
62506 | 327 |
Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is |
328 |
started. The source is either given literally or taken from a file. Multiple |
|
329 |
\<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to |
|
330 |
premature exit of the ML process with return code 1. |
|
28215 | 331 |
|
61406 | 332 |
\<^medskip> |
61575 | 333 |
The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this |
334 |
session. Typically, this is used by some user interface, e.g.\ to enable |
|
335 |
output of proper mathematical symbols. |
|
28215 | 336 |
|
61406 | 337 |
\<^medskip> |
61575 | 338 |
Isabelle normally enters an interactive top-level loop (after processing the |
339 |
\<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close> option inhibits interaction, thus providing a pure |
|
340 |
batch mode facility. |
|
28215 | 341 |
|
61406 | 342 |
\<^medskip> |
61575 | 343 |
Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process, |
344 |
see also \secref{sec:system-options}. Alternatively, option \<^verbatim>\<open>-O\<close> specifies |
|
345 |
the full environment of system options as a file in YXML format (according |
|
346 |
to the Isabelle/Scala function \<^verbatim>\<open>isabelle.Options.encode\<close>). |
|
52056 | 347 |
|
61406 | 348 |
\<^medskip> |
61575 | 349 |
The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper for Isabelle/Scala, |
350 |
with a private protocol running over the specified TCP socket. Isabelle/ML |
|
351 |
and Isabelle/Scala provide various programming interfaces to invoke protocol |
|
352 |
functions over untyped strings and XML trees. |
|
28215 | 353 |
|
61406 | 354 |
\<^medskip> |
61575 | 355 |
The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more secure by disabling some |
356 |
critical operations, notably runtime compilation and evaluation of ML source |
|
357 |
code. |
|
58618 | 358 |
\<close> |
28215 | 359 |
|
360 |
||
58618 | 361 |
subsubsection \<open>Examples\<close> |
28215 | 362 |
|
58618 | 363 |
text \<open> |
61575 | 364 |
Run an interactive session of the default object-logic (as specified by the |
365 |
@{setting ISABELLE_LOGIC} setting) like this: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
366 |
@{verbatim [display] \<open>isabelle_process\<close>} |
28215 | 367 |
|
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
368 |
\<^medskip> |
61575 | 369 |
The next example demonstrates batch execution of Isabelle. We retrieve the |
370 |
\<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate |
|
371 |
quoting rules for the Bash shell vs.\ ML): |
|
62511 | 372 |
@{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' -q HOL\<close>} |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
373 |
|
61575 | 374 |
Note that the output text will be interspersed with additional junk messages |
62475
43e64c770f28
isabelle_process executable no longer supports writable heap images;
wenzelm
parents:
62451
diff
changeset
|
375 |
by the ML runtime environment. |
58618 | 376 |
\<close> |
28238 | 377 |
|
378 |
||
58618 | 379 |
section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close> |
28238 | 380 |
|
58618 | 381 |
text \<open> |
61575 | 382 |
All Isabelle related tools and interfaces are called via a common wrapper |
383 |
--- @{executable isabelle}: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
384 |
@{verbatim [display] |
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
385 |
\<open>Usage: isabelle TOOL [ARGS ...] |
28238 | 386 |
|
28506 | 387 |
Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. |
28238 | 388 |
|
48858 | 389 |
Available tools: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
390 |
...\<close>} |
28238 | 391 |
|
61575 | 392 |
In principle, Isabelle tools are ordinary executable scripts that are run |
393 |
within the Isabelle settings environment, see \secref{sec:settings}. The set |
|
394 |
of available tools is collected by @{executable isabelle} from the |
|
395 |
directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to |
|
396 |
call the scripts directly from the shell. Neither should you add the tool |
|
397 |
directories to your shell's search path! |
|
58618 | 398 |
\<close> |
28238 | 399 |
|
400 |
||
58618 | 401 |
subsubsection \<open>Examples\<close> |
28238 | 402 |
|
61575 | 403 |
text \<open> |
404 |
Show the list of available documentation of the Isabelle distribution: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
405 |
@{verbatim [display] \<open>isabelle doc\<close>} |
28238 | 406 |
|
407 |
View a certain document as follows: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
408 |
@{verbatim [display] \<open>isabelle doc system\<close>} |
28238 | 409 |
|
48813 | 410 |
Query the Isabelle settings environment: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
411 |
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
58618 | 412 |
\<close> |
28215 | 413 |
|
62451 | 414 |
|
415 |
section \<open>YXML versus XML\<close> |
|
416 |
||
417 |
text \<open> |
|
418 |
Isabelle tools often use YXML, which is a simple and efficient syntax for |
|
419 |
untyped XML trees. The YXML format is defined as follows. |
|
420 |
||
421 |
\<^enum> The encoding is always UTF-8. |
|
422 |
||
423 |
\<^enum> Body text is represented verbatim (no escaping, no special treatment of |
|
424 |
white space, no named entities, no CDATA chunks, no comments). |
|
425 |
||
426 |
\<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close> |
|
427 |
and \<open>\<^bold>Y = 6\<close> as follows: |
|
428 |
||
429 |
\begin{tabular}{ll} |
|
430 |
XML & YXML \\\hline |
|
431 |
\<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> & |
|
432 |
\<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\ |
|
433 |
\<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\ |
|
434 |
\end{tabular} |
|
435 |
||
436 |
There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated |
|
437 |
like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in |
|
438 |
well-formed XML documents. |
|
439 |
||
440 |
Parsing YXML is pretty straight-forward: split the text into chunks |
|
441 |
separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>. |
|
442 |
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk |
|
443 |
indicates close of an element. Any other non-empty chunk consists of plain |
|
444 |
text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file |
|
445 |
"~~/src/Pure/PIDE/yxml.scala"}. |
|
446 |
||
447 |
YXML documents may be detected quickly by checking that the first two |
|
448 |
characters are \<open>\<^bold>X\<^bold>Y\<close>. |
|
449 |
\<close> |
|
450 |
||
28223 | 451 |
end |