author | wenzelm |
Thu, 11 Aug 2016 18:26:44 +0200 | |
changeset 63669 | 256fc20716f2 |
parent 62847 | 1bd1d8492931 |
child 63680 | 6e1e8b5abbfa |
permissions | -rw-r--r-- |
62643 | 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 |
|
63669 | 47 |
plain copy of the @{dir "$ISABELLE_HOME/bin"} files will not work! |
61575 | 48 |
|
49 |
\<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a |
|
50 |
@{executable_ref bash} shell script with the auto-export option for |
|
51 |
variables enabled. |
|
28238 | 52 |
|
61575 | 53 |
This file holds a rather long list of shell variable assignments, thus |
54 |
providing the site-wide default settings. The Isabelle distribution |
|
55 |
already contains a global settings file with sensible defaults for most |
|
56 |
variables. When installing the system, only a few of these may have to be |
|
57 |
adapted (probably @{setting ML_SYSTEM} etc.). |
|
58 |
||
63669 | 59 |
\<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it |
61575 | 60 |
exists) is run in the same way as the site default settings. Note that the |
61 |
variable @{setting ISABELLE_HOME_USER} has already been set before --- |
|
62 |
usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>. |
|
61458 | 63 |
|
61575 | 64 |
Thus individual users may override the site-wide defaults. Typically, a |
65 |
user settings file contains only a few lines, with some assignments that |
|
66 |
are actually changed. Never copy the central @{file |
|
67 |
"$ISABELLE_HOME/etc/settings"} file! |
|
28215 | 68 |
|
61575 | 69 |
Since settings files are regular GNU @{executable_def bash} scripts, one may |
70 |
use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set |
|
71 |
variables depending on the system architecture or other environment |
|
72 |
variables. Such advanced features should be added only with great care, |
|
73 |
though. In particular, external environment references should be kept at a |
|
28215 | 74 |
minimum. |
75 |
||
61406 | 76 |
\<^medskip> |
77 |
A few variables are somewhat special: |
|
28215 | 78 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
79 |
\<^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
|
80 |
name of the @{executable isabelle} executables. |
28215 | 81 |
|
61575 | 82 |
\<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle |
83 |
distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\ |
|
84 |
@{setting ML_IDENTIFIER}) appended automatically to its value. |
|
28215 | 85 |
|
61406 | 86 |
\<^medskip> |
61575 | 87 |
Note that the settings environment may be inspected with the @{tool getenv} |
88 |
tool. This might help to figure out the effect of complex settings scripts. |
|
89 |
\<close> |
|
28215 | 90 |
|
91 |
||
58618 | 92 |
subsection \<open>Common variables\<close> |
28215 | 93 |
|
58618 | 94 |
text \<open> |
61575 | 95 |
This is a reference of common Isabelle settings variables. Note that the |
96 |
list is somewhat open-ended. Third-party utilities or interfaces may add |
|
97 |
their own selection. Variables that are special in some sense are marked |
|
98 |
with \<open>\<^sup>*\<close>. |
|
28215 | 99 |
|
61575 | 100 |
\<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory. |
101 |
On Unix systems this is usually the same as @{setting HOME}, but on Windows |
|
102 |
it is the regular home directory of the user, not the one of within the |
|
103 |
Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its |
|
63669 | 104 |
HOME should point to the @{path "/home"} directory tree or the Windows user |
105 |
home.\<close> |
|
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
106 |
|
61575 | 107 |
\<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level |
108 |
Isabelle distribution directory. This is automatically determined from the |
|
109 |
Isabelle executable that has been invoked. Do not attempt to set @{setting |
|
110 |
ISABELLE_HOME} yourself from the shell! |
|
50182 | 111 |
|
61575 | 112 |
\<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of |
63669 | 113 |
@{setting ISABELLE_HOME}. The default value is relative to @{path |
61575 | 114 |
"$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the |
115 |
global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory |
|
116 |
mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide |
|
117 |
defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. |
|
118 |
||
119 |
\<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the |
|
120 |
general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that |
|
50182 | 121 |
platform-dependent tools usually need to refer to the more specific |
122 |
identification according to @{setting ISABELLE_PLATFORM}, @{setting |
|
123 |
ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}. |
|
124 |
||
61575 | 125 |
\<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic |
126 |
identifier for the underlying hardware and operating system. The Isabelle |
|
127 |
platform identification always refers to the 32 bit variant, even this is a |
|
128 |
64 bit machine. Note that the ML or Java runtime may have a different idea, |
|
129 |
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
|
130 |
|
61575 | 131 |
\<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting |
132 |
ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform |
|
133 |
that supports this; the value is empty for 32 bit. Note that the following |
|
134 |
bash expression (including the quotes) prefers the 64 bit platform, if that |
|
135 |
is available: |
|
47823 | 136 |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
137 |
@{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
|
138 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
139 |
\<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
140 |
of the @{executable isabelle} executable. Thus other tools and scripts need |
63669 | 141 |
not assume that the @{dir "$ISABELLE_HOME/bin"} directory is on the current |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
142 |
search path of the shell. |
28215 | 143 |
|
61575 | 144 |
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this |
145 |
Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''. |
|
146 |
||
147 |
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def |
|
148 |
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>] |
|
149 |
specify the underlying ML system to be used for Isabelle. There is only a |
|
150 |
fixed set of admissable @{setting ML_SYSTEM} names (see the @{file |
|
28238 | 151 |
"$ISABELLE_HOME/etc/settings"} file of the distribution). |
61575 | 152 |
|
28215 | 153 |
The actual compiler binary will be run from the directory @{setting |
61575 | 154 |
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line. |
155 |
The optional @{setting ML_PLATFORM} may specify the binary format of ML heap |
|
156 |
images, which is useful for cross-platform installations. The value of |
|
157 |
@{setting ML_IDENTIFIER} is automatically obtained by composing the values |
|
158 |
of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version |
|
159 |
values. |
|
47823 | 160 |
|
61575 | 161 |
\<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java |
162 |
Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is |
|
163 |
essential for Isabelle/Scala and other JVM-based tools to work properly. |
|
164 |
Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime |
|
47823 | 165 |
Environment), not JDK. |
61575 | 166 |
|
167 |
\<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by |
|
168 |
colons) where Isabelle logic images may reside. When looking up heaps files, |
|
169 |
the value of @{setting ML_IDENTIFIER} is appended to each component |
|
170 |
internally. |
|
171 |
||
172 |
\<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files |
|
173 |
should be stored by default. The ML system and Isabelle version identifier |
|
174 |
is appended here, too. |
|
175 |
||
176 |
\<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory |
|
62013 | 177 |
browser information is stored as HTML and PDF (see also \secref{sec:info}). |
63669 | 178 |
The default value is @{path "$ISABELLE_HOME_USER/browser_info"}. |
61575 | 179 |
|
180 |
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none |
|
181 |
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>. |
|
182 |
||
62562
905a5db3932d
back to external line editor, due to problems of JLine with multithreading of in vs. out;
wenzelm
parents:
62559
diff
changeset
|
183 |
\<^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
|
184 |
@{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
|
185 |
|
61575 | 186 |
\<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX}, |
187 |
@{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle |
|
188 |
document preparation (see also \secref{sec:tool-latex}). |
|
189 |
||
190 |
\<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories |
|
191 |
that are scanned by @{executable isabelle} for external utility programs |
|
192 |
(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
|
193 |
|
61575 | 194 |
\<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories |
195 |
with documentation files. |
|
196 |
||
197 |
\<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying |
|
198 |
\<^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
|
199 |
|
61575 | 200 |
\<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying |
201 |
\<^verbatim>\<open>dvi\<close> files. |
|
202 |
||
203 |
\<^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
|
204 |
running Isabelle ML process derives an individual directory for temporary |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
205 |
files. |
58618 | 206 |
\<close> |
28215 | 207 |
|
208 |
||
58618 | 209 |
subsection \<open>Additional components \label{sec:components}\<close> |
32323 | 210 |
|
61575 | 211 |
text \<open> |
212 |
Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The |
|
213 |
general layout conventions are that of the main Isabelle distribution |
|
214 |
itself, and the following two files (both optional) have a special meaning: |
|
32323 | 215 |
|
61575 | 216 |
\<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when |
217 |
bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As |
|
218 |
usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the |
|
219 |
component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable. |
|
32323 | 220 |
|
61575 | 221 |
For example, the following setting allows to refer to files within the |
222 |
component later on, without having to hardwire absolute paths: |
|
223 |
@{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>} |
|
32323 | 224 |
|
61575 | 225 |
Components can also add to existing Isabelle settings such as |
226 |
@{setting_def ISABELLE_TOOLS}, in order to provide component-specific |
|
227 |
tools that can be invoked by end-users. For example: |
|
228 |
@{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>} |
|
32323 | 229 |
|
61575 | 230 |
\<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same |
231 |
structure. The directory specifications given here can be either absolute |
|
232 |
(with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory. |
|
32323 | 233 |
|
61575 | 234 |
The root of component initialization is @{setting ISABELLE_HOME} itself. |
235 |
After initializing all of its sub-components recursively, @{setting |
|
236 |
ISABELLE_HOME_USER} is included in the same manner (if that directory |
|
63669 | 237 |
exists). This allows to install private components via @{path |
61575 | 238 |
"$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient |
239 |
to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the |
|
240 |
\<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component |
|
63669 | 241 |
directory). For example: @{verbatim [display] \<open>init_component |
242 |
"$HOME/screwdriver-2.0"\<close>} |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
243 |
|
61575 | 244 |
This is tolerant wrt.\ missing component directories, but might produce a |
245 |
warning. |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
246 |
|
61406 | 247 |
\<^medskip> |
61575 | 248 |
More complex situations may be addressed by initializing components listed |
249 |
in a given catalog file, relatively to some base directory: |
|
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
250 |
@{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
|
251 |
|
61575 | 252 |
The component directories listed in the catalog file are treated as relative |
253 |
to the given base directory. |
|
48844 | 254 |
|
61575 | 255 |
See also \secref{sec:tool-components} for some tool-support for resolving |
256 |
components that are formally initialized but not installed yet. |
|
58618 | 257 |
\<close> |
32323 | 258 |
|
259 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
260 |
section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close> |
28215 | 261 |
|
58618 | 262 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
263 |
The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
264 |
Isabelle related utilities, user interfaces etc. Such tools automatically |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
265 |
benefit from the settings mechanism. All Isabelle command-line tools are |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
266 |
invoked via a common wrapper --- @{executable_ref isabelle}: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
267 |
@{verbatim [display] |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
268 |
\<open>Usage: isabelle TOOL [ARGS ...] |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
269 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62677
diff
changeset
|
270 |
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
|
271 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
272 |
Available tools: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
273 |
...\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
274 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
275 |
In principle, Isabelle tools are ordinary executable scripts that are run |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
276 |
within the Isabelle settings environment, see \secref{sec:settings}. The set |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
277 |
of available tools is collected by @{executable isabelle} from the |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
278 |
directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
279 |
call the scripts directly from the shell. Neither should you add the tool |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
280 |
directories to your shell's search path! |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
281 |
\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
282 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
283 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
284 |
subsubsection \<open>Examples\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
285 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
286 |
text \<open> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
287 |
Show the list of available documentation of the Isabelle distribution: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
288 |
@{verbatim [display] \<open>isabelle doc\<close>} |
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 |
View a certain document as follows: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
291 |
@{verbatim [display] \<open>isabelle doc system\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
292 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
293 |
Query the Isabelle settings environment: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
294 |
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>} |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
295 |
\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
296 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
297 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
298 |
section \<open>The raw Isabelle ML process\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
299 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
300 |
subsection \<open>Batch mode \label{sec:tool-process}\<close> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
301 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
302 |
text \<open> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
303 |
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
|
304 |
@{verbatim [display] |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
305 |
\<open>Usage: isabelle process [OPTIONS] |
28215 | 306 |
|
307 |
Options are: |
|
62677 | 308 |
-T THEORY load theory |
62639 | 309 |
-d DIR include session directory |
62506 | 310 |
-e ML_EXPR evaluate ML expression on startup |
311 |
-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
|
312 |
-l NAME logic session name (default ISABELLE_LOGIC="HOL") |
28215 | 313 |
-m MODE add print mode for output |
52056 | 314 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
28215 | 315 |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
316 |
Run the raw Isabelle ML process in batch mode.\<close>} |
28215 | 317 |
|
62643 | 318 |
\<^medskip> |
62506 | 319 |
Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is |
320 |
started. The source is either given literally or taken from a file. Multiple |
|
321 |
\<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to |
|
322 |
premature exit of the ML process with return code 1. |
|
28215 | 323 |
|
61406 | 324 |
\<^medskip> |
62677 | 325 |
Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with |
326 |
a suitable @{ML use_thy} invocation. |
|
327 |
||
328 |
\<^medskip> |
|
62639 | 329 |
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies |
330 |
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
|
331 |
|
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
332 |
\<^medskip> |
61575 | 333 |
The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this |
62573 | 334 |
session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over |
335 |
mathematical Isabelle symbols. |
|
28215 | 336 |
|
61406 | 337 |
\<^medskip> |
61575 | 338 |
Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process, |
62573 | 339 |
see also \secref{sec:system-options}. |
58618 | 340 |
\<close> |
28215 | 341 |
|
342 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
343 |
subsubsection \<open>Example\<close> |
28215 | 344 |
|
58618 | 345 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
346 |
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
|
347 |
loader within ML: |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62588
diff
changeset
|
348 |
@{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
|
349 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
350 |
Observe the delicate quoting rules for the Bash shell vs.\ ML. The |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
351 |
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
|
352 |
to do it manually. |
58618 | 353 |
\<close> |
28238 | 354 |
|
355 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
356 |
subsection \<open>Interactive mode\<close> |
28238 | 357 |
|
58618 | 358 |
text \<open> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
359 |
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
|
360 |
console and line editor: |
61407
7ba7b8103565
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61406
diff
changeset
|
361 |
@{verbatim [display] |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
362 |
\<open>Usage: isabelle console [OPTIONS] |
28238 | 363 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
364 |
Options are: |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
365 |
-d DIR include session directory |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
366 |
-l NAME logic session name (default ISABELLE_LOGIC) |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
367 |
-m MODE add print mode for output |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
368 |
-n no build of session image on startup |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
369 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
62643 | 370 |
-r bootstrap from raw Poly/ML |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
371 |
-s system build mode for session image |
28238 | 372 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
373 |
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
|
374 |
in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>} |
28238 | 375 |
|
62643 | 376 |
\<^medskip> |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
377 |
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is |
62643 | 378 |
checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. |
28238 | 379 |
|
62643 | 380 |
Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is |
381 |
relevant for Isabelle/Pure development. |
|
382 |
||
383 |
\<^medskip> |
|
62639 | 384 |
Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process} |
385 |
(\secref{sec:tool-process}). |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
386 |
|
62639 | 387 |
Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build} |
388 |
(\secref{sec:tool-build}). |
|
28238 | 389 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
390 |
\<^medskip> |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
391 |
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
|
392 |
the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\ |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
393 |
@{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
|
394 |
standard input/output. |
28238 | 395 |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62576
diff
changeset
|
396 |
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
|
397 |
Isabelle/Isar nor Isabelle/ML within the usual formal context. The most |
62847 | 398 |
relevant ML commands at this stage are @{ML use} (for ML files) and |
399 |
@{ML use_thy} (for theory files). |
|
58618 | 400 |
\<close> |
28215 | 401 |
|
62451 | 402 |
|
403 |
section \<open>YXML versus XML\<close> |
|
404 |
||
405 |
text \<open> |
|
406 |
Isabelle tools often use YXML, which is a simple and efficient syntax for |
|
407 |
untyped XML trees. The YXML format is defined as follows. |
|
408 |
||
409 |
\<^enum> The encoding is always UTF-8. |
|
410 |
||
411 |
\<^enum> Body text is represented verbatim (no escaping, no special treatment of |
|
412 |
white space, no named entities, no CDATA chunks, no comments). |
|
413 |
||
414 |
\<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close> |
|
415 |
and \<open>\<^bold>Y = 6\<close> as follows: |
|
416 |
||
417 |
\begin{tabular}{ll} |
|
418 |
XML & YXML \\\hline |
|
419 |
\<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> & |
|
420 |
\<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\ |
|
421 |
\<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\ |
|
422 |
\end{tabular} |
|
423 |
||
424 |
There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated |
|
425 |
like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in |
|
426 |
well-formed XML documents. |
|
427 |
||
428 |
Parsing YXML is pretty straight-forward: split the text into chunks |
|
429 |
separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>. |
|
430 |
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk |
|
431 |
indicates close of an element. Any other non-empty chunk consists of plain |
|
432 |
text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file |
|
433 |
"~~/src/Pure/PIDE/yxml.scala"}. |
|
434 |
||
435 |
YXML documents may be detected quickly by checking that the first two |
|
436 |
characters are \<open>\<^bold>X\<^bold>Y\<close>. |
|
437 |
\<close> |
|
438 |
||
28223 | 439 |
end |