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