author | wenzelm |
Mon, 27 Aug 2012 21:37:34 +0200 | |
changeset 48945 | b5758f5a469c |
parent 48937 | e7418f8d49fe |
permissions | -rw-r--r-- |
28215 | 1 |
theory Basics |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
41955
diff
changeset
|
2 |
imports Base |
28215 | 3 |
begin |
4 |
||
5 |
chapter {* The Isabelle system environment *} |
|
6 |
||
47823 | 7 |
text {* This manual describes Isabelle together with related tools and |
8 |
user interfaces as seen from a system oriented view. See also the |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
9 |
\emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for |
47823 | 10 |
the actual Isabelle input language and related concepts, and |
11 |
\emph{The Isabelle/Isar Implementation |
|
12 |
Manual}~\cite{isabelle-implementation} for the main concepts of the |
|
13 |
underlying implementation in Isabelle/ML. |
|
28215 | 14 |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
15 |
\medskip The Isabelle system environment provides the following |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
16 |
basic infrastructure to integrate tools smoothly. |
28215 | 17 |
|
28238 | 18 |
\begin{enumerate} |
28215 | 19 |
|
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
20 |
\item The \emph{Isabelle settings} mechanism provides process |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
21 |
environment variables to all Isabelle executables (including tools |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
22 |
and user interfaces). |
28215 | 23 |
|
47823 | 24 |
\item The raw \emph{Isabelle process} (@{executable_ref |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
25 |
"isabelle-process"}) runs logic sessions either interactively or in |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
26 |
batch mode. In particular, this view abstracts over the invocation |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
27 |
of the actual ML system to be used. Regular users rarely need to |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
28 |
care about the low-level process. |
28215 | 29 |
|
48813 | 30 |
\item The main \emph{Isabelle tool wrapper} (@{executable_ref |
47823 | 31 |
isabelle}) provides a generic startup environment Isabelle related |
32 |
utilities, user interfaces etc. Such tools automatically benefit |
|
33 |
from the settings mechanism. |
|
28215 | 34 |
|
28238 | 35 |
\end{enumerate} |
28215 | 36 |
*} |
37 |
||
38 |
||
39 |
section {* Isabelle settings \label{sec:settings} *} |
|
40 |
||
41 |
text {* |
|
42 |
The Isabelle system heavily depends on the \emph{settings |
|
43 |
mechanism}\indexbold{settings}. Essentially, this is a statically |
|
44 |
scoped collection of environment variables, such as @{setting |
|
45 |
ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}. These |
|
46 |
variables are \emph{not} intended to be set directly from the shell, |
|
47 |
though. Isabelle employs a somewhat more sophisticated scheme of |
|
48 |
\emph{settings files} --- one for site-wide defaults, another for |
|
49 |
additional user-specific modifications. With all configuration |
|
47823 | 50 |
variables in clearly defined places, this scheme is more |
51 |
maintainable and user-friendly than global shell environment |
|
52 |
variables. |
|
28215 | 53 |
|
54 |
In particular, we avoid the typical situation where prospective |
|
55 |
users of a software package are told to put several things into |
|
56 |
their shell startup scripts, before being able to actually run the |
|
57 |
program. Isabelle requires none such administrative chores of its |
|
58 |
end-users --- the executables can be invoked straight away. |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40569
diff
changeset
|
59 |
Occasionally, users would still want to put the @{file |
28238 | 60 |
"$ISABELLE_HOME/bin"} directory into their shell's search path, but |
61 |
this is not required. |
|
28215 | 62 |
*} |
63 |
||
64 |
||
32323 | 65 |
subsection {* Bootstrapping the environment \label{sec:boot} *} |
28215 | 66 |
|
32323 | 67 |
text {* Isabelle executables need to be run within a proper settings |
68 |
environment. This is bootstrapped as described below, on the first |
|
69 |
invocation of one of the outer wrapper scripts (such as |
|
70 |
@{executable_ref isabelle}). This happens only once for each |
|
71 |
process tree, i.e.\ the environment is passed to subprocesses |
|
72 |
according to regular Unix conventions. |
|
28215 | 73 |
|
74 |
\begin{enumerate} |
|
75 |
||
76 |
\item The special variable @{setting_def ISABELLE_HOME} is |
|
77 |
determined automatically from the location of the binary that has |
|
78 |
been run. |
|
79 |
||
80 |
You should not try to set @{setting ISABELLE_HOME} manually. Also |
|
81 |
note that the Isabelle executables either have to be run from their |
|
82 |
original location in the distribution directory, or via the |
|
48602 | 83 |
executable objects created by the @{tool install} tool. Symbolic |
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40569
diff
changeset
|
84 |
links are admissible, but a plain copy of the @{file |
28238 | 85 |
"$ISABELLE_HOME/bin"} files will not work! |
86 |
||
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40569
diff
changeset
|
87 |
\item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a |
28238 | 88 |
@{executable_ref bash} shell script with the auto-export option for |
89 |
variables enabled. |
|
28215 | 90 |
|
91 |
This file holds a rather long list of shell variable assigments, |
|
92 |
thus providing the site-wide default settings. The Isabelle |
|
93 |
distribution already contains a global settings file with sensible |
|
94 |
defaults for most variables. When installing the system, only a few |
|
95 |
of these may have to be adapted (probably @{setting ML_SYSTEM} |
|
96 |
etc.). |
|
97 |
||
28285 | 98 |
\item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it |
28215 | 99 |
exists) is run in the same way as the site default settings. Note |
100 |
that the variable @{setting ISABELLE_HOME_USER} has already been set |
|
40387
e4c9e0dad473
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
wenzelm
parents:
38253
diff
changeset
|
101 |
before --- usually to something like @{verbatim |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
102 |
"$USER_HOME/.isabelle/IsabelleXXXX"}. |
28215 | 103 |
|
104 |
Thus individual users may override the site-wide defaults. See also |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40569
diff
changeset
|
105 |
file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the |
28238 | 106 |
distribution. Typically, a user settings file would contain only a |
107 |
few lines, just the assigments that are really changed. One should |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40569
diff
changeset
|
108 |
definitely \emph{not} start with a full copy the basic @{file |
28215 | 109 |
"$ISABELLE_HOME/etc/settings"}. This could cause very annoying |
110 |
maintainance problems later, when the Isabelle installation is |
|
111 |
updated or changed otherwise. |
|
112 |
||
113 |
\end{enumerate} |
|
114 |
||
28238 | 115 |
Since settings files are regular GNU @{executable_def bash} scripts, |
116 |
one may use complex shell commands, such as @{verbatim "if"} or |
|
28215 | 117 |
@{verbatim "case"} statements to set variables depending on the |
118 |
system architecture or other environment variables. Such advanced |
|
119 |
features should be added only with great care, though. In |
|
120 |
particular, external environment references should be kept at a |
|
121 |
minimum. |
|
122 |
||
123 |
\medskip A few variables are somewhat special: |
|
124 |
||
125 |
\begin{itemize} |
|
126 |
||
28502 | 127 |
\item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set |
28215 | 128 |
automatically to the absolute path names of the @{executable |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
129 |
"isabelle-process"} and @{executable isabelle} executables, |
28215 | 130 |
respectively. |
131 |
||
28238 | 132 |
\item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of |
28215 | 133 |
the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and |
134 |
the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically |
|
135 |
to its value. |
|
136 |
||
137 |
\end{itemize} |
|
138 |
||
28238 | 139 |
\medskip Note that the settings environment may be inspected with |
48602 | 140 |
the @{tool getenv} tool. This might help to figure out the effect |
141 |
of complex settings scripts. *} |
|
28215 | 142 |
|
143 |
||
48602 | 144 |
subsection {* Common variables *} |
28215 | 145 |
|
146 |
text {* |
|
147 |
This is a reference of common Isabelle settings variables. Note that |
|
148 |
the list is somewhat open-ended. Third-party utilities or interfaces |
|
149 |
may add their own selection. Variables that are special in some |
|
150 |
sense are marked with @{text "\<^sup>*"}. |
|
151 |
||
152 |
\begin{description} |
|
153 |
||
47823 | 154 |
\item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform |
155 |
user home directory. On Unix systems this is usually the same as |
|
156 |
@{setting HOME}, but on Windows it is the regular home directory of |
|
157 |
the user, not the one of within the Cygwin root |
|
158 |
file-system.\footnote{Cygwin itself offers another choice whether |
|
159 |
its HOME should point to the \texttt{/home} directory tree or the |
|
160 |
Windows user home.} |
|
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
161 |
|
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
162 |
\item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
163 |
top-level Isabelle distribution directory. This is automatically |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
164 |
determined from the Isabelle executable that has been invoked. Do |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
165 |
not attempt to set @{setting ISABELLE_HOME} yourself from the shell! |
28215 | 166 |
|
167 |
\item[@{setting_def ISABELLE_HOME_USER}] is the user-specific |
|
168 |
counterpart of @{setting ISABELLE_HOME}. The default value is |
|
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
169 |
relative to @{verbatim "$USER_HOME/.isabelle"}, under rare |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
170 |
circumstances this may be changed in the global setting file. |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
171 |
Typically, the @{setting ISABELLE_HOME_USER} directory mimics |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
172 |
@{setting ISABELLE_HOME} to some extend. In particular, site-wide |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
45028
diff
changeset
|
173 |
defaults may be overridden by a private @{verbatim |
40387
e4c9e0dad473
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
wenzelm
parents:
38253
diff
changeset
|
174 |
"$ISABELLE_HOME_USER/etc/settings"}. |
28215 | 175 |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
176 |
\item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
177 |
set to a symbolic identifier for the underlying hardware and |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
178 |
operating system. The Isabelle platform identification always |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
179 |
refers to the 32 bit variant, even this is a 64 bit machine. Note |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
180 |
that the ML or Java runtime may have a different idea, depending on |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
181 |
which binaries are actually run. |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
182 |
|
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
183 |
\item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
184 |
@{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant |
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
185 |
on a platform that supports this; the value is empty for 32 bit. |
47823 | 186 |
Note that the following bash expression (including the quotes) |
187 |
prefers the 64 bit platform, if that is available: |
|
188 |
||
189 |
@{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""} |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
33952
diff
changeset
|
190 |
|
28502 | 191 |
\item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting |
28500 | 192 |
ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path |
28215 | 193 |
names of the @{executable "isabelle-process"} and @{executable |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
194 |
isabelle} executables, respectively. Thus other tools and scripts |
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40569
diff
changeset
|
195 |
need not assume that the @{file "$ISABELLE_HOME/bin"} directory is |
28238 | 196 |
on the current search path of the shell. |
28215 | 197 |
|
198 |
\item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers |
|
199 |
to the name of this Isabelle distribution, e.g.\ ``@{verbatim |
|
47823 | 200 |
Isabelle2012}''. |
28215 | 201 |
|
202 |
\item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, |
|
203 |
@{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def |
|
204 |
ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system |
|
205 |
to be used for Isabelle. There is only a fixed set of admissable |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40569
diff
changeset
|
206 |
@{setting ML_SYSTEM} names (see the @{file |
28238 | 207 |
"$ISABELLE_HOME/etc/settings"} file of the distribution). |
28215 | 208 |
|
209 |
The actual compiler binary will be run from the directory @{setting |
|
210 |
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the |
|
211 |
command line. The optional @{setting ML_PLATFORM} may specify the |
|
212 |
binary format of ML heap images, which is useful for cross-platform |
|
213 |
installations. The value of @{setting ML_IDENTIFIER} is |
|
214 |
automatically obtained by composing the values of @{setting |
|
215 |
ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values. |
|
47823 | 216 |
|
217 |
\item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK |
|
218 |
(Java Development Kit) installation with @{verbatim javac} and |
|
219 |
@{verbatim jar} executables. This is essential for Isabelle/Scala |
|
220 |
and other JVM-based tools to work properly. Note that conventional |
|
221 |
@{verbatim JAVA_HOME} usually points to the JRE (Java Runtime |
|
222 |
Environment), not JDK. |
|
28215 | 223 |
|
224 |
\item[@{setting_def ISABELLE_PATH}] is a list of directories |
|
225 |
(separated by colons) where Isabelle logic images may reside. When |
|
226 |
looking up heaps files, the value of @{setting ML_IDENTIFIER} is |
|
227 |
appended to each component internally. |
|
228 |
||
229 |
\item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a |
|
230 |
directory where output heap files should be stored by default. The |
|
231 |
ML system and Isabelle version identifier is appended here, too. |
|
232 |
||
233 |
\item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where |
|
234 |
theory browser information (HTML text, graph data, and printable |
|
235 |
documents) is stored (see also \secref{sec:info}). The default |
|
236 |
value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}. |
|
237 |
||
238 |
\item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to |
|
239 |
load if none is given explicitely by the user. The default value is |
|
240 |
@{verbatim HOL}. |
|
241 |
||
242 |
\item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default |
|
28238 | 243 |
line editor for the @{tool_ref tty} interface. |
28215 | 244 |
|
245 |
\item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed |
|
28238 | 246 |
to the command line of any @{tool_ref usedir} invocation. This |
247 |
typically contains compilation options for object-logics --- @{tool |
|
48602 | 248 |
usedir} is the basic tool for managing logic sessions (cf.\ the |
28238 | 249 |
@{verbatim IsaMakefile}s in the distribution). |
28215 | 250 |
|
251 |
\item[@{setting_def ISABELLE_LATEX}, @{setting_def |
|
252 |
ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def |
|
253 |
ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle |
|
254 |
document preparation (see also \secref{sec:tool-latex}). |
|
255 |
||
256 |
\item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
257 |
directories that are scanned by @{executable isabelle} for external |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
258 |
utility programs (see also \secref{sec:isabelle-tool}). |
28215 | 259 |
|
260 |
\item[@{setting_def ISABELLE_DOCS}] is a colon separated list of |
|
261 |
directories with documentation files. |
|
262 |
||
263 |
\item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred |
|
264 |
document format, typically @{verbatim dvi} or @{verbatim pdf}. |
|
265 |
||
266 |
\item[@{setting_def DVI_VIEWER}] specifies the command to be used |
|
267 |
for displaying @{verbatim dvi} files. |
|
268 |
||
269 |
\item[@{setting_def PDF_VIEWER}] specifies the command to be used |
|
270 |
for displaying @{verbatim pdf} files. |
|
271 |
||
272 |
\item[@{setting_def PRINT_COMMAND}] specifies the standard printer |
|
273 |
spool command, which is expected to accept @{verbatim ps} files. |
|
274 |
||
275 |
\item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the |
|
28238 | 276 |
prefix from which any running @{executable "isabelle-process"} |
277 |
derives an individual directory for temporary files. The default is |
|
28215 | 278 |
somewhere in @{verbatim "/tmp"}. |
279 |
||
280 |
\end{description} |
|
281 |
*} |
|
282 |
||
283 |
||
32323 | 284 |
subsection {* Additional components \label{sec:components} *} |
285 |
||
286 |
text {* Any directory may be registered as an explicit \emph{Isabelle |
|
287 |
component}. The general layout conventions are that of the main |
|
288 |
Isabelle distribution itself, and the following two files (both |
|
289 |
optional) have a special meaning: |
|
290 |
||
291 |
\begin{itemize} |
|
292 |
||
293 |
\item @{verbatim "etc/settings"} holds additional settings that are |
|
294 |
initialized when bootstrapping the overall Isabelle environment, |
|
295 |
cf.\ \secref{sec:boot}. As usual, the content is interpreted as a |
|
296 |
@{verbatim bash} script. It may refer to the component's enclosing |
|
297 |
directory via the @{verbatim "COMPONENT"} shell variable. |
|
298 |
||
299 |
For example, the following setting allows to refer to files within |
|
300 |
the component later on, without having to hardwire absolute paths: |
|
301 |
||
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
302 |
\begin{ttbox} |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
303 |
MY_COMPONENT_HOME="$COMPONENT" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
304 |
\end{ttbox} |
32323 | 305 |
|
306 |
Components can also add to existing Isabelle settings such as |
|
307 |
@{setting_def ISABELLE_TOOLS}, in order to provide |
|
308 |
component-specific tools that can be invoked by end-users. For |
|
309 |
example: |
|
310 |
||
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
311 |
\begin{ttbox} |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
312 |
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
313 |
\end{ttbox} |
32323 | 314 |
|
315 |
\item @{verbatim "etc/components"} holds a list of further |
|
316 |
sub-components of the same structure. The directory specifications |
|
317 |
given here can be either absolute (with leading @{verbatim "/"}) or |
|
318 |
relative to the component's main directory. |
|
319 |
||
320 |
\end{itemize} |
|
321 |
||
322 |
The root of component initialization is @{setting ISABELLE_HOME} |
|
323 |
itself. After initializing all of its sub-components recursively, |
|
324 |
@{setting ISABELLE_HOME_USER} is included in the same manner (if |
|
40569
ffcff7509a49
more explicit explanation of init_component shell function;
wenzelm
parents:
40387
diff
changeset
|
325 |
that directory exists). This allows to install private components |
ffcff7509a49
more explicit explanation of init_component shell function;
wenzelm
parents:
40387
diff
changeset
|
326 |
via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is |
ffcff7509a49
more explicit explanation of init_component shell function;
wenzelm
parents:
40387
diff
changeset
|
327 |
often more convenient to do that programmatically via the |
ffcff7509a49
more explicit explanation of init_component shell function;
wenzelm
parents:
40387
diff
changeset
|
328 |
\verb,init_component, shell function in the \verb,etc/settings, |
ffcff7509a49
more explicit explanation of init_component shell function;
wenzelm
parents:
40387
diff
changeset
|
329 |
script of \verb,$ISABELLE_HOME_USER, (or any other component |
ffcff7509a49
more explicit explanation of init_component shell function;
wenzelm
parents:
40387
diff
changeset
|
330 |
directory). For example: |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
331 |
\begin{ttbox} |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
332 |
init_component "$HOME/screwdriver-2.0" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
333 |
\end{ttbox} |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
334 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
335 |
This is tolerant wrt.\ missing component directories, but might |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
336 |
produce a warning. |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
337 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
338 |
\medskip More complex situations may be addressed by initializing |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
339 |
components listed in a given catalog file, relatively to some base |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
340 |
directory: |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
341 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
342 |
\begin{ttbox} |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
343 |
init_components "$HOME/my_component_store" "some_catalog_file" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
344 |
\end{ttbox} |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
345 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
346 |
The component directories listed in the catalog file are treated as |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48813
diff
changeset
|
347 |
relative to the given base directory. |
48844 | 348 |
|
349 |
See also \secref{sec:tool-components} for some tool-support for |
|
350 |
resolving components that are formally initialized but not installed |
|
351 |
yet. |
|
32323 | 352 |
*} |
353 |
||
354 |
||
28215 | 355 |
section {* The raw Isabelle process *} |
356 |
||
357 |
text {* |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
358 |
The @{executable_def "isabelle-process"} executable runs bare-bones |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
359 |
Isabelle logic sessions --- either interactively or in batch mode. |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
360 |
It provides an abstraction over the underlying ML system, and over |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
361 |
the actual heap file locations. Its usage is: |
28215 | 362 |
|
363 |
\begin{ttbox} |
|
28238 | 364 |
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT] |
28215 | 365 |
|
366 |
Options are: |
|
367 |
-I startup Isar interaction mode |
|
368 |
-P startup Proof General interaction mode |
|
369 |
-S secure mode -- disallow critical operations |
|
45028 | 370 |
-T ADDR startup process wrapper, with socket address |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
36196
diff
changeset
|
371 |
-W IN:OUT startup process wrapper, with input/output fifos |
28215 | 372 |
-X startup PGIP interaction mode |
373 |
-e MLTEXT pass MLTEXT to the ML session |
|
374 |
-f pass 'Session.finish();' to the ML session |
|
375 |
-m MODE add print mode for output |
|
376 |
-q non-interactive session |
|
377 |
-r open heap file read-only |
|
378 |
-u pass 'use"ROOT.ML";' to the ML session |
|
379 |
-w reset write permissions on OUTPUT |
|
380 |
||
381 |
INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps. |
|
382 |
These are either names to be searched in the Isabelle path, or |
|
383 |
actual file names (containing at least one /). |
|
384 |
If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system. |
|
385 |
\end{ttbox} |
|
386 |
||
387 |
Input files without path specifications are looked up in the |
|
388 |
@{setting ISABELLE_PATH} setting, which may consist of multiple |
|
389 |
components separated by colons --- these are tried in the given |
|
390 |
order with the value of @{setting ML_IDENTIFIER} appended |
|
391 |
internally. In a similar way, base names are relative to the |
|
392 |
directory specified by @{setting ISABELLE_OUTPUT}. In any case, |
|
393 |
actual file locations may also be given by including at least one |
|
394 |
slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to |
|
395 |
refer to the current directory). |
|
396 |
*} |
|
397 |
||
398 |
||
28223 | 399 |
subsubsection {* Options *} |
28215 | 400 |
|
401 |
text {* |
|
402 |
If the input heap file does not have write permission bits set, or |
|
403 |
the @{verbatim "-r"} option is given explicitely, then the session |
|
404 |
started will be read-only. That is, the ML world cannot be |
|
405 |
committed back into the image file. Otherwise, a writable session |
|
406 |
enables commits into either the input file, or into another output |
|
407 |
heap file (if that is given as the second argument on the command |
|
408 |
line). |
|
409 |
||
410 |
The read-write state of sessions is determined at startup only, it |
|
411 |
cannot be changed intermediately. Also note that heap images may |
|
412 |
require considerable amounts of disk space (approximately |
|
413 |
50--200~MB). Users are responsible for themselves to dispose their |
|
414 |
heap files when they are no longer needed. |
|
415 |
||
416 |
\medskip The @{verbatim "-w"} option makes the output heap file |
|
417 |
read-only after terminating. Thus subsequent invocations cause the |
|
418 |
logic image to be read-only automatically. |
|
419 |
||
420 |
\medskip Using the @{verbatim "-e"} option, arbitrary ML code may be |
|
421 |
passed to the Isabelle session from the command line. Multiple |
|
422 |
@{verbatim "-e"}'s are evaluated in the given order. Strange things |
|
423 |
may happen when errorneous ML code is provided. Also make sure that |
|
424 |
the ML commands are terminated properly by semicolon. |
|
425 |
||
426 |
\medskip The @{verbatim "-u"} option is a shortcut for @{verbatim |
|
427 |
"-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session. |
|
28223 | 428 |
The @{verbatim "-f"} option passes ``@{verbatim |
429 |
"Session.finish();"}'', which is intended mainly for administrative |
|
430 |
purposes. |
|
28215 | 431 |
|
432 |
\medskip The @{verbatim "-m"} option adds identifiers of print modes |
|
433 |
to be made active for this session. Typically, this is used by some |
|
434 |
user interface, e.g.\ to enable output of proper mathematical |
|
435 |
symbols. |
|
436 |
||
437 |
\medskip Isabelle normally enters an interactive top-level loop |
|
438 |
(after processing the @{verbatim "-e"} texts). The @{verbatim "-q"} |
|
439 |
option inhibits interaction, thus providing a pure batch mode |
|
440 |
facility. |
|
441 |
||
442 |
\medskip The @{verbatim "-I"} option makes Isabelle enter Isar |
|
443 |
interaction mode on startup, instead of the primitive ML top-level. |
|
444 |
The @{verbatim "-P"} option configures the top-level loop for |
|
445 |
interaction with the Proof General user interface, and the |
|
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
36196
diff
changeset
|
446 |
@{verbatim "-X"} option enables XML-based PGIP communication. |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
36196
diff
changeset
|
447 |
|
45028 | 448 |
\medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes |
449 |
Isabelle enter a special process wrapper for interaction via the |
|
450 |
Isabelle/Scala layer, see also @{file |
|
451 |
"~~/src/Pure/System/isabelle_process.scala"}. The protocol between |
|
452 |
the ML and JVM process is private to the implementation. |
|
28215 | 453 |
|
454 |
\medskip The @{verbatim "-S"} option makes the Isabelle process more |
|
455 |
secure by disabling some critical operations, notably runtime |
|
456 |
compilation and evaluation of ML source code. |
|
457 |
*} |
|
458 |
||
459 |
||
28223 | 460 |
subsubsection {* Examples *} |
28215 | 461 |
|
462 |
text {* |
|
463 |
Run an interactive session of the default object-logic (as specified |
|
464 |
by the @{setting ISABELLE_LOGIC} setting) like this: |
|
465 |
\begin{ttbox} |
|
28238 | 466 |
isabelle-process |
28215 | 467 |
\end{ttbox} |
468 |
||
469 |
Usually @{setting ISABELLE_LOGIC} refers to one of the standard |
|
470 |
logic images, which are read-only by default. A writable session |
|
47823 | 471 |
--- based on @{verbatim HOL}, but output to @{verbatim Test} (in the |
28238 | 472 |
directory specified by the @{setting ISABELLE_OUTPUT} setting) --- |
28215 | 473 |
may be invoked as follows: |
474 |
\begin{ttbox} |
|
47823 | 475 |
isabelle-process HOL Test |
28215 | 476 |
\end{ttbox} |
477 |
Ending this session normally (e.g.\ by typing control-D) dumps the |
|
47823 | 478 |
whole ML system state into @{verbatim Test} (be prepared for more |
479 |
than 100\,MB): |
|
28215 | 480 |
|
47823 | 481 |
The @{verbatim Test} session may be continued later (still in |
28215 | 482 |
writable state) by: |
483 |
\begin{ttbox} |
|
47823 | 484 |
isabelle-process Test |
28215 | 485 |
\end{ttbox} |
47823 | 486 |
A read-only @{verbatim Test} session may be started by: |
28215 | 487 |
\begin{ttbox} |
47823 | 488 |
isabelle-process -r Test |
28215 | 489 |
\end{ttbox} |
490 |
||
491 |
\medskip Note that manual session management like this does |
|
492 |
\emph{not} provide proper setup for theory presentation. This would |
|
48602 | 493 |
require @{tool usedir}. |
28215 | 494 |
|
28238 | 495 |
\bigskip The next example demonstrates batch execution of Isabelle. |
47823 | 496 |
We retrieve the @{verbatim Main} theory value from the theory loader |
497 |
within ML (observe the delicate quoting rules for the Bash shell |
|
498 |
vs.\ ML): |
|
28215 | 499 |
\begin{ttbox} |
47823 | 500 |
isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL |
28215 | 501 |
\end{ttbox} |
502 |
Note that the output text will be interspersed with additional junk |
|
28238 | 503 |
messages by the ML runtime environment. The @{verbatim "-W"} option |
504 |
allows to communicate with the Isabelle process via an external |
|
505 |
program in a more robust fashion. |
|
506 |
*} |
|
507 |
||
508 |
||
48813 | 509 |
section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *} |
28238 | 510 |
|
511 |
text {* |
|
512 |
All Isabelle related tools and interfaces are called via a common |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
513 |
wrapper --- @{executable isabelle}: |
28238 | 514 |
|
515 |
\begin{ttbox} |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
516 |
Usage: isabelle TOOL [ARGS ...] |
28238 | 517 |
|
28506 | 518 |
Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. |
28238 | 519 |
|
48858 | 520 |
Available tools: |
521 |
\dots |
|
28238 | 522 |
\end{ttbox} |
523 |
||
524 |
In principle, Isabelle tools are ordinary executable scripts that |
|
525 |
are run within the Isabelle settings environment, see |
|
526 |
\secref{sec:settings}. The set of available tools is collected by |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
527 |
@{executable isabelle} from the directories listed in the @{setting |
28238 | 528 |
ISABELLE_TOOLS} setting. Do not try to call the scripts directly |
529 |
from the shell. Neither should you add the tool directories to your |
|
530 |
shell's search path! |
|
531 |
*} |
|
532 |
||
533 |
||
534 |
subsubsection {* Examples *} |
|
535 |
||
48813 | 536 |
text {* Show the list of available documentation of the Isabelle |
537 |
distribution: |
|
28238 | 538 |
|
539 |
\begin{ttbox} |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28502
diff
changeset
|
540 |
isabelle doc |
28238 | 541 |
\end{ttbox} |
542 |
||
543 |
View a certain document as follows: |
|
544 |
\begin{ttbox} |
|
47823 | 545 |
isabelle doc system |
28238 | 546 |
\end{ttbox} |
547 |
||
48813 | 548 |
Query the Isabelle settings environment: |
28238 | 549 |
\begin{ttbox} |
48813 | 550 |
isabelle getenv ISABELLE_HOME_USER |
28238 | 551 |
\end{ttbox} |
28215 | 552 |
*} |
553 |
||
28223 | 554 |
end |