# HG changeset patch # User wenzelm # Date 864149664 -7200 # Node ID 7115da5538955c24abe0188b3f54207e4b3ccb97 # Parent 8fe63a9cd0c7f3f2faa4500c6e652d83740eef7e under construction; diff -r 8fe63a9cd0c7 -r 7115da553895 doc-src/System/basics.tex --- a/doc-src/System/basics.tex Tue May 20 19:33:53 1997 +0200 +++ b/doc-src/System/basics.tex Tue May 20 19:34:24 1997 +0200 @@ -3,11 +3,10 @@ \chapter{Basic concepts} -The \emph{Isabelle System Manual} describes Isabelle together with its -related tools and user interfaces --- as seen from an outside -(operating system oriented) view. See the \emph{Isabelle Reference - Manual} for all internal {\ML} level user commands, on the other -hand. +The \emph{Isabelle System Manual} describes Isabelle together with +related tools and user interfaces as seen from an outside (operating +system oriented) view. See the \emph{Isabelle Reference Manual} for +all internal {\ML} level user commands, on the other hand. \medskip The Isabelle system level environment is based on a few general concepts: @@ -31,10 +30,10 @@ \medskip The beginning user would probably just run one of the interfaces (by invoking the capital \texttt{Isabelle}), and maybe some -basic other tools like \texttt{doc} (see \S\ref{sec:tool-doc}). This +basic tools like \texttt{doc} (see \S\ref{sec:tool-doc}). This assumes that the system has already been installed properly, of -course.\footnote{In case you have to do this yourself from scratch, - see the \ttindex{INSTALL} file in the top-level directory of the +course.\footnote{In case you have to do this yourself, see the + \ttindex{INSTALL} file in the top-level directory of the distribution. The information provided there should be sufficient as a start.} @@ -50,7 +49,7 @@ Isabelle employs a somewhat more sophisticated scheme of \emph{settings files} --- one for site-wide defaults, another for optional user-specific modifications. With all configuration -variables in only one or two places, this is considered much more +variables in just a few places, this is considered much more maintainable and user-friendly than ordinary shell environment variables. @@ -64,7 +63,7 @@ \subsection{Building the environment} -Whenever any of the Isabelle executables is run, theri settings +Whenever any of the Isabelle executables is run, their settings environment is built as follows: \begin{enumerate} @@ -94,11 +93,11 @@ 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 required. One should definitely - \emph{not} start with a full copy the central - \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very anoying - maintainance problems later, when the Isabelle installation is - updated or changed otherwise. + 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. \end{enumerate} @@ -166,8 +165,8 @@ automatically. \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap - files should be stored. The \texttt{ML_SYSTEM} identifier is - appended here, too. + files should be stored by default. The \texttt{ML_SYSTEM} identifier + is appended here, too. \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is given explicitely by the user --- e.g.\ when running @@ -186,14 +185,14 @@ \item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories with documentation files. - -\item[\settdx{DVI_VIEWER}] specifies the program to be used for + +\item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying \texttt{dvi} files. \item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the - Isabelle symbol fonts are installed into your running X11 display - server. X11 fonts are a non-trivial issue, see \S\ref{sec:fonts} for - more information. + Isabelle symbol fonts are installed into your currently running X11 + display server. X11 fonts are a non-trivial issue, see + \S\ref{sec:tool-installfonts} for more information. \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the actual user interface that the capital \texttt{Isabelle} should @@ -228,8 +227,8 @@ 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 -could also be given by including at least one \texttt{/} in the name -(use \texttt{./} to refer to the current directory). +may also be given by including at least one \texttt{/} in the name +(hint: use \texttt{./} to refer to the current directory). \subsection*{Options} @@ -248,16 +247,16 @@ \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to the Isabelle session from the command line. Multiple -\texttt{-e}'s are evaluated in the given order. Strange things may -happen when errorneous {\ML} code is supplied. Also make sure that -commands are terminated properly by semicolon. +\texttt{-e}'s are evaluated in order. Strange things may happen when +errorneous {\ML} code is given. Also make sure that commands are +terminated properly by semicolon. -\medskip The \texttt{-m} option adds identifiers of print modes that -are 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. +\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. \medskip Isabelle normally enters an interactice {\ML} top-level loop (after processing the \texttt{-e} texts). The \texttt{-q} option @@ -284,7 +283,7 @@ megabytes! The \texttt{Foo} session may be continued later (still in writable -state) at exactly the same point: +state) by: \begin{ttbox} isabelle Foo \end{ttbox} diff -r 8fe63a9cd0c7 -r 7115da553895 doc-src/System/fonts.tex --- a/doc-src/System/fonts.tex Tue May 20 19:33:53 1997 +0200 +++ b/doc-src/System/fonts.tex Tue May 20 19:34:24 1997 +0200 @@ -1,20 +1,21 @@ \chapter{Fonts and character encodings} -With the advent of print modes in Isabelle (see also The -\emph{Isabelle Reference Manual}, 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 output -(and input) of nice mathematical symbols out of the box. +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. 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 by default. +\S\ref{sec:isa-xterm}) usually do this already by default. -\medskip Of course, this requires special screen fonts (see -\S\ref{sec:tool-installfonts}). Furthermore, various {\ML} systems -cause some problems with non-\textsc{ascii} characters in literal -strings. These are avoided by the \texttt{symbolinput} filter (see +\medskip Displaying non-standard characters requires special screen +fonts, of course. The \texttt{installfonts} utility takes care of +this, see \S\ref{sec:tool-installfonts}. Furthermore, some {\ML} +systems disallow non-\textsc{ascii} characters in literal strings. +This problem is avoided by the \texttt{symbolinput} filter (see \S\ref{sec:tool-symbolinput}). Both of these are invoked transparently in normal operation. So one @@ -22,7 +23,7 @@ something fails to work. -\section{Telling X11 about Isabelle fonts --- \texttt{isatool installfonts}} +\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}} \label{sec:tool-installfonts} The \tooldx{installfonts} utility ensures that your currently running @@ -35,19 +36,19 @@ (May be safely called repeatedly.) \end{ttbox} Note that this need not be called manually under normal circumstances ---- user interfaces depending on the Isabelle fonts will invoke -\texttt{installfonts} transparently. +--- user interfaces depending on the Isabelle fonts usually invoke +\texttt{installfonts} automatically. \medskip As simple as this might appear to be, it is not! X11 fonts are a surprisingly complicated matter. Depending on your network structure, fonts might have to be installed differently. This has to -be specified via the \settdx{ISABELLE_INSTALLFONTS}. +be specified via the \settdx{ISABELLE_INSTALLFONTS} variable in your +local settings. \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. Then most X11 display servers should be happy to being -just told about the directory where the fonts reside within the -Isabelle distribution: +same machine. In this case, most X11 display servers should be happy +by being about the directory where the fonts reside as follows: \begin{ttbox} ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash" \end{ttbox} @@ -55,33 +56,64 @@ network, where the X11 display machine mounts the Isabelle distribution under the same name as the client side. -\medskip Above method fails, if the display machine does have the font -files at the same location as the client. In case your server is a -full workstation with its own file system, you could in principle just -copy the fonts there and do an appropriate \texttt{xset~fp+} manually -before running the Isabelle interface. This is awkward, of course, but -is even \emph{impossible} for proper X terminals that do not have -their own file system. +\medskip Above method fails, though, if the display machine does have +the font files at the same location as the client. In case your server +is a full workstation with its own file system, you could in principle +just copy the fonts there and do an appropriate \texttt{xset~fp+} +manually before running the Isabelle interface. This is very awkward, +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 use an \emph{X11 font - server}, offering the Isabelle font to the Net. In principle it is -relatively easy to setup one your own --- the program is called -\texttt{xfs} (or just \texttt{fs)}, see the \texttt{man} pages of your -system. - -Your are very lucky, though, if you have a sensible connection to the -Internet. We already offer a world-wide X11 font service for the -Isabelle fonts. To have \texttt{installfonts} make use of this, just -set \texttt{ISABELLE_INSTALLFONTS} is follows: +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: \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 +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. + \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$>}. + +The \tooldx{symbolinput} utility converts a input stream encoded +according to the standard Isabelle font layout into pure +\textsc{ascii} text. There is no usage --- \texttt{symbolinput} just +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 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 +symbols appear only in mixfix annotations --- using the +\texttt{$\backslash$<$charname$>} form, proof scripts are just left in +plain \texttt{ascii}. + +Thus users with \texttt{ascii}-only facilities will still be able to +read your files. + %FIXME not yet %\section{ --- \texttt{isatool showsymbols}} diff -r 8fe63a9cd0c7 -r 7115da553895 doc-src/System/misc.tex --- a/doc-src/System/misc.tex Tue May 20 19:33:53 1997 +0200 +++ b/doc-src/System/misc.tex Tue May 20 19:34:24 1997 +0200 @@ -31,7 +31,7 @@ The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance readability a bit: \begin{ttbox} -Usage: expandshort [FILES ...] +Usage: isatool expandshort [FILES ...] Expand shorthand goal commands in FILES. Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on @@ -58,7 +58,7 @@ \end{ttbox} The base names of all files found on the path are printed --- sorted and with duplicates removed. Also note that \texttt{ISABELLE_PATH} -implicitely depends upon \texttt{ML_SYSTEM}. Thus switching to another +implicitly depends upon \texttt{ML_SYSTEM}. Thus switching to another {\ML} compiler may change the set of logic images available. @@ -124,18 +124,19 @@ 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 \texttt{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. -\medskip You may want to have a look at the \texttt{IsaMakefile}s of -the distributed object-logics as examples for your own developements. +Typically, \texttt{IsaMakefile}s defer the real work to the +\texttt{usedir} utility, see \S\ref{sec:tool-usedir}. + \section{Running complete logics --- \texttt{isatool usedir}} \label{sec:tool-usedir} -FIXME - +The \tooldx{usedir} utility builds object-logic images, or runs +example sessions based on existing logics. Its usage is: %FIXME % -g BOOL generate theory graph data (default false) \begin{ttbox} @@ -150,4 +151,50 @@ information (HTML etc.) according to settings. \end{ttbox} -FIXME +The value of the \settdx{ISABELLE_USEDIR_OPTIONS} setting is +implicitely 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, +generation of \rmindex{HTML} browsing information is enabled or +disabled this way. + + +\subsection*{Options} + +There are two slightly 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 +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 +\texttt{ROOT.ML} in directory \texttt{NAME} contains appropriate {\ML} +commands to run the desired examples. + +\medskip The \texttt{-h} option controls HTML browsing data +generation. It may be explicitely turned on or off --- the last +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 +{\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} +argument (in example mode). This may be overridden explicitely via the +\texttt{-s} option. + + +\subsection*{Examples} + +Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's +object-logics as a model for your own developements. diff -r 8fe63a9cd0c7 -r 7115da553895 doc-src/System/system.tex --- a/doc-src/System/system.tex Tue May 20 19:33:53 1997 +0200 +++ b/doc-src/System/system.tex Tue May 20 19:34:24 1997 +0200 @@ -16,7 +16,7 @@ \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{browse} was written by Stefan + Clasohm. Chapter~\protect\ref{sec:browse} was written by Stefan Berghofer. Other parts are by Markus Wenzel.}} \makeindex