--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/System/basics.tex Wed May 14 19:27:21 1997 +0200
@@ -0,0 +1,229 @@
+
+% $Id$
+
+\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. On the other hand, see
+\emph{Isabelle Reference} for all internal {\ML} level user commands.
+
+\medskip The Isabelle system level environment is based on a few
+generic concepts that are simple, but non-trivial:
+\begin{itemize}
+\item The \emph{Isabelle settings mechanism}, which provides
+ environment values 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.
+ 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).
+\end{itemize}
+
+\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
+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
+ distribution. The information provided there should be sufficient as
+ a start.}
+
+
+\section{Isabelle settings} \label{sec:settings}
+
+The Isabelle system heavily depends on the \emph{settings
+ mechanism}\indexbold{settings}. Basically, this is just a collection
+of environment variables, e.g.\ \texttt{ISABELLE_HOME},
+\texttt{ML_SYSTEM}, \texttt{ML_HOME}. These variables are \emph{not}
+intended to be set directly from the shell!
+
+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
+maintainable and user-friendly than ordinary shell environment
+variables.
+
+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.
+
+
+\subsection{Building the environment}
+
+The environment that all Isabelle programs are run in 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}).
+
+ 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.
+
+ 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).
+
+\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it
+ exists) is run the same way as the site default settings. The
+ variable \texttt{ISABELLE_HOME_USER} has already been set before ---
+ usually to \texttt{\~\relax/isabelle}.
+
+ 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 may cause severe
+ 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.
+
+\medskip A few variables are somewhat:
+\begin{itemize}
+\item \ttindex{ISABELLE} and \ttindex{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
+ 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
+\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.
+
+\begin{ttdescription}
+\item[FIXME] FIXME
+\end{ttdescription}
+
+
+\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:
+\begin{ttbox}
+Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
+
+ Options are:
+ -e MLTEXT pass MLTEXT to the ML session
+ -m MODE add print mode for output
+ -q non-interactive session
+ -r open heap file read-only
+
+ INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
+ These are either names to be searched in the Isabelle path, or actual
+ file names (then containing at least one /).
+ If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
+\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
+\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.
+
+
+\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.
+
+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).
+
+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.
+
+
+\subsection*{Examples}
+
+Run an interactive session of the default object-logic:
+\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):
+\begin{ttbox}
+isabelle FOL Foo
+\end{ttbox}
+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:
+\begin{ttbox}
+isabelle Foo
+\end{ttbox}
+
+\medskip This is a simple batch mode example, printing 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
+garbage produced by the {\ML} compiler.
+