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