372 slash ``\texttt{/}'') of some executable. Currently, the following interfaces |
372 slash ``\texttt{/}'') of some executable. Currently, the following interfaces |
373 are available: |
373 are available: |
374 |
374 |
375 \begin{itemize} |
375 \begin{itemize} |
376 \item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus |
376 \item \texttt{none} is just a pass-through to plain \texttt{isabelle}. Thus |
377 \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}. |
377 \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}. This is |
378 |
378 the factory default. |
|
379 |
379 \item \texttt{xterm} refers to a simple \textsl{xterm} based interface which |
380 \item \texttt{xterm} refers to a simple \textsl{xterm} based interface which |
380 is part of the Isabelle distribution. |
381 is part of the Isabelle distribution. |
|
382 |
|
383 This interface runs \texttt{isabelle} within its own \textsl{xterm} window. |
|
384 Usually, display of mathematical symbols from the Isabelle font is enabled |
|
385 as well (see \S\ref{sec:tool-installfonts} for X11 font configuration |
|
386 issues). Furthermore, different kinds of identifiers in logical terms are |
|
387 highlighted appropriately, e.g.\ free variables in bold and bound variables |
|
388 underlined. There are some more options available, just pass |
|
389 ``\texttt{-?}'' to get the usage printed. |
381 |
390 |
382 \item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user |
391 \item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user |
383 interface!Isamode} for emacs. Isabelle just provides a wrapper for this, |
392 interface!Isamode} for emacs. Isabelle just provides a wrapper for this, |
384 the actual Isamode distribution is available elsewhere \cite{isamode}. |
393 the actual Isamode distribution is available elsewhere \cite{isamode}. |
385 |
394 |
386 \item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} is |
395 \item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} is |
387 distributed with separate interface wrapper scripts for Isabelle. See below |
396 an advanced interface for common theorem proving environments. It has |
388 for more details. |
397 become the de-facto standard for Isabelle recently, supporting both the old |
|
398 ML top-level of classic Isabelle and the more convenient Isabelle/Isar |
|
399 interpreter loop. The Proof~General distributions includes separate |
|
400 interface wrapper scripts (in \texttt{ProofGeneral/isa} and |
|
401 \texttt{ProofGeneral/isar}). The canonical settings for Isabelle/Isar are |
|
402 as follows: |
|
403 \begin{ttbox} |
|
404 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface |
|
405 PROOFGENERAL_OPTIONS="" |
|
406 \end{ttbox} |
|
407 Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of |
|
408 the Proof~General Lisp packages. There are some options available, such as |
|
409 \texttt{-l} for passing the logic image to be used, or \texttt{-m} to tune |
|
410 the standard print mode. |
|
411 |
|
412 \medskip Note that the world may be also seen the other way round: Emacs may |
|
413 be started first (with proper setup of Proof~General mode), and |
|
414 \texttt{isabelle} run from within. This requires further Emacs Lisp |
|
415 configuration, see the Proof~General documentation \cite{proofgeneral} for |
|
416 more information. |
|
417 |
389 \end{itemize} |
418 \end{itemize} |
390 |
|
391 The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}. This |
|
392 interface runs \texttt{isabelle} within its own \textsl{xterm} window. |
|
393 Usually, display of mathematical symbols from the Isabelle font is enabled as |
|
394 well (see \S\ref{sec:tool-installfonts} for X11 font configuration issues). |
|
395 Furthermore, different kinds of identifiers in logical terms are highlighted |
|
396 appropriately, e.g.\ free variables in bold and bound variables underlined. |
|
397 There are some more options available, just pass ``\texttt{-?}'' to get the |
|
398 usage printed. |
|
399 |
|
400 \medskip Proof~General\index{user interface!Proof General} is a much more |
|
401 advanced interface. It supports both classic Isabelle (as |
|
402 \texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}). |
|
403 Note that the latter is inherently more robust. |
|
404 |
|
405 Using the Isabelle interface wrapper scripts as provided by Proof~General, a |
|
406 typical setup for Isabelle/Isar would be like this: |
|
407 \begin{ttbox} |
|
408 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface |
|
409 PROOFGENERAL_OPTIONS="-u false" |
|
410 \end{ttbox} |
|
411 Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of |
|
412 the Proof~General Lisp packages. There are some options available, such as |
|
413 \texttt{-l} for passing the logic image to be used. |
|
414 |
|
415 \medskip Note that the world may be also seen the other way round: Emacs may |
|
416 be started first (with proper setup of Proof~General mode), and |
|
417 \texttt{isabelle} run from within. This requires further Emacs Lisp |
|
418 configuration, see the Proof~General documentation \cite{proofgeneral} for |
|
419 more information. |
|
420 |
419 |
421 %%% Local Variables: |
420 %%% Local Variables: |
422 %%% mode: latex |
421 %%% mode: latex |
423 %%% TeX-master: "system" |
422 %%% TeX-master: "system" |
424 %%% End: |
423 %%% End: |