author | wenzelm |
Tue, 04 Aug 2009 15:59:57 +0200 | |
changeset 32323 | 8185d3bfcbf1 |
parent 32088 | 2110fcd86efb |
child 32324 | a99e58e043ee |
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 |
|
28505 | 40 |
\item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) runs logic sessions either interactively or in |
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 |
|
61 |
scoped collection of environment variables, such as \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}, \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}, \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}. These |
|
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. |
|
28238 | 74 |
Occasionally, users would still want to put the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory into their shell's search path, but |
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 |
||
93 |
\item The special variable \indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}} is |
|
94 |
determined automatically from the location of the binary that has |
|
95 |
been run. |
|
96 |
||
97 |
You should not try to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} manually. Also |
|
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 |
101 |
links are admissible, but a plain copy of the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} files will not work! |
|
102 |
||
103 |
\item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} ist run as a |
|
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 |
|
111 |
of these may have to be adapted (probably \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}} |
|
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 |
116 |
that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set |
|
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28507
diff
changeset
|
117 |
before --- usually to \verb|~/.isabelle|. |
28222 | 118 |
|
119 |
Thus individual users may override the site-wide defaults. See also |
|
28238 | 120 |
file \hyperlink{file.$ISABELLE-HOME/etc/user-settings.sample}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}user{\isacharminus}settings{\isachardot}sample}}}} in the |
121 |
distribution. Typically, a user settings file would contain only a |
|
122 |
few lines, just the assigments that are really changed. One should |
|
123 |
definitely \emph{not} start with a full copy the basic \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\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 |
||
28503 | 141 |
\item \indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}} and \indexdef{}{setting}{ISABELLE\_TOOL}\hypertarget{setting.ISABELLE-TOOL}{\hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}} are set |
28505 | 142 |
automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, |
28222 | 143 |
respectively. |
144 |
||
28238 | 145 |
\item \indexref{}{setting}{ISABELLE\_OUTPUT}\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} will have the identifiers of |
28222 | 146 |
the Isabelle distribution (cf.\ \hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}) and |
147 |
the ML system (cf.\ \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}) appended automatically |
|
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 |
|
166 |
sense are marked with \isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}. |
|
167 |
||
168 |
\begin{description} |
|
169 |
||
170 |
\item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is the |
|
171 |
location of the top-level Isabelle distribution directory. This is |
|
172 |
automatically determined from the Isabelle executable that has been |
|
173 |
invoked. Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} yourself |
|
28238 | 174 |
from the shell! |
28222 | 175 |
|
176 |
\item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}}}] is the user-specific |
|
177 |
counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is |
|
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28507
diff
changeset
|
178 |
\verb|~/.isabelle|, under rare circumstances this may be |
28222 | 179 |
changed in the global setting file. Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to |
180 |
some extend. In particular, site-wide defaults may be overridden by |
|
28286 | 181 |
a private \verb|$ISABELLE_HOME_USER/etc/settings|. |
28222 | 182 |
|
28503 | 183 |
\item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path |
28505 | 184 |
names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively. Thus other tools and scripts |
28238 | 185 |
need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is |
186 |
on the current search path of the shell. |
|
28222 | 187 |
|
188 |
\item[\indexdef{}{setting}{ISABELLE\_IDENTIFIER}\hypertarget{setting.ISABELLE-IDENTIFIER}{\hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}IDENTIFIER}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] refers |
|
189 |
to the name of this Isabelle distribution, e.g.\ ``\verb|Isabelle2008|''. |
|
190 |
||
191 |
\item[\indexdef{}{setting}{ML\_SYSTEM}\hypertarget{setting.ML-SYSTEM}{\hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}}, \indexdef{}{setting}{ML\_HOME}\hypertarget{setting.ML-HOME}{\hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}}, |
|
192 |
\indexdef{}{setting}{ML\_OPTIONS}\hypertarget{setting.ML-OPTIONS}{\hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isacharunderscore}OPTIONS}}}}}, \indexdef{}{setting}{ML\_PLATFORM}\hypertarget{setting.ML-PLATFORM}{\hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}}}, \indexdef{}{setting}{ML\_IDENTIFIER}\hypertarget{setting.ML-IDENTIFIER}{\hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] specify the underlying ML system |
|
193 |
to be used for Isabelle. There is only a fixed set of admissable |
|
28238 | 194 |
\hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}} names (see the \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}settings}}}} file of the distribution). |
28222 | 195 |
|
196 |
The actual compiler binary will be run from the directory \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isacharunderscore}HOME}}}}, with \hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isacharunderscore}OPTIONS}}}} as first arguments on the |
|
197 |
command line. The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} may specify the |
|
198 |
binary format of ML heap images, which is useful for cross-platform |
|
199 |
installations. The value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is |
|
200 |
automatically obtained by composing the values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}, \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}} and the Isabelle version values. |
|
201 |
||
202 |
\item[\indexdef{}{setting}{ISABELLE\_PATH}\hypertarget{setting.ISABELLE-PATH}{\hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}}}] is a list of directories |
|
203 |
(separated by colons) where Isabelle logic images may reside. When |
|
204 |
looking up heaps files, the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} is |
|
205 |
appended to each component internally. |
|
206 |
||
207 |
\item[\indexdef{}{setting}{ISABELLE\_OUTPUT}\hypertarget{setting.ISABELLE-OUTPUT}{\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is a |
|
208 |
directory where output heap files should be stored by default. The |
|
209 |
ML system and Isabelle version identifier is appended here, too. |
|
210 |
||
211 |
\item[\indexdef{}{setting}{ISABELLE\_BROWSER\_INFO}\hypertarget{setting.ISABELLE-BROWSER-INFO}{\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}}] is the directory where |
|
212 |
theory browser information (HTML text, graph data, and printable |
|
213 |
documents) is stored (see also \secref{sec:info}). The default |
|
214 |
value is \verb|$ISABELLE_HOME_USER/browser_info|. |
|
215 |
||
216 |
\item[\indexdef{}{setting}{ISABELLE\_LOGIC}\hypertarget{setting.ISABELLE-LOGIC}{\hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}}}] specifies the default logic to |
|
217 |
load if none is given explicitely by the user. The default value is |
|
218 |
\verb|HOL|. |
|
219 |
||
220 |
\item[\indexdef{}{setting}{ISABELLE\_LINE\_EDITOR}\hypertarget{setting.ISABELLE-LINE-EDITOR}{\hyperlink{setting.ISABELLE-LINE-EDITOR}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LINE{\isacharunderscore}EDITOR}}}}}] specifies the default |
|
28238 | 221 |
line editor for the \indexref{}{tool}{tty}\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}} interface. |
28222 | 222 |
|
223 |
\item[\indexdef{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hypertarget{setting.ISABELLE-USEDIR-OPTIONS}{\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}}] is implicitly prefixed |
|
28238 | 224 |
to the command line of any \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} invocation. This |
225 |
typically contains compilation options for object-logics --- \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} is the basic utility for managing logic sessions (cf.\ the |
|
226 |
\verb|IsaMakefile|s in the distribution). |
|
28222 | 227 |
|
228 |
\item[\indexdef{}{setting}{ISABELLE\_FILE\_IDENT}\hypertarget{setting.ISABELLE-FILE-IDENT}{\hyperlink{setting.ISABELLE-FILE-IDENT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}FILE{\isacharunderscore}IDENT}}}}}] specifies a shell command |
|
229 |
for producing a source file identification, based on the actual |
|
230 |
content instead of the full physical path and date stamp (which is |
|
231 |
the default). A typical identification would produce a ``digest'' of |
|
232 |
the text, using a cryptographic hash function like SHA-1, for |
|
233 |
example. |
|
234 |
||
235 |
\item[\indexdef{}{setting}{ISABELLE\_LATEX}\hypertarget{setting.ISABELLE-LATEX}{\hyperlink{setting.ISABELLE-LATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LATEX}}}}}, \indexdef{}{setting}{ISABELLE\_PDFLATEX}\hypertarget{setting.ISABELLE-PDFLATEX}{\hyperlink{setting.ISABELLE-PDFLATEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PDFLATEX}}}}}, \indexdef{}{setting}{ISABELLE\_BIBTEX}\hypertarget{setting.ISABELLE-BIBTEX}{\hyperlink{setting.ISABELLE-BIBTEX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BIBTEX}}}}}, \indexdef{}{setting}{ISABELLE\_DVIPS}\hypertarget{setting.ISABELLE-DVIPS}{\hyperlink{setting.ISABELLE-DVIPS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DVIPS}}}}}] refer to {\LaTeX} related tools for Isabelle |
|
236 |
document preparation (see also \secref{sec:tool-latex}). |
|
237 |
||
238 |
\item[\indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}}}] is a colon separated list of |
|
28505 | 239 |
directories that are scanned by \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} for external |
240 |
utility programs (see also \secref{sec:isabelle-tool}). |
|
28222 | 241 |
|
242 |
\item[\indexdef{}{setting}{ISABELLE\_DOCS}\hypertarget{setting.ISABELLE-DOCS}{\hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOCS}}}}}] is a colon separated list of |
|
243 |
directories with documentation files. |
|
244 |
||
245 |
\item[\indexdef{}{setting}{ISABELLE\_DOC\_FORMAT}\hypertarget{setting.ISABELLE-DOC-FORMAT}{\hyperlink{setting.ISABELLE-DOC-FORMAT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOC{\isacharunderscore}FORMAT}}}}}] specifies the preferred |
|
246 |
document format, typically \verb|dvi| or \verb|pdf|. |
|
247 |
||
248 |
\item[\indexdef{}{setting}{DVI\_VIEWER}\hypertarget{setting.DVI-VIEWER}{\hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isacharunderscore}VIEWER}}}}}] specifies the command to be used |
|
249 |
for displaying \verb|dvi| files. |
|
250 |
||
251 |
\item[\indexdef{}{setting}{PDF\_VIEWER}\hypertarget{setting.PDF-VIEWER}{\hyperlink{setting.PDF-VIEWER}{\mbox{\isa{\isatt{PDF{\isacharunderscore}VIEWER}}}}}] specifies the command to be used |
|
252 |
for displaying \verb|pdf| files. |
|
253 |
||
254 |
\item[\indexdef{}{setting}{PRINT\_COMMAND}\hypertarget{setting.PRINT-COMMAND}{\hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isacharunderscore}COMMAND}}}}}] specifies the standard printer |
|
255 |
spool command, which is expected to accept \verb|ps| files. |
|
256 |
||
257 |
\item[\indexdef{}{setting}{ISABELLE\_TMP\_PREFIX}\hypertarget{setting.ISABELLE-TMP-PREFIX}{\hyperlink{setting.ISABELLE-TMP-PREFIX}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TMP{\isacharunderscore}PREFIX}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is the |
|
28238 | 258 |
prefix from which any running \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} |
259 |
derives an individual directory for temporary files. The default is |
|
28222 | 260 |
somewhere in \verb|/tmp|. |
261 |
||
262 |
\end{description}% |
|
263 |
\end{isamarkuptext}% |
|
264 |
\isamarkuptrue% |
|
265 |
% |
|
32323 | 266 |
\isamarkupsubsection{Additional components \label{sec:components}% |
267 |
} |
|
268 |
\isamarkuptrue% |
|
269 |
% |
|
270 |
\begin{isamarkuptext}% |
|
271 |
Any directory may be registered as an explicit \emph{Isabelle |
|
272 |
component}. The general layout conventions are that of the main |
|
273 |
Isabelle distribution itself, and the following two files (both |
|
274 |
optional) have a special meaning: |
|
275 |
||
276 |
\begin{itemize} |
|
277 |
||
278 |
\item \verb|etc/settings| holds additional settings that are |
|
279 |
initialized when bootstrapping the overall Isabelle environment, |
|
280 |
cf.\ \secref{sec:boot}. As usual, the content is interpreted as a |
|
281 |
\verb|bash| script. It may refer to the component's enclosing |
|
282 |
directory via the \verb|COMPONENT| shell variable. |
|
283 |
||
284 |
For example, the following setting allows to refer to files within |
|
285 |
the component later on, without having to hardwire absolute paths: |
|
286 |
||
287 |
\begin{ttbox} |
|
288 |
MY_COMPONENT_HOME="$COMPONENT" |
|
289 |
\end{ttbox} |
|
290 |
||
291 |
Components can also add to existing Isabelle settings such as |
|
292 |
\indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}}}, in order to provide |
|
293 |
component-specific tools that can be invoked by end-users. For |
|
294 |
example: |
|
295 |
||
296 |
\begin{ttbox} |
|
297 |
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" |
|
298 |
\end{ttbox} |
|
299 |
||
300 |
\item \verb|etc/components| holds a list of further |
|
301 |
sub-components of the same structure. The directory specifications |
|
302 |
given here can be either absolute (with leading \verb|/|) or |
|
303 |
relative to the component's main directory. |
|
304 |
||
305 |
\end{itemize} |
|
306 |
||
307 |
The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} |
|
308 |
itself. After initializing all of its sub-components recursively, |
|
309 |
\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} is included in the same manner (if |
|
310 |
that directory exists). Thus users can easily add private |
|
311 |
components to \verb|$ISABELLE_HOME_USER/etc/components|.% |
|
312 |
\end{isamarkuptext}% |
|
313 |
\isamarkuptrue% |
|
314 |
% |
|
28222 | 315 |
\isamarkupsection{The raw Isabelle process% |
316 |
} |
|
317 |
\isamarkuptrue% |
|
318 |
% |
|
319 |
\begin{isamarkuptext}% |
|
28505 | 320 |
The \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}} executable runs bare-bones |
321 |
Isabelle logic sessions --- either interactively or in batch mode. |
|
322 |
It provides an abstraction over the underlying ML system, and over |
|
323 |
the actual heap file locations. Its usage is: |
|
28222 | 324 |
|
325 |
\begin{ttbox} |
|
28238 | 326 |
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT] |
28222 | 327 |
|
328 |
Options are: |
|
329 |
-I startup Isar interaction mode |
|
330 |
-P startup Proof General interaction mode |
|
331 |
-S secure mode -- disallow critical operations |
|
332 |
-W OUTPUT startup process wrapper, with messages going to OUTPUT stream |
|
333 |
-X startup PGIP interaction mode |
|
334 |
-e MLTEXT pass MLTEXT to the ML session |
|
335 |
-f pass 'Session.finish();' to the ML session |
|
336 |
-m MODE add print mode for output |
|
337 |
-q non-interactive session |
|
338 |
-r open heap file read-only |
|
339 |
-u pass 'use"ROOT.ML";' to the ML session |
|
340 |
-w reset write permissions on OUTPUT |
|
341 |
||
342 |
INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps. |
|
343 |
These are either names to be searched in the Isabelle path, or |
|
344 |
actual file names (containing at least one /). |
|
345 |
If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system. |
|
346 |
\end{ttbox} |
|
347 |
||
348 |
Input files without path specifications are looked up in the |
|
349 |
\hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}} setting, which may consist of multiple |
|
350 |
components separated by colons --- these are tried in the given |
|
351 |
order with the value of \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} appended |
|
352 |
internally. In a similar way, base names are relative to the |
|
353 |
directory specified by \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}. In any case, |
|
354 |
actual file locations may also be given by including at least one |
|
355 |
slash (\verb|/|) in the name (hint: use \verb|./| to |
|
356 |
refer to the current directory).% |
|
357 |
\end{isamarkuptext}% |
|
358 |
\isamarkuptrue% |
|
359 |
% |
|
360 |
\isamarkupsubsubsection{Options% |
|
361 |
} |
|
362 |
\isamarkuptrue% |
|
363 |
% |
|
364 |
\begin{isamarkuptext}% |
|
365 |
If the input heap file does not have write permission bits set, or |
|
366 |
the \verb|-r| option is given explicitely, then the session |
|
367 |
started will be read-only. That is, the ML world cannot be |
|
368 |
committed back into the image file. Otherwise, a writable session |
|
369 |
enables commits into either the input file, or into another output |
|
370 |
heap file (if that is given as the second argument on the command |
|
371 |
line). |
|
372 |
||
373 |
The read-write state of sessions is determined at startup only, it |
|
374 |
cannot be changed intermediately. Also note that heap images may |
|
375 |
require considerable amounts of disk space (approximately |
|
376 |
50--200~MB). Users are responsible for themselves to dispose their |
|
377 |
heap files when they are no longer needed. |
|
378 |
||
379 |
\medskip The \verb|-w| option makes the output heap file |
|
380 |
read-only after terminating. Thus subsequent invocations cause the |
|
381 |
logic image to be read-only automatically. |
|
382 |
||
383 |
\medskip Using the \verb|-e| option, arbitrary ML code may be |
|
384 |
passed to the Isabelle session from the command line. Multiple |
|
385 |
\verb|-e|'s are evaluated in the given order. Strange things |
|
386 |
may happen when errorneous ML code is provided. Also make sure that |
|
387 |
the ML commands are terminated properly by semicolon. |
|
388 |
||
389 |
\medskip The \verb|-u| option is a shortcut for \verb|-e| passing ``\verb|use "ROOT.ML";|'' to the ML session. |
|
390 |
The \verb|-f| option passes ``\verb|Session.finish();|'', which is intended mainly for administrative |
|
391 |
purposes. |
|
392 |
||
393 |
\medskip The \verb|-m| option adds identifiers of print modes |
|
394 |
to be made active for this session. Typically, this is used by some |
|
395 |
user interface, e.g.\ to enable output of proper mathematical |
|
396 |
symbols. |
|
397 |
||
398 |
\medskip Isabelle normally enters an interactive top-level loop |
|
399 |
(after processing the \verb|-e| texts). The \verb|-q| |
|
400 |
option inhibits interaction, thus providing a pure batch mode |
|
401 |
facility. |
|
402 |
||
403 |
\medskip The \verb|-I| option makes Isabelle enter Isar |
|
404 |
interaction mode on startup, instead of the primitive ML top-level. |
|
405 |
The \verb|-P| option configures the top-level loop for |
|
406 |
interaction with the Proof General user interface, and the |
|
407 |
\verb|-X| option enables XML-based PGIP communication. The |
|
408 |
\verb|-W| option makes Isabelle enter a special process |
|
409 |
wrapper for interaction via an external program; the protocol is a |
|
28238 | 410 |
stripped-down version of Proof General the interaction mode, see |
30195 | 411 |
also \hyperlink{file.~~/src/Pure/System/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}. |
28222 | 412 |
|
413 |
\medskip The \verb|-S| option makes the Isabelle process more |
|
414 |
secure by disabling some critical operations, notably runtime |
|
415 |
compilation and evaluation of ML source code.% |
|
416 |
\end{isamarkuptext}% |
|
417 |
\isamarkuptrue% |
|
418 |
% |
|
419 |
\isamarkupsubsubsection{Examples% |
|
420 |
} |
|
421 |
\isamarkuptrue% |
|
422 |
% |
|
423 |
\begin{isamarkuptext}% |
|
424 |
Run an interactive session of the default object-logic (as specified |
|
425 |
by the \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} setting) like this: |
|
426 |
\begin{ttbox} |
|
28238 | 427 |
isabelle-process |
28222 | 428 |
\end{ttbox} |
429 |
||
430 |
Usually \hyperlink{setting.ISABELLE-LOGIC}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}LOGIC}}}} refers to one of the standard |
|
431 |
logic images, which are read-only by default. A writable session |
|
432 |
--- based on \verb|FOL|, but output to \verb|Foo| (in the |
|
28238 | 433 |
directory specified by the \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} setting) --- |
28222 | 434 |
may be invoked as follows: |
435 |
\begin{ttbox} |
|
28238 | 436 |
isabelle-process FOL Foo |
28222 | 437 |
\end{ttbox} |
438 |
Ending this session normally (e.g.\ by typing control-D) dumps the |
|
439 |
whole ML system state into \verb|Foo|. Be prepared for several |
|
440 |
tens of megabytes. |
|
441 |
||
442 |
The \verb|Foo| session may be continued later (still in |
|
443 |
writable state) by: |
|
444 |
\begin{ttbox} |
|
28238 | 445 |
isabelle-process Foo |
28222 | 446 |
\end{ttbox} |
447 |
A read-only \verb|Foo| session may be started by: |
|
448 |
\begin{ttbox} |
|
28238 | 449 |
isabelle-process -r Foo |
28222 | 450 |
\end{ttbox} |
451 |
||
452 |
\medskip Note that manual session management like this does |
|
453 |
\emph{not} provide proper setup for theory presentation. This would |
|
28238 | 454 |
require the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility. |
28222 | 455 |
|
28238 | 456 |
\bigskip The next example demonstrates batch execution of Isabelle. |
457 |
We retrieve the \verb|FOL| theory value from the theory loader |
|
458 |
within ML: |
|
28222 | 459 |
\begin{ttbox} |
28238 | 460 |
isabelle-process -e 'theory "FOL";' -q -r FOL |
28222 | 461 |
\end{ttbox} |
462 |
Note that the output text will be interspersed with additional junk |
|
28238 | 463 |
messages by the ML runtime environment. The \verb|-W| option |
464 |
allows to communicate with the Isabelle process via an external |
|
465 |
program in a more robust fashion.% |
|
466 |
\end{isamarkuptext}% |
|
467 |
\isamarkuptrue% |
|
468 |
% |
|
28505 | 469 |
\isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}% |
28238 | 470 |
} |
471 |
\isamarkuptrue% |
|
472 |
% |
|
473 |
\begin{isamarkuptext}% |
|
474 |
All Isabelle related tools and interfaces are called via a common |
|
28505 | 475 |
wrapper --- \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}: |
28238 | 476 |
|
477 |
\begin{ttbox} |
|
28505 | 478 |
Usage: isabelle TOOL [ARGS ...] |
28238 | 479 |
|
28507 | 480 |
Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. |
28238 | 481 |
|
482 |
Available tools are: |
|
483 |
||
484 |
browser - Isabelle graph browser |
|
485 |
\dots |
|
486 |
\end{ttbox} |
|
487 |
||
488 |
In principle, Isabelle tools are ordinary executable scripts that |
|
489 |
are run within the Isabelle settings environment, see |
|
490 |
\secref{sec:settings}. The set of available tools is collected by |
|
28505 | 491 |
\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} from the directories listed in the \hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}} setting. Do not try to call the scripts directly |
28238 | 492 |
from the shell. Neither should you add the tool directories to your |
493 |
shell's search path!% |
|
494 |
\end{isamarkuptext}% |
|
495 |
\isamarkuptrue% |
|
496 |
% |
|
497 |
\isamarkupsubsubsection{Examples% |
|
498 |
} |
|
499 |
\isamarkuptrue% |
|
500 |
% |
|
501 |
\begin{isamarkuptext}% |
|
502 |
Show the list of available documentation of the current Isabelle |
|
503 |
installation like this: |
|
504 |
||
505 |
\begin{ttbox} |
|
28505 | 506 |
isabelle doc |
28238 | 507 |
\end{ttbox} |
508 |
||
509 |
View a certain document as follows: |
|
510 |
\begin{ttbox} |
|
28505 | 511 |
isabelle doc isar-ref |
28238 | 512 |
\end{ttbox} |
513 |
||
514 |
Create an Isabelle session derived from HOL (see also |
|
515 |
\secref{sec:tool-mkdir} and \secref{sec:tool-make}): |
|
516 |
\begin{ttbox} |
|
28505 | 517 |
isabelle mkdir HOL Test && isabelle make |
28238 | 518 |
\end{ttbox} |
28505 | 519 |
Note that \verb|isabelle mkdir| is usually only invoked once; |
28238 | 520 |
existing sessions (including document output etc.) are then updated |
28505 | 521 |
by \verb|isabelle make| alone.% |
28222 | 522 |
\end{isamarkuptext}% |
523 |
\isamarkuptrue% |
|
524 |
% |
|
525 |
\isadelimtheory |
|
526 |
% |
|
527 |
\endisadelimtheory |
|
528 |
% |
|
529 |
\isatagtheory |
|
530 |
\isacommand{end}\isamarkupfalse% |
|
531 |
% |
|
532 |
\endisatagtheory |
|
533 |
{\isafoldtheory}% |
|
534 |
% |
|
535 |
\isadelimtheory |
|
536 |
% |
|
537 |
\endisadelimtheory |
|
538 |
\end{isabellebody}% |
|
539 |
%%% Local Variables: |
|
540 |
%%% mode: latex |
|
541 |
%%% TeX-master: "root" |
|
542 |
%%% End: |