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