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