doc-src/System/basics.tex
changeset 3217 d30d62128fe5
parent 3188 445555a7b714
child 3262 7115da553895
--- a/doc-src/System/basics.tex	Fri May 16 15:55:02 1997 +0200
+++ b/doc-src/System/basics.tex	Fri May 16 15:57:11 1997 +0200
@@ -5,28 +5,28 @@
 
 The \emph{Isabelle System Manual} describes Isabelle together with its
 related tools and user interfaces --- as seen from an outside
-(operating system oriented) view.  On the other hand, see
-\emph{Isabelle Reference} for all internal {\ML} level user commands.
+(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
-generic concepts that are simple, but non-trivial:
+general concepts:
 \begin{itemize}
 \item The \emph{Isabelle settings mechanism}, which provides
-  environment values to all Isabelle programs (including tools and
+  environment variables to all Isabelle programs (including tools and
   user interfaces).
 \item \emph{Isabelle proper} (\ttindex{isabelle}), which runs logic
   sessions, both interactively or in batch mode. In particular,
   \texttt{isabelle} abstracts over the invocation of the actual {\ML}
   system to be used.
 \item The \emph{Isabelle tools wrapper} (\ttindex{isatool}), which
-  provides a generic startup platform for miscellaneous utilities.
+  provides a generic startup platform for Isabelle related utilities.
   Thus tools automatically benefit from the settings mechanism.
   Furthermore, the shell's search path is kept clean from many small
   programs.
 \item The \emph{Isabelle interface wrapper}
   (\ttindex{Isabelle}\footnote{Note the capital \texttt{I}!}), which
-  provides some abstraction over the actual user interface to be used
-  (this may include third-party ones).
+  provides some abstraction over the actual user interface to be used.
 \end{itemize}
 
 \medskip The beginning user would probably just run one of the
@@ -64,27 +64,27 @@
 
 \subsection{Building the environment}
 
-The environment that all Isabelle programs are run in is built as
-follows:
+Whenever any of the Isabelle executables is run, theri settings
+environment is built as follows:
 
 \begin{enumerate}
-\item The special variable \ttindex{ISABELLE_HOME} is determined
-  automatically from the location of the binary that has been run
-  (e.g.\ \texttt{isabelle}).
+\item The special variable \settdx{ISABELLE_HOME} is determined
+  automatically from the location of the binary that has been run.
   
   You should not try to set \texttt{ISABELLE_HOME} manually. Also note
   that the Isabelle executables have to be run from their original
   location in the distribution directory --- copying or linking them
   somewhere else just won't work!
   
-\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a GNU
-  bash script with the variable auto-export option enabled.
+\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a
+  shell script with the auto-export option for variables enabled.
   
-  The file typically contains a rather long list of assigments
-  \texttt{FOO="bar"}, thus providing the site default settings. The
-  Isabelle distribution already contains a global settings file with
-  sensible defaults. When installing the system, only a few of these
-  have to be adapted (most likely \texttt{ML_SYSTEM} and friends).
+  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
+  \texttt{ML_SYSTEM} etc.).
   
 \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it
   exists) is run the same way as the site default settings. The
@@ -96,52 +96,119 @@
   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 may cause severe
+  \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very anoying
   maintainance problems later, when the Isabelle installation is
   updated or changed otherwise.
 
 \end{enumerate}
 
-Note that settings files are actually bash scripts. So one may use
-complex shell commands, e.g.\ \texttt{if} or \texttt{case} statements
-to set variables depending on the system architecture or other
-environment variables. Such advanced features should be added only
-with great care, though. In particular, external environment
-references should be kept at a minimum.
+Note that settings files are actually full GNU bash scripts. So one
+may use complex shell commands, say \texttt{if} or \texttt{case}
+statements to set variables depending on the system architecture or
+other environment variables, for example. Such advanced features
+should be added only with great care, though. In particular, external
+environment references should be kept at a minimum.
 
-\medskip A few variables are somewhat:
+\medskip A few variables are somewhat special:
 \begin{itemize}
-\item \ttindex{ISABELLE} and \ttindex{ISATOOL} are set automatically
-  to the absolute path names of the \texttt{isabelle} and
+\item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to
+  the absolute path names of the \texttt{isabelle} and
   \texttt{isatool} executables, respectively.
   
-\item \ttindex{ISABELLE_PATH} and \ttindex{ISABELLE_OUTPUT} will have
+\item \settdx{ISABELLE_PATH} and \settdx{ISABELLE_OUTPUT} will have
   the {\ML} system identifier (as specified by \texttt{ML_SYSTEM})
   automatically appended to their values.
 \end{itemize}
 
 \medskip The Isabelle settings scheme is basically quite simple, but
 non-trivial.  For debugging purposes, the generated environment may be
-inspected with the \texttt{getenv} Isabelle tool, see
+inspected with the \texttt{getenv} utility, see
 \S\ref{sec:tool-getenv}.
 
 
 \subsection{Common variables}
 
-Below is a reference of common Isabelle settings variables. The list
-is somewhat open-ended, in particular, third-party utilities or
-interfaces may add their own selection.
+Below is a reference of common Isabelle settings variables. Note that
+the list is somewhat open-ended. Third-party utilities or interfaces
+may add their own selection. Variables that are special in some sense
+are marked with *.
+
+\begin{description}
+\item[\settdx{ISABELLE_HOME}*] is the location of the top-level
+  Isabelle distribution directory. This is automatically determined
+  from the Isabelle executable that has been invoked.  Do not try to
+  set \texttt{ISABELLE_HOME} yourself from the shell.
+  
+\item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of
+  \texttt{ISABELLE_HOME}. The default value is
+  \texttt{\~\relax/isabelle}, under rare circumstances this may be
+  changed in the global setting file.  Typically, the
+  \texttt{ISABELLE_HOME_USER} directory mimics \texttt{ISABELLE_HOME}
+  to some extend. In particular, site-wide defaults may be overridden
+  by a private \texttt{etc/settings}.
+  
+\item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to
+  the full paths of the \texttt{isabelle} and \texttt{isatool}
+  executables, respectively.  Thus other tools and scripts need not
+  assume that the Isabelle \texttt{bin} directory is on the current
+  search path of the shell.
 
-\begin{ttdescription}
-\item[FIXME] FIXME
-\end{ttdescription}
+\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS}]
+  specify the underlying {\ML} system to be used for Isabelle.  The
+  choice of \texttt{ML_SYSTEM} identifiers is quite fixed, see the
+  global \texttt{etc/settings} file for some examples. The actual
+  compiler binary will be run from directory \texttt{ML_HOME}, with
+  \texttt{ML_OPTIONS} as first arguments on the command line.
+  
+\item[\settdx{ISABELLE_PATH}*] is a list of directories (separated by
+  colons) where Isabelle logic images may reside. Note that the
+  \texttt{ML_SYSTEM} identifier is appended to each component
+  automatically.
+  
+\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
+  files should be stored. 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
+  \texttt{isabelle} directly, or some user interface.
+
+\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitely 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
+  that builds them (cf.\ the \texttt{IsaMakefile}s in the
+  distribution).
+
+\item[\settdx{ISABELLE_TOOLS}] is a colon separated list of
+  directories that are scanned by \texttt{isatool} for utility
+  programs (see also \S\ref{sec:isatool}).
+
+\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
+  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.
+  
+\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
+  actual user interface that the capital \texttt{Isabelle} should
+  invoke.  Currently available are \texttt{none}, \texttt{xterm} and
+  \texttt{emacs}. See \S\ref{sec:interface} for more details.
+
+\end{description}
 
 
 \section{Isabelle proper --- \texttt{isabelle}}
 
 The \ttindex{isabelle} executable runs logic sessions --- either
 interactively or in batch mode. It provides an abstraction over the
-underlying {\ML} system, and over the actual heap file locations. The usage is:
+underlying {\ML} system, and over the actual heap file locations. Its
+usage is:
 \begin{ttbox}
 Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
 
@@ -158,72 +225,89 @@
 \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 the given order.
-Short output names are relative to the directory specified by
+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
-can be given by including at least one \texttt{/} (use \texttt{./} to
-refer to the current directory).
-
-If the input heap file is not writable, or the \texttt{-r} option is
-given explicitely, the session will be read-only. That is, the {\ML}
-world cannot be committed back into the logic image.  A writable
-session enables commits into either the input file, or into an
-alternative output heap file which may be given as the second
-argument.
-
-The read-write state of sessions is determined at startup only, it
-cannot be changed intermediately. Also note that heap images may
-require considerable amounts of disk space. Users are responsible
-themselves to dispose no longer needed heap files.
+could also be given by including at least one \texttt{/} in the name
+(use \texttt{./} to refer to the current directory).
 
 
 \subsection*{Options}
 
-Using \texttt{-e} one may pass {\ML} code to the Isabelle session from
-the command line. Multiple \texttt{-e}'s are evaluated in the given
-order.
+If the input heap file does not have write permission bits set, or the
+\texttt{-r} option is given explicitely, then the session will be
+read-only. That is, the {\ML} world cannot be committed back into the
+logic image.  Otherwise, a writable session enables commits into
+either the input file, or into an alternative output heap file (in
+case this is given as the second argument).
+
+The read-write state of sessions is determined at startup only, it
+cannot be changed intermediately. Also note that heap images may
+require considerable amounts of disk space. Users are responsible
+themselves to dispose their heap files when they are no longer needed.
 
-The \texttt{-m} option addes print mode identifiers to be made active
-for this session. Typically this is used by some user interface to
-enable output of mathematical symbols from a special screen font, for
-example (see also \S\ref{sec:fonts} about fonts and the \emph{Isabelle
-  Reference Manual} about print modes in general).
+\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.
 
-Isabelle normally enters an interactice {\ML} top-level loop (after
-processing the \texttt{-e} texts). The \texttt{-q} option inhibits
-this, providing a pure batch mode facility.
+\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 Isabelle normally enters an interactice {\ML} top-level loop
+(after processing the \texttt{-e} texts). The \texttt{-q} option
+inhibits this, thus providing a pure batch mode facility.
 
 
 \subsection*{Examples}
 
-Run an interactive session of the default object-logic:
+Run an interactive session of the default object-logic (as specified
+by the \texttt{ISABELLE_LOGIC} setting) like this:
 \begin{ttbox}
 isabelle
 \end{ttbox}
-Usually, this refers to one of the standard logic images, which are
-read-only by default.
-
-Run a writable session, based on \texttt{FOL}, but output to
-\texttt{Foo} (in the directory specified by the
-\texttt{ISABELLE_OUTPUT} setting):
+Usually \texttt{ISABELLE_LOGIC} refers to one of the standard logic
+images, which are read-only by default.  A writable session --- based
+on \texttt{FOL}, but output to \texttt{Foo} (in the directory
+specified by the \texttt{ISABELLE_OUTPUT} setting) --- may be invoked
+as follows:
 \begin{ttbox}
 isabelle FOL Foo
 \end{ttbox}
-Ending this session normally (e.g.\ by typing control-D), dumps the
+Ending this session normally (e.g.\ by typing control-D) dumps the
 whole {\ML} system state into \texttt{Foo}. Be prepared for several
 megabytes!
 
-The \texttt{Foo} session may be continued (writably!) at exactly the
-same point as follows:
+The \texttt{Foo} session may be continued later (still in writable
+state) at exactly the same point:
 \begin{ttbox}
 isabelle Foo
 \end{ttbox}
+A read-only \texttt{Foo} session may be started by:
+\begin{ttbox}
+isabelle -r Foo
+\end{ttbox}
+One may also use something like \texttt{chmod~-w} on the logic image
+to have them read-only automatically.
 
-\medskip This is a simple batch mode example, printing a certain
-theorem of \texttt{FOL}:
+\medskip The next example demonstrates batch execution of Isabelle. We
+print a certain theorem of \texttt{FOL}:
 \begin{ttbox}
 isabelle -e "prth allE;" -q -r FOL
 \end{ttbox}
-Note that the output text will be usually interspered with some
+Note that the output text will be usually interspersed with some
 garbage produced by the {\ML} compiler.
 
+
+\section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
+
+FIXME
+
+\section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface}
+
+FIXME