author | nipkow |
Wed, 10 Jan 2018 15:25:09 +0100 | |
changeset 67399 | eab6ce8368fa |
parent 67044 | 3d81a1a67302 |
child 67904 | 465f43a9f780 |
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 |
||
63669 | 58 |
\<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (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 --- |
|
67044 | 61 |
usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2017\<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> |
76 |
A few variables are somewhat special: |
|
28215 | 77 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
78 |
\<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
79 |
name of the @{executable isabelle} executables. |
28215 | 80 |
|
61575 | 81 |
\<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle |
82 |
distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\ |
|
83 |
@{setting ML_IDENTIFIER}) appended automatically to its value. |
|
28215 | 84 |
|
61406 | 85 |
\<^medskip> |
61575 | 86 |
Note that the settings environment may be inspected with the @{tool getenv} |
87 |
tool. This might help to figure out the effect of complex settings scripts. |
|
88 |
\<close> |
|
28215 | 89 |
|
90 |
||
58618 | 91 |
subsection \<open>Common variables\<close> |
28215 | 92 |
|
58618 | 93 |
text \<open> |
61575 | 94 |
This is a reference of common Isabelle settings variables. Note that the |
95 |
list is somewhat open-ended. Third-party utilities or interfaces may add |
|
96 |
their own selection. Variables that are special in some sense are marked |
|
97 |
with \<open>\<^sup>*\<close>. |
|
28215 | 98 |
|
61575 | 99 |
\<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory. |
100 |
On Unix systems this is usually the same as @{setting HOME}, but on Windows |
|
101 |
it is the regular home directory of the user, not the one of within the |
|
102 |
Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its |
|
63669 | 103 |
HOME should point to the @{path "/home"} directory tree or the Windows user |
104 |
home.\<close> |
|
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
105 |
|
61575 | 106 |
\<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level |
107 |
Isabelle distribution directory. This is automatically determined from the |
|
108 |
Isabelle executable that has been invoked. Do not attempt to set @{setting |
|
109 |
ISABELLE_HOME} yourself from the shell! |
|
50182 | 110 |
|
61575 | 111 |
\<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of |
63669 | 112 |
@{setting ISABELLE_HOME}. The default value is relative to @{path |
61575 | 113 |
"$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the |
114 |
global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory |
|
115 |
mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide |
|
116 |
defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. |
|
117 |
||
118 |
\<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the |
|
119 |
general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that |
|
50182 | 120 |
platform-dependent tools usually need to refer to the more specific |
66732 | 121 |
identification according to @{setting ISABELLE_PLATFORM} etc. |
122 |
||
123 |
\<^descr>[@{setting_def ISABELLE_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def |
|
124 |
ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>, @{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] indicate the |
|
125 |
standard Posix platform: \<^verbatim>\<open>x86\<close> for 32 bit and \<^verbatim>\<open>x86_64\<close> for 64 bit, |
|
126 |
together with a symbolic name for the operating system (\<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>darwin\<close>, |
|
127 |
\<^verbatim>\<open>cygwin\<close>). Some platforms support both 32 bit and 64 bit executables, but |
|
128 |
this depends on various side-conditions. |
|
129 |
||
130 |
In GNU bash scripts, it is possible to use the following expressions |
|
131 |
(including the quotes) to specify a preference of 64 bit over 32 bit: |
|
132 |
||
133 |
@{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"\<close>} |
|
50182 | 134 |
|
66732 | 135 |
In contrast, the subsequent expression prefers the 32 bit variant; this is |
136 |
how @{setting ISABELLE_PLATFORM} is defined: |
|
137 |
||
138 |
@{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
|
139 |
|
66732 | 140 |
\<^descr>[@{setting_def ISABELLE_WINDOWS_PLATFORM32}\<open>\<^sup>*\<close>, @{setting_def |
141 |
ISABELLE_WINDOWS_PLATFORM64}\<open>\<^sup>*\<close>,] @{setting_def |
|
142 |
ISABELLE_WINDOWS_PLATFORM}\<open>\<^sup>*\<close> indicate the native Windows platform. These |
|
143 |
settings are analogous (but independent) of those for the standard Posix |
|
144 |
subsystem: @{setting ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}, |
|
145 |
@{setting ISABELLE_PLATFORM}. |
|
47823 | 146 |
|
66732 | 147 |
In GNU bash scripts, a preference for native Windows platform variants may |
148 |
be specified like this: |
|
149 |
||
150 |
@{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM:-$ISABELLE_PLATFORM}"\<close>} |
|
151 |
||
152 |
@{verbatim [display] \<open>"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${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
|
153 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
154 |
\<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name |
66787 | 155 |
of the @{executable isabelle} executable. |
28215 | 156 |
|
61575 | 157 |
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this |
66785 | 158 |
Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017\<close>''. |
61575 | 159 |
|
160 |
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def |
|
161 |
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>] |
|
162 |
specify the underlying ML system to be used for Isabelle. There is only a |
|
63680 | 163 |
fixed set of admissable @{setting ML_SYSTEM} names (see the |
164 |
\<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution). |
|
61575 | 165 |
|
28215 | 166 |
The actual compiler binary will be run from the directory @{setting |
61575 | 167 |
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line. |
168 |
The optional @{setting ML_PLATFORM} may specify the binary format of ML heap |
|
169 |
images, which is useful for cross-platform installations. The value of |
|
170 |
@{setting ML_IDENTIFIER} is automatically obtained by composing the values |
|
171 |
of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version |
|
172 |
values. |
|
47823 | 173 |
|
66733 | 174 |
\<^descr>[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development |
175 |
Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. Note that |
|
176 |
conventional \<^verbatim>\<open>JAVA_HOME\<close> points to the JRE (Java Runtime Environment), not |
|
177 |
the JDK. |
|
178 |
||
179 |
\<^descr>[@{setting_def ISABELLE_JAVA_PLATFORM}] identifies the hardware and |
|
180 |
operating system platform for the Java installation of Isabelle. That is |
|
66906 | 181 |
always the (native) 64 bit variant: \<^verbatim>\<open>x86_64-linux\<close>, \<^verbatim>\<open>x86_64-darwin\<close>, |
66733 | 182 |
\<^verbatim>\<open>x86_64-windows\<close>. |
61575 | 183 |
|
184 |
\<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by |
|
185 |
colons) where Isabelle logic images may reside. When looking up heaps files, |
|
186 |
the value of @{setting ML_IDENTIFIER} is appended to each component |
|
187 |
internally. |
|
188 |
||
189 |
\<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files |
|
190 |
should be stored by default. The ML system and Isabelle version identifier |
|
191 |
is appended here, too. |
|
192 |
||
193 |
\<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory |
|
62013 | 194 |
browser information is stored as HTML and PDF (see also \secref{sec:info}). |
63669 | 195 |
The default value is @{path "$ISABELLE_HOME_USER/browser_info"}. |
61575 | 196 |
|
197 |
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none |
|
198 |
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>. |
|
199 |
||
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62559
diff
changeset
|
200 |
\<^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
|
201 |
@{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
|
202 |
|
61575 | 203 |
\<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, |
204 |
@{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle |
|
205 |
document preparation (see also \secref{sec:tool-latex}). |
|
206 |
||
207 |
\<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories |
|
208 |
that are scanned by @{executable isabelle} for external utility programs |
|
209 |
(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
|
210 |
|
61575 | 211 |
\<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories |
212 |
with documentation files. |
|
213 |
||
214 |
\<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying |
|
215 |
\<^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
|
216 |
|
61575 | 217 |
\<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying |
218 |
\<^verbatim>\<open>dvi\<close> files. |
|
219 |
||
220 |
\<^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
|
221 |
running Isabelle ML process derives an individual directory for temporary |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
222 |
files. |
58618 | 223 |
\<close> |
28215 | 224 |
|
225 |
||
58618 | 226 |
subsection \<open>Additional components \label{sec:components}\<close> |
32323 | 227 |
|
61575 | 228 |
text \<open> |
229 |
Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The |
|
230 |
general layout conventions are that of the main Isabelle distribution |
|
231 |
itself, and the following two files (both optional) have a special meaning: |
|
32323 | 232 |
|
61575 | 233 |
\<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when |
234 |
bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As |
|
64509 | 235 |
usual, the content is interpreted as a GNU bash script. It may refer to |
236 |
the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable. |
|
32323 | 237 |
|
61575 | 238 |
For example, the following setting allows to refer to files within the |
239 |
component later on, without having to hardwire absolute paths: |
|
240 |
@{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>} |
|
32323 | 241 |
|
61575 | 242 |
Components can also add to existing Isabelle settings such as |
243 |
@{setting_def ISABELLE_TOOLS}, in order to provide component-specific |
|
244 |
tools that can be invoked by end-users. For example: |
|
245 |
@{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>} |
|
32323 | 246 |
|
61575 | 247 |
\<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same |
248 |
structure. The directory specifications given here can be either absolute |
|
249 |
(with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory. |
|
32323 | 250 |
|
61575 | 251 |
The root of component initialization is @{setting ISABELLE_HOME} itself. |
252 |
After initializing all of its sub-components recursively, @{setting |
|
253 |
ISABELLE_HOME_USER} is included in the same manner (if that directory |
|
63669 | 254 |
exists). This allows to install private components via @{path |
61575 | 255 |
"$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient |
256 |
to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the |
|
257 |
\<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component |
|
66947 | 258 |
directory). For example: |
259 |
@{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
|
260 |
|
61575 | 261 |
This is tolerant wrt.\ missing component directories, but might produce a |
262 |
warning. |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
263 |
|
61406 | 264 |
\<^medskip> |
61575 | 265 |
More complex situations may be addressed by initializing components listed |
266 |
in a given catalog file, relatively to some base directory: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
267 |
@{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
|
268 |
|
61575 | 269 |
The component directories listed in the catalog file are treated as relative |
270 |
to the given base directory. |
|
48844 | 271 |
|
61575 | 272 |
See also \secref{sec:tool-components} for some tool-support for resolving |
273 |
components that are formally initialized but not installed yet. |
|
58618 | 274 |
\<close> |
32323 | 275 |
|
276 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
277 |
section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close> |
28215 | 278 |
|
58618 | 279 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
280 |
The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for |
64509 | 281 |
Isabelle-related utilities, user interfaces, add-on applications etc. Such |
282 |
tools automatically benefit from the settings mechanism |
|
283 |
(\secref{sec:settings}). Moreover, this is the standard way to invoke |
|
284 |
Isabelle/Scala functionality as a separate operating-system process. |
|
285 |
Isabelle command-line tools are run uniformly via a common wrapper --- |
|
286 |
@{executable_ref isabelle}: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
287 |
@{verbatim [display] |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
288 |
\<open>Usage: isabelle TOOL [ARGS ...] |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
289 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62677
diff
changeset
|
290 |
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
|
291 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
292 |
Available tools: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
293 |
...\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
294 |
|
64509 | 295 |
Tools may be implemented in Isabelle/Scala or as stand-alone executables |
296 |
(usually as GNU bash scripts). In the invocation of ``@{executable |
|
297 |
isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the |
|
298 |
given order). |
|
299 |
||
300 |
\<^enum> An external tool found on the directories listed in the @{setting |
|
301 |
ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX |
|
302 |
notation). |
|
303 |
||
304 |
\<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define |
|
305 |
some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala |
|
306 |
compiler is invoked on the spot (which may take some time), and the body |
|
307 |
function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>. |
|
308 |
||
309 |
\<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as |
|
310 |
stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close> |
|
311 |
array. |
|
312 |
||
313 |
\<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close> |
|
314 |
within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred |
|
315 |
entry-point for high-end tools implemented in Isabelle/Scala --- compiled |
|
316 |
once when the Isabelle distribution is built. These tools are provided by |
|
317 |
Isabelle/Pure and cannot be augmented in user-space. |
|
318 |
||
319 |
There are also some administrative tools that are available from a bare |
|
320 |
repository clone of Isabelle, but not in regular distributions. |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
321 |
\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
322 |
|
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 |
subsubsection \<open>Examples\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
325 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
326 |
text \<open> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
327 |
Show the list of available documentation of the Isabelle distribution: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
328 |
@{verbatim [display] \<open>isabelle doc\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
329 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
330 |
View a certain document as follows: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
331 |
@{verbatim [display] \<open>isabelle doc system\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
332 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
333 |
Query the Isabelle settings environment: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
334 |
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
335 |
\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
336 |
|
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 |
section \<open>The raw Isabelle ML process\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
339 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
340 |
subsection \<open>Batch mode \label{sec:tool-process}\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
341 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
342 |
text \<open> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
343 |
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
|
344 |
@{verbatim [display] |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
345 |
\<open>Usage: isabelle process [OPTIONS] |
28215 | 346 |
|
347 |
Options are: |
|
62677 | 348 |
-T THEORY load theory |
62639 | 349 |
-d DIR include session directory |
62506 | 350 |
-e ML_EXPR evaluate ML expression on startup |
351 |
-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
|
352 |
-l NAME logic session name (default ISABELLE_LOGIC="HOL") |
28215 | 353 |
-m MODE add print mode for output |
52056 | 354 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
28215 | 355 |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
356 |
Run the raw Isabelle ML process in batch mode.\<close>} |
28215 | 357 |
|
62643 | 358 |
\<^medskip> |
62506 | 359 |
Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is |
360 |
started. The source is either given literally or taken from a file. Multiple |
|
361 |
\<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to |
|
362 |
premature exit of the ML process with return code 1. |
|
28215 | 363 |
|
61406 | 364 |
\<^medskip> |
62677 | 365 |
Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with |
366 |
a suitable @{ML use_thy} invocation. |
|
367 |
||
368 |
\<^medskip> |
|
62639 | 369 |
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies |
370 |
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
|
371 |
|
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
372 |
\<^medskip> |
61575 | 373 |
The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this |
62573 | 374 |
session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over |
375 |
mathematical Isabelle symbols. |
|
28215 | 376 |
|
61406 | 377 |
\<^medskip> |
61575 | 378 |
Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process, |
62573 | 379 |
see also \secref{sec:system-options}. |
58618 | 380 |
\<close> |
28215 | 381 |
|
382 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
383 |
subsubsection \<open>Example\<close> |
28215 | 384 |
|
58618 | 385 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
386 |
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
|
387 |
loader within ML: |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
388 |
@{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
|
389 |
|
64509 | 390 |
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
|
391 |
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
|
392 |
to do it manually. |
58618 | 393 |
\<close> |
28238 | 394 |
|
395 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
396 |
subsection \<open>Interactive mode\<close> |
28238 | 397 |
|
58618 | 398 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
399 |
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
|
400 |
console and line editor: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
401 |
@{verbatim [display] |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
402 |
\<open>Usage: isabelle console [OPTIONS] |
28238 | 403 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
404 |
Options are: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
405 |
-d DIR include session directory |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
406 |
-l NAME logic session name (default ISABELLE_LOGIC) |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
407 |
-m MODE add print mode for output |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
408 |
-n no build of session image on startup |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
409 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
62643 | 410 |
-r bootstrap from raw Poly/ML |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
411 |
-s system build mode for session image |
28238 | 412 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
413 |
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
|
414 |
in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>} |
28238 | 415 |
|
62643 | 416 |
\<^medskip> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
417 |
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is |
62643 | 418 |
checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. |
28238 | 419 |
|
62643 | 420 |
Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is |
421 |
relevant for Isabelle/Pure development. |
|
422 |
||
423 |
\<^medskip> |
|
62639 | 424 |
Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process} |
425 |
(\secref{sec:tool-process}). |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
426 |
|
62639 | 427 |
Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build} |
428 |
(\secref{sec:tool-build}). |
|
28238 | 429 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
430 |
\<^medskip> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
431 |
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
|
432 |
the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\ |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
433 |
@{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
|
434 |
standard input/output. |
28238 | 435 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
436 |
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
|
437 |
Isabelle/Isar nor Isabelle/ML within the usual formal context. The most |
62847 | 438 |
relevant ML commands at this stage are @{ML use} (for ML files) and |
439 |
@{ML use_thy} (for theory files). |
|
58618 | 440 |
\<close> |
28215 | 441 |
|
62451 | 442 |
|
63995 | 443 |
section \<open>The raw Isabelle Java process \label{sec:isabelle-java}\<close> |
444 |
||
445 |
text \<open> |
|
446 |
The @{executable_ref isabelle_java} executable allows to run a Java process |
|
447 |
within the name space of Java and Scala components that are bundled with |
|
448 |
Isabelle, but \<^emph>\<open>without\<close> the Isabelle settings environment |
|
449 |
(\secref{sec:settings}). |
|
450 |
||
451 |
After such a JVM cold-start, the Isabelle environment can be accessed via |
|
452 |
\<^verbatim>\<open>Isabelle_System.getenv\<close> as usual, but the underlying process environment |
|
453 |
remains clean. This is e.g.\ relevant when invoking other processes that |
|
454 |
should remain separate from the current Isabelle installation. |
|
455 |
||
456 |
\<^medskip> |
|
457 |
Note that under normal circumstances, Isabelle command-line tools are run |
|
458 |
\<^emph>\<open>within\<close> the settings environment, as provided by the @{executable |
|
459 |
isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}). |
|
460 |
\<close> |
|
461 |
||
462 |
||
463 |
subsubsection \<open>Example\<close> |
|
464 |
||
465 |
text \<open> |
|
466 |
The subsequent example creates a raw Java process on the command-line and |
|
467 |
invokes the main Isabelle application entry point: |
|
468 |
@{verbatim [display] \<open>isabelle_java isabelle.Main\<close>} |
|
469 |
\<close> |
|
470 |
||
471 |
||
62451 | 472 |
section \<open>YXML versus XML\<close> |
473 |
||
474 |
text \<open> |
|
475 |
Isabelle tools often use YXML, which is a simple and efficient syntax for |
|
476 |
untyped XML trees. The YXML format is defined as follows. |
|
477 |
||
478 |
\<^enum> The encoding is always UTF-8. |
|
479 |
||
480 |
\<^enum> Body text is represented verbatim (no escaping, no special treatment of |
|
481 |
white space, no named entities, no CDATA chunks, no comments). |
|
482 |
||
483 |
\<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close> |
|
484 |
and \<open>\<^bold>Y = 6\<close> as follows: |
|
485 |
||
486 |
\begin{tabular}{ll} |
|
487 |
XML & YXML \\\hline |
|
488 |
\<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> & |
|
489 |
\<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\ |
|
490 |
\<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\ |
|
491 |
\end{tabular} |
|
492 |
||
493 |
There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated |
|
494 |
like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in |
|
495 |
well-formed XML documents. |
|
496 |
||
497 |
Parsing YXML is pretty straight-forward: split the text into chunks |
|
498 |
separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>. |
|
499 |
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk |
|
500 |
indicates close of an element. Any other non-empty chunk consists of plain |
|
63680 | 501 |
text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or |
502 |
\<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>. |
|
62451 | 503 |
|
504 |
YXML documents may be detected quickly by checking that the first two |
|
505 |
characters are \<open>\<^bold>X\<^bold>Y\<close>. |
|
506 |
\<close> |
|
507 |
||
67399 | 508 |
end |