author | wenzelm |
Fri, 11 Sep 2020 12:17:19 +0200 | |
changeset 72252 | 3b17e7688dc6 |
parent 71904 | 70442ddbfb15 |
child 72309 | 564012e31db1 |
permissions | -rw-r--r-- |
66732 | 1 |
(*:maxLineLen=78:*) |
61575 | 2 |
|
62640 | 3 |
theory Environment |
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> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
10 |
This manual describes Isabelle together with related tools as seen from a |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
11 |
system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
12 |
"isabelle-isar-ref"} for the actual Isabelle input language and related |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
13 |
concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
14 |
"isabelle-implementation"} for the main concepts of the underlying |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
15 |
implementation in Isabelle/ML. |
58618 | 16 |
\<close> |
28215 | 17 |
|
18 |
||
58618 | 19 |
section \<open>Isabelle settings \label{sec:settings}\<close> |
28215 | 20 |
|
58618 | 21 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
22 |
Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
23 |
process environment. This is a statically scoped collection of environment |
62013 | 24 |
variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting |
25 |
ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
26 |
shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
27 |
explained below. |
58618 | 28 |
\<close> |
28215 | 29 |
|
30 |
||
58618 | 31 |
subsection \<open>Bootstrapping the environment \label{sec:boot}\<close> |
28215 | 32 |
|
61575 | 33 |
text \<open> |
34 |
Isabelle executables need to be run within a proper settings environment. |
|
35 |
This is bootstrapped as described below, on the first invocation of one of |
|
36 |
the outer wrapper scripts (such as @{executable_ref isabelle}). This happens |
|
37 |
only once for each process tree, i.e.\ the environment is passed to |
|
38 |
subprocesses according to regular Unix conventions. |
|
39 |
||
40 |
\<^enum> The special variable @{setting_def ISABELLE_HOME} is determined |
|
41 |
automatically from the location of the binary that has been run. |
|
28215 | 42 |
|
61575 | 43 |
You should not try to set @{setting ISABELLE_HOME} manually. Also note |
44 |
that the Isabelle executables either have to be run from their original |
|
45 |
location in the distribution directory, or via the executable objects |
|
46 |
created by the @{tool install} tool. Symbolic links are admissible, but a |
|
63680 | 47 |
plain copy of the \<^dir>\<open>$ISABELLE_HOME/bin\<close> files will not work! |
61575 | 48 |
|
63680 | 49 |
\<^enum> The file \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> is run as a @{executable_ref |
50 |
bash} shell script with the auto-export option for variables enabled. |
|
28238 | 51 |
|
61575 | 52 |
This file holds a rather long list of shell variable assignments, thus |
53 |
providing the site-wide default settings. The Isabelle distribution |
|
54 |
already contains a global settings file with sensible defaults for most |
|
55 |
variables. When installing the system, only a few of these may have to be |
|
56 |
adapted (probably @{setting ML_SYSTEM} etc.). |
|
57 |
||
69593 | 58 |
\<^enum> The file \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close> (if it |
61575 | 59 |
exists) is run in the same way as the site default settings. Note that the |
60 |
variable @{setting ISABELLE_HOME_USER} has already been set before --- |
|
71578 | 61 |
usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2020\<close>. |
61458 | 62 |
|
61575 | 63 |
Thus individual users may override the site-wide defaults. Typically, a |
64 |
user settings file contains only a few lines, with some assignments that |
|
63680 | 65 |
are actually changed. Never copy the central |
66 |
\<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file! |
|
28215 | 67 |
|
61575 | 68 |
Since settings files are regular GNU @{executable_def bash} scripts, one may |
69 |
use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set |
|
70 |
variables depending on the system architecture or other environment |
|
71 |
variables. Such advanced features should be added only with great care, |
|
72 |
though. In particular, external environment references should be kept at a |
|
28215 | 73 |
minimum. |
74 |
||
61406 | 75 |
\<^medskip> |
68514 | 76 |
A few variables are somewhat special, e.g.\ @{setting_def ISABELLE_TOOL} is |
68219 | 77 |
set automatically to the absolute path name of the @{executable isabelle} |
78 |
executables. |
|
28215 | 79 |
|
61406 | 80 |
\<^medskip> |
61575 | 81 |
Note that the settings environment may be inspected with the @{tool getenv} |
82 |
tool. This might help to figure out the effect of complex settings scripts. |
|
83 |
\<close> |
|
28215 | 84 |
|
85 |
||
58618 | 86 |
subsection \<open>Common variables\<close> |
28215 | 87 |
|
58618 | 88 |
text \<open> |
61575 | 89 |
This is a reference of common Isabelle settings variables. Note that the |
90 |
list is somewhat open-ended. Third-party utilities or interfaces may add |
|
91 |
their own selection. Variables that are special in some sense are marked |
|
92 |
with \<open>\<^sup>*\<close>. |
|
28215 | 93 |
|
61575 | 94 |
\<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory. |
95 |
On Unix systems this is usually the same as @{setting HOME}, but on Windows |
|
96 |
it is the regular home directory of the user, not the one of within the |
|
97 |
Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its |
|
69593 | 98 |
HOME should point to the \<^path>\<open>/home\<close> directory tree or the Windows user |
63669 | 99 |
home.\<close> |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
100 |
|
61575 | 101 |
\<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level |
102 |
Isabelle distribution directory. This is automatically determined from the |
|
103 |
Isabelle executable that has been invoked. Do not attempt to set @{setting |
|
104 |
ISABELLE_HOME} yourself from the shell! |
|
50182 | 105 |
|
61575 | 106 |
\<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of |
69593 | 107 |
@{setting ISABELLE_HOME}. The default value is relative to \<^path>\<open>$USER_HOME/.isabelle\<close>, under rare circumstances this may be changed in the |
61575 | 108 |
global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory |
109 |
mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide |
|
110 |
defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. |
|
111 |
||
112 |
\<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the |
|
113 |
general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that |
|
50182 | 114 |
platform-dependent tools usually need to refer to the more specific |
68003 | 115 |
identification according to @{setting ISABELLE_PLATFORM64}, @{setting |
116 |
ISABELLE_PLATFORM32}, @{setting ISABELLE_WINDOWS_PLATFORM64}, @{setting |
|
117 |
ISABELLE_WINDOWS_PLATFORM32}. |
|
66732 | 118 |
|
68003 | 119 |
\<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def |
120 |
ISABELLE_PLATFORM32}\<open>\<^sup>*\<close>] indicate the standard Posix platform: \<^verbatim>\<open>x86_64\<close> |
|
121 |
for 64 bit and \<^verbatim>\<open>x86\<close> for 32 bit, together with a symbolic name for the |
|
122 |
operating system (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>darwin\<close>, \<^verbatim>\<open>cygwin\<close>). All platforms support 64 |
|
123 |
bit executables, some platforms also support 32 bit executables. |
|
66732 | 124 |
|
68003 | 125 |
In GNU bash scripts, it is possible to use the following expressions (with |
126 |
quotes) to specify a preference of 64 bit over 32 bit: |
|
66732 | 127 |
|
128 |
@{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\<close>} |
|
50182 | 129 |
|
68003 | 130 |
In contrast, the subsequent expression prefers the old 32 bit variant (which |
131 |
is only relevant for unusual applications): |
|
66732 | 132 |
|
133 |
@{verbatim [display] \<open>"${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"\<close>} |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
134 |
|
68003 | 135 |
\<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def |
136 |
ISABELLE_WINDOWS_PLATFORM32}\<open>\<^sup>*\<close>] indicate the native Windows platform. |
|
137 |
These settings are analogous (but independent) of those for the standard |
|
138 |
Posix subsystem: @{setting ISABELLE_PLATFORM64}, @{setting |
|
139 |
ISABELLE_PLATFORM32}. |
|
47823 | 140 |
|
66732 | 141 |
In GNU bash scripts, a preference for native Windows platform variants may |
68003 | 142 |
be specified like this (first 64 bit, second 32 bit): |
66732 | 143 |
|
68003 | 144 |
@{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:- |
145 |
${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"\<close>} |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
146 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
147 |
\<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name |
66787 | 148 |
of the @{executable isabelle} executable. |
28215 | 149 |
|
61575 | 150 |
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this |
71578 | 151 |
Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020\<close>''. |
61575 | 152 |
|
153 |
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def |
|
154 |
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>] |
|
155 |
specify the underlying ML system to be used for Isabelle. There is only a |
|
63680 | 156 |
fixed set of admissable @{setting ML_SYSTEM} names (see the |
157 |
\<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution). |
|
61575 | 158 |
|
28215 | 159 |
The actual compiler binary will be run from the directory @{setting |
61575 | 160 |
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line. |
161 |
The optional @{setting ML_PLATFORM} may specify the binary format of ML heap |
|
162 |
images, which is useful for cross-platform installations. The value of |
|
163 |
@{setting ML_IDENTIFIER} is automatically obtained by composing the values |
|
164 |
of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version |
|
165 |
values. |
|
47823 | 166 |
|
66733 | 167 |
\<^descr>[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development |
168 |
Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. Note that |
|
169 |
conventional \<^verbatim>\<open>JAVA_HOME\<close> points to the JRE (Java Runtime Environment), not |
|
170 |
the JDK. |
|
171 |
||
172 |
\<^descr>[@{setting_def ISABELLE_JAVA_PLATFORM}] identifies the hardware and |
|
173 |
operating system platform for the Java installation of Isabelle. That is |
|
66906 | 174 |
always the (native) 64 bit variant: \<^verbatim>\<open>x86_64-linux\<close>, \<^verbatim>\<open>x86_64-darwin\<close>, |
66733 | 175 |
\<^verbatim>\<open>x86_64-windows\<close>. |
61575 | 176 |
|
68523
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68514
diff
changeset
|
177 |
\<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where HTML and PDF |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68514
diff
changeset
|
178 |
browser information is stored (see also \secref{sec:info}); its default is |
69593 | 179 |
\<^path>\<open>$ISABELLE_HOME_USER/browser_info\<close>. For ``system build mode'' (see |
68523
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68514
diff
changeset
|
180 |
\secref{sec:tool-build}), @{setting_def ISABELLE_BROWSER_INFO_SYSTEM} is |
69593 | 181 |
used instead; its default is \<^path>\<open>$ISABELLE_HOME/browser_info\<close>. |
68523
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68514
diff
changeset
|
182 |
|
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68514
diff
changeset
|
183 |
\<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images, |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69593
diff
changeset
|
184 |
log files, and build databases are stored; its default is |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69593
diff
changeset
|
185 |
\<^path>\<open>$ISABELLE_HOME_USER/heaps\<close>. If @{system_option system_heaps} is |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69593
diff
changeset
|
186 |
\<^verbatim>\<open>true\<close>, @{setting_def ISABELLE_HEAPS_SYSTEM} is used instead; its default |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69593
diff
changeset
|
187 |
is \<^path>\<open>$ISABELLE_HOME/heaps\<close>. See also \secref{sec:tool-build}. |
61575 | 188 |
|
189 |
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none |
|
190 |
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>. |
|
191 |
||
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62559
diff
changeset
|
192 |
\<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the |
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62559
diff
changeset
|
193 |
@{tool_ref console} interface. |
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62559
diff
changeset
|
194 |
|
61575 | 195 |
\<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, |
196 |
@{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle |
|
197 |
document preparation (see also \secref{sec:tool-latex}). |
|
198 |
||
199 |
\<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories |
|
200 |
that are scanned by @{executable isabelle} for external utility programs |
|
201 |
(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
|
202 |
|
61575 | 203 |
\<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories |
204 |
with documentation files. |
|
205 |
||
206 |
\<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying |
|
207 |
\<^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
|
208 |
|
61575 | 209 |
\<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying |
210 |
\<^verbatim>\<open>dvi\<close> files. |
|
211 |
||
212 |
\<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
213 |
running Isabelle ML process derives an individual directory for temporary |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
214 |
files. |
68477 | 215 |
|
216 |
\<^descr>[@{setting_def ISABELLE_TOOL_JAVA_OPTIONS}] is passed to the \<^verbatim>\<open>java\<close> |
|
68514 | 217 |
executable when running Isabelle tools (e.g.\ @{tool build}). This is |
68477 | 218 |
occasionally helpful to provide more heap space, via additional options like |
219 |
\<^verbatim>\<open>-Xms1g -Xmx4g\<close>. |
|
58618 | 220 |
\<close> |
28215 | 221 |
|
222 |
||
58618 | 223 |
subsection \<open>Additional components \label{sec:components}\<close> |
32323 | 224 |
|
61575 | 225 |
text \<open> |
226 |
Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The |
|
227 |
general layout conventions are that of the main Isabelle distribution |
|
228 |
itself, and the following two files (both optional) have a special meaning: |
|
32323 | 229 |
|
61575 | 230 |
\<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when |
231 |
bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As |
|
64509 | 232 |
usual, the content is interpreted as a GNU bash script. It may refer to |
233 |
the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable. |
|
32323 | 234 |
|
61575 | 235 |
For example, the following setting allows to refer to files within the |
236 |
component later on, without having to hardwire absolute paths: |
|
237 |
@{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>} |
|
32323 | 238 |
|
61575 | 239 |
Components can also add to existing Isabelle settings such as |
240 |
@{setting_def ISABELLE_TOOLS}, in order to provide component-specific |
|
241 |
tools that can be invoked by end-users. For example: |
|
242 |
@{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>} |
|
32323 | 243 |
|
61575 | 244 |
\<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same |
245 |
structure. The directory specifications given here can be either absolute |
|
246 |
(with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory. |
|
32323 | 247 |
|
61575 | 248 |
The root of component initialization is @{setting ISABELLE_HOME} itself. |
249 |
After initializing all of its sub-components recursively, @{setting |
|
250 |
ISABELLE_HOME_USER} is included in the same manner (if that directory |
|
71904 | 251 |
exists). This allows to install private components via |
252 |
\<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>, although it is often more |
|
253 |
convenient to do that programmatically via the |
|
254 |
\<^bash_function>\<open>init_component\<close> shell function in the \<^verbatim>\<open>etc/settings\<close> |
|
255 |
script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component directory). For |
|
256 |
example: |
|
66947 | 257 |
@{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
|
258 |
|
61575 | 259 |
This is tolerant wrt.\ missing component directories, but might produce a |
260 |
warning. |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
261 |
|
61406 | 262 |
\<^medskip> |
61575 | 263 |
More complex situations may be addressed by initializing components listed |
264 |
in a given catalog file, relatively to some base directory: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
265 |
@{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
|
266 |
|
61575 | 267 |
The component directories listed in the catalog file are treated as relative |
268 |
to the given base directory. |
|
48844 | 269 |
|
61575 | 270 |
See also \secref{sec:tool-components} for some tool-support for resolving |
271 |
components that are formally initialized but not installed yet. |
|
58618 | 272 |
\<close> |
32323 | 273 |
|
274 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
275 |
section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close> |
28215 | 276 |
|
58618 | 277 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
278 |
The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for |
64509 | 279 |
Isabelle-related utilities, user interfaces, add-on applications etc. Such |
280 |
tools automatically benefit from the settings mechanism |
|
281 |
(\secref{sec:settings}). Moreover, this is the standard way to invoke |
|
282 |
Isabelle/Scala functionality as a separate operating-system process. |
|
283 |
Isabelle command-line tools are run uniformly via a common wrapper --- |
|
284 |
@{executable_ref isabelle}: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
285 |
@{verbatim [display] |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
286 |
\<open>Usage: isabelle TOOL [ARGS ...] |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
287 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62677
diff
changeset
|
288 |
Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
289 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
290 |
Available tools: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
291 |
...\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
292 |
|
64509 | 293 |
Tools may be implemented in Isabelle/Scala or as stand-alone executables |
294 |
(usually as GNU bash scripts). In the invocation of ``@{executable |
|
295 |
isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the |
|
296 |
given order). |
|
297 |
||
298 |
\<^enum> An external tool found on the directories listed in the @{setting |
|
299 |
ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX |
|
300 |
notation). |
|
301 |
||
302 |
\<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define |
|
303 |
some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala |
|
304 |
compiler is invoked on the spot (which may take some time), and the body |
|
305 |
function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>. |
|
306 |
||
307 |
\<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as |
|
308 |
stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close> |
|
309 |
array. |
|
310 |
||
72252 | 311 |
\<^enum> An internal tool that is registered in \<^verbatim>\<open>etc/settings\<close> via the shell |
312 |
function \<^bash_function>\<open>isabelle_scala_service\<close>, referring to a |
|
313 |
suitable instance of class \<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close>. |
|
314 |
This is the preferred approach for non-trivial systems programming in |
|
315 |
Isabelle/Scala: instead of adhoc interpretation of \<^verbatim>\<open>scala\<close> scripts, |
|
316 |
which is somewhat slow and only type-checked at runtime, there are |
|
317 |
properly compiled \<^verbatim>\<open>jar\<close> modules (see also the shell function |
|
318 |
\<^bash_function>\<open>classpath\<close> in \secref{sec:scala}). |
|
64509 | 319 |
|
72252 | 320 |
There are also various administrative tools that are available from a bare |
64509 | 321 |
repository clone of Isabelle, but not in regular distributions. |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
322 |
\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
323 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
324 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
325 |
subsubsection \<open>Examples\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
326 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
327 |
text \<open> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
328 |
Show the list of available documentation of the Isabelle distribution: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
329 |
@{verbatim [display] \<open>isabelle doc\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
330 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
331 |
View a certain document as follows: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
332 |
@{verbatim [display] \<open>isabelle doc system\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
333 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
334 |
Query the Isabelle settings environment: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
335 |
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
336 |
\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
337 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
338 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
339 |
section \<open>The raw Isabelle ML process\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
340 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
341 |
subsection \<open>Batch mode \label{sec:tool-process}\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
342 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
343 |
text \<open> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
344 |
The @{tool_def process} tool runs the raw ML process in batch mode: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
345 |
@{verbatim [display] |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
346 |
\<open>Usage: isabelle process [OPTIONS] |
28215 | 347 |
|
348 |
Options are: |
|
62677 | 349 |
-T THEORY load theory |
62639 | 350 |
-d DIR include session directory |
62506 | 351 |
-e ML_EXPR evaluate ML expression on startup |
352 |
-f ML_FILE evaluate ML file on startup |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
353 |
-l NAME logic session name (default ISABELLE_LOGIC="HOL") |
28215 | 354 |
-m MODE add print mode for output |
52056 | 355 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
28215 | 356 |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
357 |
Run the raw Isabelle ML process in batch mode.\<close>} |
28215 | 358 |
|
62643 | 359 |
\<^medskip> |
62506 | 360 |
Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is |
361 |
started. The source is either given literally or taken from a file. Multiple |
|
362 |
\<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to |
|
363 |
premature exit of the ML process with return code 1. |
|
28215 | 364 |
|
61406 | 365 |
\<^medskip> |
62677 | 366 |
Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with |
69593 | 367 |
a suitable \<^ML>\<open>use_thy\<close> invocation. |
62677 | 368 |
|
369 |
\<^medskip> |
|
62639 | 370 |
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies |
371 |
additional directories for session roots, see also \secref{sec:tool-build}. |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
372 |
|
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
373 |
\<^medskip> |
61575 | 374 |
The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this |
62573 | 375 |
session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over |
376 |
mathematical Isabelle symbols. |
|
28215 | 377 |
|
61406 | 378 |
\<^medskip> |
61575 | 379 |
Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process, |
62573 | 380 |
see also \secref{sec:system-options}. |
58618 | 381 |
\<close> |
28215 | 382 |
|
383 |
||
68275 | 384 |
subsubsection \<open>Examples\<close> |
28215 | 385 |
|
58618 | 386 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
387 |
The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
388 |
loader within ML: |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
389 |
@{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>} |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
390 |
|
64509 | 391 |
Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
392 |
Isabelle/ML and Scala libraries provide functions for that, but here we need |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
393 |
to do it manually. |
68275 | 394 |
|
395 |
\<^medskip> |
|
396 |
This is how to invoke a function body with proper return code and printing |
|
397 |
of errors, and without printing of a redundant \<^verbatim>\<open>val it = (): unit\<close> result: |
|
71632 | 398 |
@{verbatim [display] \<open>isabelle process -e 'Command_Line.tool (fn () => writeln "OK")'\<close>} |
399 |
@{verbatim [display] \<open>isabelle process -e 'Command_Line.tool (fn () => error "Bad")'\<close>} |
|
58618 | 400 |
\<close> |
28238 | 401 |
|
402 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
403 |
subsection \<open>Interactive mode\<close> |
28238 | 404 |
|
58618 | 405 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
406 |
The @{tool_def console} tool runs the raw ML process with interactive |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
407 |
console and line editor: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
408 |
@{verbatim [display] |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
409 |
\<open>Usage: isabelle console [OPTIONS] |
28238 | 410 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
411 |
Options are: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
412 |
-d DIR include session directory |
68541 | 413 |
-i NAME include session in name-space of theories |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
414 |
-l NAME logic session name (default ISABELLE_LOGIC) |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
415 |
-m MODE add print mode for output |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
416 |
-n no build of session image on startup |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
417 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
62643 | 418 |
-r bootstrap from raw Poly/ML |
28238 | 419 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
420 |
Build a logic session image and run the raw Isabelle ML process |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
421 |
in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>} |
28238 | 422 |
|
62643 | 423 |
\<^medskip> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
424 |
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is |
62643 | 425 |
checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. |
28238 | 426 |
|
68541 | 427 |
Option \<^verbatim>\<open>-i\<close> includes additional sessions into the name-space of theories: |
428 |
multiple occurrences are possible. |
|
429 |
||
62643 | 430 |
Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is |
431 |
relevant for Isabelle/Pure development. |
|
432 |
||
433 |
\<^medskip> |
|
62639 | 434 |
Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process} |
435 |
(\secref{sec:tool-process}). |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
436 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
437 |
\<^medskip> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
438 |
The Isabelle/ML process is run through the line editor that is specified via |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
439 |
the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\ |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
440 |
@{executable_def rlwrap} for GNU readline); the fall-back is to use plain |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
441 |
standard input/output. |
28238 | 442 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
443 |
The user is connected to the raw ML toplevel loop: this is neither |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
444 |
Isabelle/Isar nor Isabelle/ML within the usual formal context. The most |
69593 | 445 |
relevant ML commands at this stage are \<^ML>\<open>use\<close> (for ML files) and |
446 |
\<^ML>\<open>use_thy\<close> (for theory files). |
|
58618 | 447 |
\<close> |
28215 | 448 |
|
62451 | 449 |
|
63995 | 450 |
section \<open>The raw Isabelle Java process \label{sec:isabelle-java}\<close> |
451 |
||
452 |
text \<open> |
|
453 |
The @{executable_ref isabelle_java} executable allows to run a Java process |
|
454 |
within the name space of Java and Scala components that are bundled with |
|
455 |
Isabelle, but \<^emph>\<open>without\<close> the Isabelle settings environment |
|
456 |
(\secref{sec:settings}). |
|
457 |
||
458 |
After such a JVM cold-start, the Isabelle environment can be accessed via |
|
459 |
\<^verbatim>\<open>Isabelle_System.getenv\<close> as usual, but the underlying process environment |
|
460 |
remains clean. This is e.g.\ relevant when invoking other processes that |
|
461 |
should remain separate from the current Isabelle installation. |
|
462 |
||
463 |
\<^medskip> |
|
464 |
Note that under normal circumstances, Isabelle command-line tools are run |
|
465 |
\<^emph>\<open>within\<close> the settings environment, as provided by the @{executable |
|
466 |
isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}). |
|
467 |
\<close> |
|
468 |
||
469 |
||
470 |
subsubsection \<open>Example\<close> |
|
471 |
||
472 |
text \<open> |
|
473 |
The subsequent example creates a raw Java process on the command-line and |
|
474 |
invokes the main Isabelle application entry point: |
|
475 |
@{verbatim [display] \<open>isabelle_java isabelle.Main\<close>} |
|
476 |
\<close> |
|
477 |
||
478 |
||
67904 | 479 |
section \<open>YXML versus XML \label{sec:yxml-vs-xml}\<close> |
62451 | 480 |
|
481 |
text \<open> |
|
482 |
Isabelle tools often use YXML, which is a simple and efficient syntax for |
|
483 |
untyped XML trees. The YXML format is defined as follows. |
|
484 |
||
485 |
\<^enum> The encoding is always UTF-8. |
|
486 |
||
487 |
\<^enum> Body text is represented verbatim (no escaping, no special treatment of |
|
488 |
white space, no named entities, no CDATA chunks, no comments). |
|
489 |
||
490 |
\<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close> |
|
491 |
and \<open>\<^bold>Y = 6\<close> as follows: |
|
492 |
||
493 |
\begin{tabular}{ll} |
|
494 |
XML & YXML \\\hline |
|
495 |
\<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> & |
|
496 |
\<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\ |
|
497 |
\<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\ |
|
498 |
\end{tabular} |
|
499 |
||
500 |
There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated |
|
501 |
like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in |
|
502 |
well-formed XML documents. |
|
503 |
||
504 |
Parsing YXML is pretty straight-forward: split the text into chunks |
|
505 |
separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>. |
|
506 |
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk |
|
507 |
indicates close of an element. Any other non-empty chunk consists of plain |
|
63680 | 508 |
text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or |
509 |
\<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>. |
|
62451 | 510 |
|
511 |
YXML documents may be detected quickly by checking that the first two |
|
512 |
characters are \<open>\<^bold>X\<^bold>Y\<close>. |
|
513 |
\<close> |
|
514 |
||
67399 | 515 |
end |