3188
|
1 |
|
|
2 |
% $Id$
|
|
3 |
|
7882
|
4 |
\chapter{The Isabelle system environment}
|
3188
|
5 |
|
7882
|
6 |
This manual describes Isabelle together with related tools and user interfaces
|
|
7 |
as seen from an outside, system oriented view. See also the \emph{Isabelle
|
|
8 |
Reference Manual}~\cite{isabelle-ref} and the \emph{Isabelle Isar Reference
|
|
9 |
Manual}~\cite{isabelle-isar-ref} for the actual Isabelle commands and
|
|
10 |
related functions.
|
3188
|
11 |
|
7849
|
12 |
\medskip The Isabelle system environment is based on a few general elements:
|
3188
|
13 |
\begin{itemize}
|
7882
|
14 |
\item The \emph{Isabelle settings mechanism}, which provides environment
|
|
15 |
variables to all Isabelle programs (including tools and user interfaces).
|
7849
|
16 |
\item \emph{Isabelle proper} (\ttindex{isabelle}), which invokes logic
|
3188
|
17 |
sessions, both interactively or in batch mode. In particular,
|
7849
|
18 |
\texttt{isabelle} abstracts over the invocation of the actual {\ML} system
|
|
19 |
to be used.
|
7882
|
20 |
\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}), which provides a
|
|
21 |
generic startup platform for Isabelle related utilities. Thus tools
|
|
22 |
automatically benefit from the settings mechanism.
|
|
23 |
\item The \emph{Isabelle interface wrapper} (\ttindex{Isabelle}\footnote{Note
|
|
24 |
the capital \texttt{I}!}), which provides some abstraction over the actual
|
|
25 |
user interface to be used.
|
3188
|
26 |
\end{itemize}
|
|
27 |
|
7882
|
28 |
\medskip The beginning user would probably just run one of the interfaces (by
|
|
29 |
invoking the capital \texttt{Isabelle}), and maybe some basic tools like
|
|
30 |
\texttt{doc} (see \S\ref{sec:tool-doc}). This assumes that the system has
|
|
31 |
already been installed, of course.\footnote{In case you have to do this
|
|
32 |
yourself, see the \ttindex{INSTALL} file in the top-level directory of the
|
|
33 |
distribution of how to proceed. Some binary packages are available as
|
|
34 |
well.}
|
3188
|
35 |
|
|
36 |
|
|
37 |
\section{Isabelle settings} \label{sec:settings}
|
|
38 |
|
|
39 |
The Isabelle system heavily depends on the \emph{settings
|
7882
|
40 |
mechanism}\indexbold{settings}. Basically, this is a statically scoped
|
|
41 |
collection of environment variables, such as \texttt{ISABELLE_HOME},
|
|
42 |
\texttt{ML_SYSTEM}, \texttt{ML_HOME}. These variables are \emph{not} intended
|
|
43 |
to be set directly from the shell, though. Isabelle employs a somewhat more
|
|
44 |
sophisticated scheme of \emph{settings files} --- one for site-wide defaults,
|
|
45 |
another for additional user-specific modifications. With all configuration
|
|
46 |
variables in at most two places, this scheme is more maintainable and
|
|
47 |
user-friendly than plain shell environment variables.
|
3188
|
48 |
|
7882
|
49 |
In particular, we avoid the typical situation where prospective users of a
|
|
50 |
software package are told to put several things into their shell startup
|
|
51 |
scripts, before being able to actually run it. Isabelle requires none such
|
|
52 |
administrative chores of its end-users --- the executables can be invoked
|
|
53 |
straight away. Occasionally, users would still want to put the Isabelle
|
|
54 |
\texttt{bin} directory into their shell's search path, but this is not
|
|
55 |
required.
|
3188
|
56 |
|
|
57 |
|
7882
|
58 |
\subsection{Creating the environment}
|
3188
|
59 |
|
7882
|
60 |
Whenever any of the Isabelle executables is run, their settings environment is
|
|
61 |
built as follows:
|
3188
|
62 |
|
|
63 |
\begin{enumerate}
|
7882
|
64 |
\item The special variable \settdx{ISABELLE_HOME} is determined automatically
|
|
65 |
from the location of the binary that has been run.
|
|
66 |
|
|
67 |
You should not try to set \texttt{ISABELLE_HOME} manually. Also note that
|
|
68 |
the Isabelle executables either have to be run from their original location
|
|
69 |
in the distribution directory, or via the executable objects created via the
|
|
70 |
\texttt{install} utility (see \S\ref{sec:tool-install}). Just doing a plain
|
|
71 |
copy of the \texttt{bin} files will not work!
|
|
72 |
|
|
73 |
\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
|
|
74 |
with the auto-export option for variables enabled.
|
|
75 |
|
3278
|
76 |
This file typically contains a rather long list of shell variable
|
7882
|
77 |
assigments, thus providing the site-wide default settings. The Isabelle
|
|
78 |
distribution already contains a global settings file with sensible defaults
|
|
79 |
for most variables. When installing the system, only a few of these have to
|
|
80 |
be adapted (most likely \texttt{ML_SYSTEM} etc.).
|
7849
|
81 |
|
|
82 |
\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
|
7882
|
83 |
run in the same way as the site default settings. Note that the variable
|
7849
|
84 |
\texttt{ISABELLE_HOME_USER} has already been set before --- usually to
|
|
85 |
\texttt{\~\relax/isabelle}.
|
7882
|
86 |
|
|
87 |
Thus individual users may override the site-wide defaults. See also file
|
|
88 |
\texttt{etc/user-settings.sample} in the distribution. Typically, a user
|
|
89 |
settings file would contain only a few lines, just the assigments that are
|
|
90 |
really changed. One should definitely \emph{not} start with a full copy the
|
|
91 |
basic \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very annoying
|
|
92 |
maintainance problems later, when the Isabelle installation is updated or
|
|
93 |
changed otherwise.
|
3188
|
94 |
|
|
95 |
\end{enumerate}
|
|
96 |
|
7882
|
97 |
Note that settings files are actually full GNU bash scripts. So one may use
|
|
98 |
complex shell commands, such as \texttt{if} or \texttt{case} statements, to
|
|
99 |
set variables depending on the system architecture or other environment
|
|
100 |
variables. Such advanced features should be added only with great care,
|
|
101 |
though. In particular, external environment references should be kept at a
|
|
102 |
minimum.
|
3188
|
103 |
|
3217
|
104 |
\medskip A few variables are somewhat special:
|
3188
|
105 |
\begin{itemize}
|
3217
|
106 |
\item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to
|
|
107 |
the absolute path names of the \texttt{isabelle} and
|
3188
|
108 |
\texttt{isatool} executables, respectively.
|
6414
|
109 |
|
|
110 |
\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have the {\ML}
|
|
111 |
system identifier (according to \texttt{ML_IDENTIFIER} automatically
|
|
112 |
appended to their values.
|
3188
|
113 |
\end{itemize}
|
|
114 |
|
7882
|
115 |
\medskip The Isabelle settings scheme is basically simple, but non-trivial.
|
|
116 |
For debugging purposes, the resulting environment may be inspected with the
|
|
117 |
\texttt{getenv} utility, see \S\ref{sec:tool-getenv}.
|
3188
|
118 |
|
|
119 |
|
|
120 |
\subsection{Common variables}
|
|
121 |
|
7882
|
122 |
This is a reference of common Isabelle settings variables. Note that the list
|
|
123 |
is somewhat open-ended. Third-party utilities or interfaces may add their own
|
|
124 |
selection. Variables that are special in some sense are marked with *.
|
3217
|
125 |
|
|
126 |
\begin{description}
|
7882
|
127 |
\item[\settdx{ISABELLE_HOME}*] is the location of the top-level Isabelle
|
|
128 |
distribution directory. This is automatically determined from the Isabelle
|
|
129 |
executable that has been invoked. Do not try to set \texttt{ISABELLE_HOME}
|
|
130 |
yourself from the shell.
|
|
131 |
|
3217
|
132 |
\item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of
|
7882
|
133 |
\texttt{ISABELLE_HOME}. The default value is \texttt{\~\relax/isabelle},
|
|
134 |
under rare circumstances this may be changed in the global setting file.
|
|
135 |
Typically, the \texttt{ISABELLE_HOME_USER} directory mimics
|
|
136 |
\texttt{ISABELLE_HOME} to some extend. In particular, site-wide defaults may
|
|
137 |
be overridden by a private \texttt{etc/settings}.
|
|
138 |
|
|
139 |
\item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to the full
|
|
140 |
path names of the \texttt{isabelle} and \texttt{isatool} executables,
|
|
141 |
respectively. Thus other tools and scripts need not assume that the
|
|
142 |
Isabelle \texttt{bin} directory is on the current search path of the shell.
|
6412
|
143 |
|
|
144 |
\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
|
6414
|
145 |
\settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
|
7882
|
146 |
system to be used for Isabelle. There is only a fixed set of admissable
|
|
147 |
\texttt{ML_SYSTEM} names (see the \texttt{etc/settings} file of the
|
|
148 |
distribution).
|
|
149 |
|
|
150 |
The actual compiler binary will be run from the directory \texttt{ML_HOME},
|
|
151 |
with \texttt{ML_OPTIONS} as first arguments on the command line. The
|
|
152 |
optional \texttt{ML_PLATFORM} may specify the binary format of ML heap
|
|
153 |
images, which is useful for cross-platform installations. The value of
|
|
154 |
\texttt{ML_IDENTIFIER} is automatically obtained by composing the
|
|
155 |
\texttt{ML_SYSTEM} and \texttt{ML_PLATFORM} values.
|
6414
|
156 |
|
|
157 |
\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by colons)
|
|
158 |
where Isabelle logic images may reside. Note that the value of
|
|
159 |
\texttt{ML_IDENTIFIER} is appended to each component automatically.
|
7882
|
160 |
|
|
161 |
\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should
|
|
162 |
be stored by default. The \texttt{ML_SYSTEM} identifier is appended here,
|
|
163 |
too.
|
|
164 |
|
|
165 |
\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory browser
|
|
166 |
information (HTML text, graph data, and printable documents) is stored (see
|
|
167 |
also \S\ref{sec:info}). The default value is
|
4555
|
168 |
\texttt{\$ISABELLE_HOME_USER/browser_info}.
|
7882
|
169 |
|
|
170 |
\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is
|
|
171 |
given explicitely by the user. The default value is \texttt{HOL}.
|
|
172 |
|
|
173 |
\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command
|
|
174 |
line of any \texttt{isatool usedir} invocation (see also
|
|
175 |
\S\ref{sec:tool-usedir}). This typically contains compilation options for
|
|
176 |
object-logics --- \texttt{usedir} is the basic utility for managing logic
|
|
177 |
sessions (cf.\ the \texttt{IsaMakefile}s in the distribution).
|
7849
|
178 |
|
|
179 |
\item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX},
|
|
180 |
\settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related
|
|
181 |
tools for Isabelle document preparation (see also \S\ref{sec:tool-latex}).
|
7882
|
182 |
|
|
183 |
\item[\settdx{ISABELLE_TOOLS}] is a colon separated list of directories that
|
|
184 |
are scanned by \texttt{isatool} for external utility programs (see also
|
|
185 |
\S\ref{sec:isatool}).
|
|
186 |
|
|
187 |
\item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories with
|
|
188 |
documentation files.
|
|
189 |
|
|
190 |
\item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying
|
|
191 |
\texttt{dvi} files.
|
|
192 |
|
|
193 |
\item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the Isabelle
|
|
194 |
symbol fonts are installed into your currently running X11 display server.
|
|
195 |
X11 fonts are a subtle issue, see \S\ref{sec:tool-installfonts} for more
|
|
196 |
information.
|
|
197 |
|
|
198 |
\item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any running
|
|
199 |
\texttt{isabelle} process derives an individual directory for temporary
|
|
200 |
files. The default is somewhere in \texttt{/tmp}.
|
|
201 |
|
|
202 |
\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the actual
|
|
203 |
user interface that the capital \texttt{Isabelle} should invoke. See
|
|
204 |
\S\ref{sec:interface} for more details.
|
3217
|
205 |
|
|
206 |
\end{description}
|
3188
|
207 |
|
|
208 |
|
|
209 |
\section{Isabelle proper --- \texttt{isabelle}}
|
|
210 |
|
7882
|
211 |
The \ttindex{isabelle} executable runs logic sessions --- either interactively
|
|
212 |
or in batch mode. It provides an abstraction over the underlying {\ML} system,
|
|
213 |
and over the actual heap file locations. Its usage is:
|
3188
|
214 |
\begin{ttbox}
|
|
215 |
Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
|
|
216 |
|
|
217 |
Options are:
|
5814
|
218 |
-I startup Isar interaction mode
|
3188
|
219 |
-e MLTEXT pass MLTEXT to the ML session
|
|
220 |
-m MODE add print mode for output
|
|
221 |
-q non-interactive session
|
|
222 |
-r open heap file read-only
|
4540
|
223 |
-u pass 'use"ROOT.ML";' to the ML session
|
|
224 |
-w reset write permissions on OUTPUT
|
3188
|
225 |
|
|
226 |
INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
|
|
227 |
These are either names to be searched in the Isabelle path, or actual
|
4540
|
228 |
file names (containing at least one /).
|
3188
|
229 |
If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
|
|
230 |
\end{ttbox}
|
|
231 |
Input files without path specifications are looked up in the
|
7849
|
232 |
\texttt{ISABELLE_PATH} setting, which may consist of multiple components
|
7882
|
233 |
separated by colons --- these are tried in the given order. Likewise, base
|
|
234 |
names are relative to the directory specified by \texttt{ISABELLE_OUTPUT}. In
|
|
235 |
any case, actual file locations may also be given by including at least one
|
|
236 |
slash (\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
|
7849
|
237 |
directory).
|
3188
|
238 |
|
|
239 |
|
|
240 |
\subsection*{Options}
|
|
241 |
|
3217
|
242 |
If the input heap file does not have write permission bits set, or the
|
7882
|
243 |
\texttt{-r} option is given explicitely, then the session started will be
|
|
244 |
read-only. That is, the {\ML} world cannot be committed back into the logic
|
|
245 |
image. Otherwise, a writable session enables commits into either the input
|
|
246 |
file, or into an alternative output heap file (in case that is given as the
|
|
247 |
second argument on the command line).
|
3217
|
248 |
|
7882
|
249 |
The read-write state of sessions is determined at startup only, it cannot be
|
|
250 |
changed intermediately. Also note that heap images may require considerable
|
|
251 |
amounts of disk space. Users are responsible themselves to dispose their heap
|
|
252 |
files when they are no longer needed.
|
3188
|
253 |
|
7882
|
254 |
\medskip The \texttt{-w} option makes the output heap file read-only after
|
|
255 |
terminating. Thus subsequent invocations cause the logic image to be
|
|
256 |
read-only automatically.
|
4540
|
257 |
|
7882
|
258 |
\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
|
|
259 |
the Isabelle session from the command line. Multiple \texttt{-e}'s are
|
|
260 |
evaluated in the given order. Strange things may happen when errorneous {\ML}
|
|
261 |
code is provided. Also make sure that the {\ML} commands are terminated
|
|
262 |
properly by semicolon.
|
3188
|
263 |
|
4540
|
264 |
\medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
|
4555
|
265 |
``\texttt{use"ROOT.ML";}'' to the {\ML} session.
|
4540
|
266 |
|
7882
|
267 |
\medskip The \texttt{-m} option adds identifiers of print modes to be made
|
|
268 |
active for this session. Typically, this is used by some user interface, e.g.\
|
|
269 |
to enable output of mathematical symbols from a special screen font.
|
3217
|
270 |
|
7882
|
271 |
\medskip Isabelle normally enters an interactive top-level loop (after
|
|
272 |
processing the \texttt{-e} texts). The \texttt{-q} option inhibits
|
|
273 |
interaction, thus providing a pure batch mode facility.
|
5814
|
274 |
|
|
275 |
\medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
|
7882
|
276 |
startup, instead of the primitive {\ML} top-level. User interfaces (such
|
|
277 |
Proof~General) take care of this switch automatically.
|
3188
|
278 |
|
|
279 |
|
|
280 |
\subsection*{Examples}
|
|
281 |
|
3217
|
282 |
Run an interactive session of the default object-logic (as specified
|
|
283 |
by the \texttt{ISABELLE_LOGIC} setting) like this:
|
3188
|
284 |
\begin{ttbox}
|
|
285 |
isabelle
|
|
286 |
\end{ttbox}
|
3217
|
287 |
Usually \texttt{ISABELLE_LOGIC} refers to one of the standard logic
|
|
288 |
images, which are read-only by default. A writable session --- based
|
|
289 |
on \texttt{FOL}, but output to \texttt{Foo} (in the directory
|
|
290 |
specified by the \texttt{ISABELLE_OUTPUT} setting) --- may be invoked
|
|
291 |
as follows:
|
3188
|
292 |
\begin{ttbox}
|
|
293 |
isabelle FOL Foo
|
|
294 |
\end{ttbox}
|
3217
|
295 |
Ending this session normally (e.g.\ by typing control-D) dumps the
|
3188
|
296 |
whole {\ML} system state into \texttt{Foo}. Be prepared for several
|
|
297 |
megabytes!
|
|
298 |
|
3217
|
299 |
The \texttt{Foo} session may be continued later (still in writable
|
3262
|
300 |
state) by:
|
3188
|
301 |
\begin{ttbox}
|
|
302 |
isabelle Foo
|
|
303 |
\end{ttbox}
|
3217
|
304 |
A read-only \texttt{Foo} session may be started by:
|
|
305 |
\begin{ttbox}
|
|
306 |
isabelle -r Foo
|
|
307 |
\end{ttbox}
|
3188
|
308 |
|
7849
|
309 |
\medskip Note that manual session management like this does \emph{not} provide
|
|
310 |
proper setup for theory presentation. This would require the \texttt{usedir}
|
|
311 |
utility, see \S\ref{sec:tool-usedir}.
|
|
312 |
|
|
313 |
\bigskip The next example demonstrates batch execution of Isabelle. We print a
|
|
314 |
certain theorem of \texttt{FOL}:
|
3188
|
315 |
\begin{ttbox}
|
|
316 |
isabelle -e "prth allE;" -q -r FOL
|
|
317 |
\end{ttbox}
|
7882
|
318 |
Note that the output text will be interspersed with additional junk messages
|
|
319 |
by the {\ML} runtime environment.
|
3188
|
320 |
|
3217
|
321 |
|
|
322 |
\section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
|
|
323 |
|
3278
|
324 |
All Isabelle related utilities are called via a common wrapper ---
|
|
325 |
\ttindex{isatool}:
|
|
326 |
\begin{ttbox}
|
|
327 |
Usage: isatool TOOL [ARGS ...]
|
|
328 |
|
|
329 |
Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
|
|
330 |
for more specific help.
|
|
331 |
|
|
332 |
Available tools are:
|
|
333 |
|
7882
|
334 |
browser - Isabelle graph browser
|
3278
|
335 |
doc - view Isabelle documentation
|
4540
|
336 |
\dots
|
3278
|
337 |
\end{ttbox}
|
7882
|
338 |
Basically, Isabelle tools are ordinary executable scripts. These are run
|
|
339 |
within the same Isabelle settings environment, see \S\ref{sec:settings}. The
|
|
340 |
set of available tools is collected by \texttt{isatool} from the directories
|
|
341 |
listed in the \texttt{ISABELLE_TOOLS} setting. Do not try to call the scripts
|
|
342 |
directly. Neither should you add the tool directories to your shell's search
|
|
343 |
path.
|
3278
|
344 |
|
3217
|
345 |
|
|
346 |
\section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface}
|
|
347 |
|
7208
|
348 |
Isabelle is a generic theorem prover, even w.r.t.\ its user interface. The
|
|
349 |
\ttindex{Isabelle} command (note the capital \texttt{I}) provides a uniform
|
|
350 |
way for end-users to invoke a certain interface; which one to start actually
|
7882
|
351 |
is determined by the \settdx{ISABELLE_INTERFACE} setting variable. Also note
|
|
352 |
that the \texttt{install} utility provides some options to install desktop
|
|
353 |
environment icons as well (see \S\ref{sec:tool-install}).
|
7208
|
354 |
|
7849
|
355 |
An interface may be specified either by giving an identifier that the Isabelle
|
|
356 |
distribution knows about, or by specifying an actual path name (containing a
|
|
357 |
slash ``\texttt{/}'') of some executable. Currently, the following interfaces
|
|
358 |
are available:
|
|
359 |
|
|
360 |
\begin{itemize}
|
7882
|
361 |
\item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus
|
3278
|
362 |
\texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
|
7849
|
363 |
|
|
364 |
\item \texttt{xterm} refers to a simple xterm based interface which is part of
|
3278
|
365 |
the Isabelle distribution.
|
7208
|
366 |
|
7849
|
367 |
\item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user
|
7208
|
368 |
interface!Isamode} for emacs. Isabelle just provides a wrapper for this,
|
|
369 |
the actual Isamode distribution is available elsewhere \cite{isamode}.
|
7849
|
370 |
|
|
371 |
\item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} of
|
|
372 |
LFCS Edinburgh is distributed with separate interface wrapper scripts for
|
|
373 |
Isabelle. See below for more details.
|
|
374 |
\end{itemize}
|
3278
|
375 |
|
7849
|
376 |
The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}. This
|
|
377 |
interface runs \texttt{isabelle} within its own \textsl{xterm} window.
|
7882
|
378 |
Usually, display of mathematical symbols from the Isabelle font is enabled as
|
|
379 |
well (see \S\ref{sec:tool-installfonts} for X11 font configuration issues).
|
7849
|
380 |
Furthermore, different kinds of identifiers in logical terms are highlighted
|
|
381 |
appropriately, e.g.\ free variables in bold and bound variables underlined.
|
7861
|
382 |
There are some more options available, just pass ``\texttt{-?}'' to get the
|
|
383 |
usage printed.
|
5364
|
384 |
|
7849
|
385 |
\medskip Proof~General\index{user interface!Proof General} is a much more
|
|
386 |
advanced interface. It supports both classic Isabelle (as
|
7208
|
387 |
\texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}).
|
7882
|
388 |
Note that the latter is inherently more robust.
|
7849
|
389 |
|
7882
|
390 |
Using the Isabelle interface wrapper scripts as provided by Proof~General, a
|
|
391 |
typical setup for Isabelle/Isar would be like this:
|
7208
|
392 |
\begin{ttbox}
|
|
393 |
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
|
7882
|
394 |
PROOFGENERAL_OPTIONS="-u false"
|
7208
|
395 |
\end{ttbox}
|
7849
|
396 |
Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
|
|
397 |
the Proof~General Lisp packages. There are some options available, such as
|
|
398 |
\texttt{-l} for passing the logic image to be used.
|
7208
|
399 |
|
7849
|
400 |
\medskip Note that the world may be also seen the other way round: Emacs may
|
7882
|
401 |
be started first (with proper setup of Proof~General mode), and
|
|
402 |
\texttt{isabelle} run from within. This requires further Emacs Lisp
|
7849
|
403 |
configuration, see the Proof~General documentation \cite{proofgeneral} for
|
|
404 |
more information.
|
5364
|
405 |
|
6412
|
406 |
%%% Local Variables:
|
5364
|
407 |
%%% mode: latex
|
|
408 |
%%% TeX-master: "system"
|
6412
|
409 |
%%% End:
|