# HG changeset patch # User wenzelm # Date 864227506 -7200 # Node ID 636322bfd05798a3b047aa0aa55311336a918cdc # Parent d95d209ae1c2a21cd41abd4e483d3db7f2d922f2 release version (sort of); diff -r d95d209ae1c2 -r 636322bfd057 doc-src/System/basics.tex --- a/doc-src/System/basics.tex Wed May 21 17:11:24 1997 +0200 +++ b/doc-src/System/basics.tex Wed May 21 17:11:46 1997 +0200 @@ -55,10 +55,11 @@ In particular, we avoid the typical situation where prospective users of a software package are told to put this and that in their shell -startup scripts. Isabelle requires none such administrative chores of -its end-users --- the executables can be run straight away. Usually, -users would want to put the Isabelle \texttt{bin} directory into their -shell's search path, of course. +startup scripts, before being able to actually run it. Isabelle +requires none such administrative chores of its end-users --- the +executables can be invoked straight away. Usually, users would just +want to put the Isabelle \texttt{bin} directory into their shell's +search path, of course. \subsection{Building the environment} @@ -78,11 +79,11 @@ \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script with the auto-export option for variables enabled. - This file typically contains a rather long list of assigments - \texttt{FOO="bar"}, thus providing the site-wide default settings. - The Isabelle distribution already contains a global settings file - with sensible defaults for most variables. When installing the - system, only a few of these have to be adapted (most likely + This file typically contains a rather long list of shell variable + assigments, thus providing the site-wide default settings. The + Isabelle distribution already contains a global settings file with + sensible defaults for most variables. When installing the system, + only a few of these have to be adapted (most likely \texttt{ML_SYSTEM} etc.). \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it @@ -92,9 +93,9 @@ Thus individual users may override the site-wide defaults. See also file \texttt{etc/user-settings.sample} in the distribution. - Typically, user settings are a few lines only, just containing the - assigments that are really needed. One should definitely \emph{not} - start with a full copy the central + Typically, user settings should be a few lines only, just containing + the assigments that are really needed. One should definitely + \emph{not} start with a full copy the central \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very annoying maintainance problems later, when the Isabelle installation is updated or changed otherwise. @@ -171,8 +172,8 @@ \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is given explicitely by the user --- e.g.\ when running \texttt{isabelle} directly, or some user interface. - -\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitely prefixed to the + +\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command line of any \texttt{isatool usedir} invocation (see also \S\ref{sec:tool-usedir}). This typically contains compilation options for object-logics --- \texttt{usedir} is the basic utility @@ -224,11 +225,11 @@ \end{ttbox} Input files without path specifications are looked up in the \texttt{ISABELLE_PATH} setting, which may consist of multiple -components separated by colons --- these are tried in order. Short -output names are relative to the directory specified by -\texttt{ISABELLE_OUTPUT} setting. In any case, actual file locations -may also be given by including at least one \texttt{/} in the name -(hint: use \texttt{./} to refer to the current directory). +components separated by colons --- these are tried in order. +Likewise, short output names are relative to the directory specified +by \texttt{ISABELLE_OUTPUT}. In any case, actual file locations may +also be given by including at least one \texttt{/} in the name (hint: +use \texttt{./} to refer to the current directory). \subsection*{Options} @@ -254,9 +255,7 @@ \medskip The \texttt{-m} option adds identifiers of print modes to be made active for this session. Typically, this is used by some user interface, for example to enable output of mathematical symbols from a -special screen font. See also \S\ref{sec:tool-installfonts} about -fonts and the \emph{Isabelle Reference Manual} about print modes in -general. +special screen font. \medskip Isabelle normally enters an interactice {\ML} top-level loop (after processing the \texttt{-e} texts). The \texttt{-q} option @@ -292,7 +291,7 @@ isabelle -r Foo \end{ttbox} One may also use something like \texttt{chmod~-w} on the logic image -to have them read-only automatically. +to have it read-only automatically. \medskip The next example demonstrates batch execution of Isabelle. We print a certain theorem of \texttt{FOL}: @@ -305,8 +304,58 @@ \section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool} -FIXME +All Isabelle related utilities are called via a common wrapper --- +\ttindex{isatool}: +\begin{ttbox} +Usage: isatool TOOL [ARGS ...] + + Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL + for more specific help. + + Available tools are: + + doc - view Isabelle documentation + \(\vdots\) +\end{ttbox} +Basically, Isabelle tools are ordinary executable scripts. These are +run within the same settings environment as Isabelle proper, though, +see \S\ref{sec:settings}. The set of available tools is collected by +isatool from the directories listed in the \texttt{ISABELLE_TOOLS} +setting. Do not try to call the scripts directly. Neither should you +add the tools directories to your shell's search path. + + +\medskip See chapter~\ref{ch:tools} for descriptions of most utilities +that come with the Isabelle distributions. Third-parties may add their +own, of course. + \section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface} -FIXME +Isabelle is a generic theorem prover, even w.r.t.\ its user interface. +The \ttindex{Isabelle} command (note the capital \texttt{I}) provides +a uniform way for end-users to invoke a certain interface. Which one +to actually start is determined by the \settdx{ISABELLE_INTERFACE} +setting variable. Currently, the following are recognized: +\begin{ttdescription} +\item[none] is just a pass-through to \texttt{isabelle}. Thus + \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}. + +\item[xterm] refers to a simple xterm-based interface which is part of + the Isabelle distribution. + +\item[emacs] refers to David Aspinall's \emph{Isamode} for emacs. + Isabelle just provides a wrapper for this, the actual Isamode + distribution is available elsewhere. +\end{ttdescription} + +The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}. +This interface runs \texttt{isabelle} within its own xterm window. +Usually, display of mathematical symbols from the Isabelle font is +also enabled (see \S\ref{sec:tool-installfonts} for font configuration +issues). Furthermore, different kinds of identifiers in logical terms +are highlighted appropriately, e.g.\ free variables in bold and bound +variables underlined. + +There are some more options available. Just pass \texttt{-?} to the +\texttt{xterm} interface to have its usage printed. diff -r d95d209ae1c2 -r 636322bfd057 doc-src/System/fonts.tex --- a/doc-src/System/fonts.tex Wed May 21 17:11:24 1997 +0200 +++ b/doc-src/System/fonts.tex Wed May 21 17:11:46 1997 +0200 @@ -1,15 +1,15 @@ \chapter{Fonts and character encodings} -With print modes being now available in Isabelle, variant forms of -output have become very easy. As the canonical application of this -feature, {\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF) -support optional input and output of nice mathematical symbols as an -built-in option. +With the advent of print modes in Isabelle, variant forms of output +have become very easy. As the canonical application of this feature, +{\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF) support +optional input and output of nice mathematical symbols as an built-in +option. Symbolic output is enabled by activating the \ttindex{symbols} print mode. User interfaces (e.g.\ \texttt{isa-xterm}, see -\S\ref{sec:isa-xterm}) usually do this already by default. +\S\ref{sec:interface}) usually do this already by default. \medskip Displaying non-standard characters requires special screen fonts, of course. The \texttt{installfonts} utility takes care of @@ -48,9 +48,9 @@ \medskip In the simplest situation, X11 is used only locally, i.e.\ the client program (Isabelle) and the display server are run on the same machine. In this case, most X11 display servers should be happy -by being about the directory where the fonts reside as follows: +by being told about the Isabelle fonts directory as follows: \begin{ttbox} -ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash" +ISABELLE_INSTALLFONTS="xset fp+{\thinspace}$ISABELLE_HOME/lib/fonts; xset fp rehash" \end{ttbox} The same also works for remote X11 sessions in a somewhat homogeneous network, where the X11 display machine mounts the Isabelle @@ -64,34 +64,33 @@ of course. It is even \emph{impossible} for proper X terminals that do not have their own file system. -A much better solution to this problem is to have an X11 \emph{font - server} offer the Isabelle fonts to any X11 display on the network. -There is already a font server running at Munich. So in case you have -a sensible Internet connection, you may plug attach yourself as -follows: +A much better solution is to have a \emph{font server} offer the +Isabelle fonts to any X display on the network. There is already a +suitable server running at Munich. So in case you have a sensible +Internet connection, you may just attach yourself as follows: \begin{ttbox} ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" \end{ttbox} -\medskip In the (rare?) case that neither local fonts work, nor +\medskip In the unfortunate case that neither local fonts work, nor accessing our world-wide font service is practical, it might be best -to start your own in-house font service. This is in principle quite -easy to setup. The program is called \texttt{xfs} (or just -\texttt{fs)}, see the \texttt{man} pages of your system. There is an -example configuration available in the \texttt{lib/fontserver} -directory of the Isabelle distribution. +to start your own in-house font service. This is in principle easy to +setup. The program is called \texttt{xfs} (or just \texttt{fs)}, see +the \texttt{man} pages of your system. There is an example +configuration available in the \texttt{lib/fontserver} directory of +the Isabelle distribution. \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}} \label{sec:tool-symbolinput} -Processing non-\textsc{ascii} text is notoriously difficult. Some -{\ML} systems reject character codes outside the range 32--127 as part -of literal string constants. In order to circumvent such restrictions, -Isabelle employs a general notation where glyphs are referred by some -symbolic name instead of their actual encoding. Its general form is -\texttt{$\backslash$<$charname$>}. +Processing non-\textsc{ascii} text is notoriously difficult. In +particular, some {\ML} systems reject character codes outside the +range 32--127 as part of literal string constants. In order to +circumvent such restrictions, Isabelle employs a general notation +where glyphs are referred by some symbolic name instead of their +actual encoding: Its general form is \verb|\<|$charname$\verb|>|. The \tooldx{symbolinput} utility converts a input stream encoded according to the standard Isabelle font layout into pure @@ -99,19 +98,20 @@ works from standard input to standard output, without any options available. -\medskip For example, the non-\textsc{ascii} input \texttt{"A $\land$ - B $\lor$ C"} is replaced by \texttt{"A $\backslash\backslash$ B - $\backslash\backslash$ C"}. +\medskip For example, the non-\textsc{ascii} input string \texttt{"A + $\land$ B $\lor$ C"} will be replaced by \verb|"A \\ B \\ C"|. +Note that the \verb|\| are escaped, accomodating concrete {\ML} string +syntax. \medskip In many cases, it might be wise not to rely on symbolic characters and avoid non-\textsc{ascii} text in files altogether. Then symbolic syntax would be really optional, with always suitable -\texttt{ascii} representations available. In theory definitions +\textsc{ascii} representations available: In theory definitions symbols appear only in mixfix annotations --- using the -\texttt{$\backslash$<$charname$>} form, proof scripts are just left in -plain \texttt{ascii}. +\verb|\<|$charname$\verb|>| form, proof scripts are just left in plain +\textsc{ascii}. -Thus users with \texttt{ascii}-only facilities will still be able to +Thus users with \textsc{ascii}-only facilities will still be able to read your files. diff -r d95d209ae1c2 -r 636322bfd057 doc-src/System/misc.tex --- a/doc-src/System/misc.tex Wed May 21 17:11:24 1997 +0200 +++ b/doc-src/System/misc.tex Wed May 21 17:11:46 1997 +0200 @@ -1,7 +1,7 @@ % $Id$ -\chapter{Miscellaneous tools} +\chapter{Miscellaneous tools} \label{ch:tools} Subsequently we describe various Isabelle related utilities --- in alphabetical order. @@ -124,13 +124,16 @@ ARGS are directly passed to the system make program. \end{ttbox} Note that the Isabelle settings environment is also active. Thus one -may refer to its values within the \ttindex{IsaMakefile}, e.g.\ +may refer to its values within the \ttindex{IsaMakefile}, e.g.\ \texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the -make file also inherit this environment. +make file also inherit this environment. Typically, +\texttt{IsaMakefile}s defer the real work to the \texttt{usedir} +utility, see \S\ref{sec:tool-usedir}. -Typically, \texttt{IsaMakefile}s defer the real work to the -\texttt{usedir} utility, see \S\ref{sec:tool-usedir}. - +\medskip The basic \texttt{IsaMakefile} convention is that the default +target builds the actual logic, including its parents if absent (but +not if just out of date). Furthermore, the \texttt{test} target shall +build the logic \emph{and} run it on all distributed examples. \section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir} @@ -152,7 +155,7 @@ \end{ttbox} The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is -implicitely prefixed to \emph{any} \texttt{usedir} call. Since the +implicitly prefixed to \emph{any} \texttt{usedir} call. Since the \ttindex{IsaMakefile}s of all object-logics distributed with Isabelle just invoke \texttt{usedir} for the real work, one may control compilation options globally via above variable. In particular, @@ -162,19 +165,20 @@ \subsection*{Options} -There are two slightly different modes of operation: \emph{build} mode -(enabled through the \texttt{-b} option) and \emph{example} mode. +Basically, there are two different modes of operation: \emph{build + mode} (enabled through the \texttt{-b} option) and \emph{example + mode}. Calling \texttt{usedir} with \texttt{-b} runs \texttt{isabelle} with -input image \texttt{LOGIC} and output to \texttt{NAME}, as provided as -arguments. This will be a batch session, executing just -\texttt{use_dir".";}\index{*use_dir}, and then quitting. It is assumed +input image \texttt{LOGIC} and output to \texttt{NAME}, as provided on +the command line. This will be a batch session, executing just +\texttt{use_dir".";}\index{*use_dir} and then quitting. It is assumed that there is a file \texttt{ROOT.ML} in the current directory containing all {\ML} commands required to build the logic. In example mode, on the other hand, \texttt{usedir} runs a read-only session of \texttt{LOGIC} (typically just built before) and does an -automatic \texttt{use_dir"NAME";}. I.e.\ it assumes that some file +automatic \texttt{use_dir"NAME";} I.e.\ it assumes that some file \texttt{ROOT.ML} in directory \texttt{NAME} contains appropriate {\ML} commands to run the desired examples. @@ -183,13 +187,13 @@ occurrence of some \texttt{-h} on the command line wins. \medskip Any \texttt{usedir} session is named by some \emph{session - identifier}. These may accumulate, documenting the way sessions -depend on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which -refers the examples of {\ZF} set theory, built upon {\FOL}, built upon + identifier}. These accumulate, documenting the way sessions depend +on others. For example, consider \texttt{Pure/FOL/ZF/ex}, which refers +to the examples of {\ZF} set theory, built upon {\FOL}, built upon {\Pure}. The current session's identifier is by default just the base name of -the \texttt{LOGIC} argument (in build mode), or the \texttt{NAME} +the \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in example mode). This may be overridden explicitely via the \texttt{-s} option. diff -r d95d209ae1c2 -r 636322bfd057 doc-src/System/system.tex --- a/doc-src/System/system.tex Wed May 21 17:11:24 1997 +0200 +++ b/doc-src/System/system.tex Wed May 21 17:11:46 1997 +0200 @@ -14,10 +14,11 @@ \author{{\em Lawrence C. Paulson}\\ Computer Laboratory \\ University of Cambridge \\ \texttt{lcp@cl.cam.ac.uk}\\[3ex] - With Contributions by Tobias Nipkow and Markus Wenzel% - \thanks{Section~\protect\ref{sec:html} was written by Carsten - Clasohm. Chapter~\protect\ref{sec:browse} was written by Stefan - Berghofer. Other parts are by Markus Wenzel.}} + With Contributions by Tobias Nipkow and Markus Wenzel} +%FIXME not yet +% \thanks{Section~\protect\ref{sec:html} was written by Carsten +% Clasohm. Chapter~\protect\ref{sec:browse} was written by Stefan +% Berghofer. Other parts are by Markus Wenzel.} \makeindex