# HG changeset patch # User wenzelm # Date 953329865 -3600 # Node ID 76d8d8aab881fe7a8de4416b2e3bc7eec156ccda # Parent d22fcea34cb7938e0d67cb2fab508f8af6f90208 simplified Proof General setup; diff -r d22fcea34cb7 -r 76d8d8aab881 doc-src/IsarRef/intro.tex --- a/doc-src/IsarRef/intro.tex Fri Mar 17 22:50:41 2000 +0100 +++ b/doc-src/IsarRef/intro.tex Fri Mar 17 22:51:05 2000 +0100 @@ -3,6 +3,8 @@ \section{Quick start} +\subsection{Terminal sessions} + Isar is already part of Isabelle (as of version Isabelle99, or later). The \texttt{isabelle} binary provides option \texttt{-I} to run the Isar interaction loop at startup, rather than the plain ML top-level. Thus the @@ -18,59 +20,66 @@ Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the \texttt{help} command prints a list of available language elements. -Plain TTY-based interaction like this used to be quite feasible with + +\subsection{The Proof~General interface} + +Plain TTY-based interaction as above used to be quite feasible with traditional tactic based theorem proving, but developing Isar documents -demands some better user-interface support. \emph{Proof~General}\index{Proof - General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based -environment for interactive theorem provers that does all the cut-and-paste -and forward-backward walk through the text in a very neat way. Note that in -Isabelle/Isar, the current position within a partial proof document is equally -important than the actual proof state. Thus Proof~General provides the -canonical working environment for Isabelle/Isar, both for getting acquainted -(e.g.\ by replaying existing Isar documents) and real production work. +demands some better user-interface support. David Aspinall's +\emph{Proof~General}\index{Proof General} environment +\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs-based interface +for interactive theorem provers that does all the cut-and-paste and +forward-backward walk through the text in a very neat way. In Isabelle/Isar, +the current position within a partial proof document is equally important than +the actual proof state. Thus Proof~General provides the canonical working +environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying +existing Isar documents) and real production work. \medskip The easiest way to use Proof~General is to make it the default Isabelle user -interface. Just put something like this into your Isabelle settings file (see -also \cite{isabelle-sys}): +interface (see also \cite{isabelle-sys}). Just put something like this into +your Isabelle settings file: \begin{ttbox} ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface -PROOFGENERAL_OPTIONS="-u false" +PROOFGENERAL_OPTIONS="" \end{ttbox} You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the actual installation directory of Proof~General. From now on, the capital \texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar} interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for - classic Isabelle tactic scripts.} Its usage is as follows: -\begin{ttbox} -Usage: interface [OPTIONS] [FILES ...] - - Options are: - -l NAME logic image name (default $ISABELLE_LOGIC=HOL) - -p NAME Emacs program name (default xemacs) - -u BOOL use .emacs file (default true) - -w BOOL use window system (default true) + classic Isabelle tactic scripts.} - Starts Proof General for Isabelle/Isar with proof documents FILES - (default Scratch.thy). +%FIXME remove? +%Its usage is as follows: +%\begin{ttbox} +%Usage: interface [OPTIONS] [FILES ...] +% +% Options are: +% -l NAME logic image name (default $ISABELLE_LOGIC=HOL) +% -p NAME Emacs program name (default xemacs) +% -u BOOL use .emacs file (default true) +% -w BOOL use window system (default true) +% -x BOOL enable x-symbol package +% Starts Proof General for Isabelle/Isar with proof documents FILES +% (default Scratch.thy). +% +% PROOFGENERAL_OPTIONS= +%\end{ttbox} %$ - PROOFGENERAL_OPTIONS= -\end{ttbox} %$ -Apart from the command line, the defaults for these options may be overridden -via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, plain GNU -Emacs may be configured as follows: -\begin{ttbox} -PROOFGENERAL_OPTIONS="-u false -p emacs" -\end{ttbox} +The interface script provides several options (pass ``\texttt{-?}'' to see its +usage). Apart from the command line, the defaults for these options may be +overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For +example, plain GNU Emacs instead of XEmacs (which is the default) may be +configured in Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="-p + emacs"}. Occasionally, a user's \texttt{.emacs} file contains material that is incompatible with the version of (X)Emacs that Proof~General prefers. Then -proper startup may be still achieved by using the \texttt{-u false} -option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el} - occurring in \texttt{\$ISABELLE_HOME/etc} or - \texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the - Proof~General interface script as well.} +proper startup may be still achieved by using the \texttt{-u false} option. +Also note that any Emacs lisp file \texttt{proofgeneral-settings.el} occurring +in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is +automatically loaded by the Proof~General interface script as well. \medskip @@ -80,9 +89,17 @@ Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy \end{ttbox} Users of XEmacs may note the tool bar for navigating forward and backward -through the text. Consult the Proof~General documentation \cite{proofgeneral} -for further basic command sequences, such as ``\texttt{c-c return}'' or -``\texttt{c-c u}''. +through the text. Consult the Proof~General documentation +\cite{proofgeneral,Aspinall:TACAS:2000} for further basic command sequences, +such as ``\texttt{c-c return}'' or ``\texttt{c-c u}''. + +\medskip + +Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which +provides a nice way to get proper mathematical symbols displayed on screen. +Just pass option \texttt{-x true} to the Isabelle interface script, or check +the appropriate menu setting by hand. In any case, the X-Symbol package +already must have been properly installed. \section{Isabelle/Isar theories} @@ -94,7 +111,7 @@ \item A \emph{formal proof document language} designed to support intelligible semi-automated reasoning. Instead of putting together unreadable tactic scripts, the author is enabled to express the reasoning in way that is close - to mathematical practice. + to usual mathematical practice. \end{enumerate} The Isar proof language is embedded into the new theory format as a proper @@ -146,12 +163,13 @@ \begin{tabular}{l} \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ \url{http://isabelle.in.tum.de/library/} \\ + \url{http://isabelle.in.tum.de/Isar/} \\ \end{tabular} \end{center} See \texttt{HOL/Isar_examples} for a collection of introductory examples, and \texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from -browsable HTML sources, both sessions provide actual documents (in PDF). +plain HTML sources, these sessions also provide actual documents (in PDF). %%% Local Variables: %%% mode: latex