changeset 3188 445555a7b714
child 3217 d30d62128fe5
--- /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:
+\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).
+\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
+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
+\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.
+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:
+\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.
+\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
+\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.
+\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:
+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.
+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
+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.
+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
+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.
+Run an interactive session of the default object-logic:
+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):
+isabelle FOL Foo
+Ending this session normally (e.g.\ by typing control-D), dumps the
+whole {\ML} system state into \texttt{Foo}. Be prepared for several
+The \texttt{Foo} session may be continued (writably!) at exactly the
+same point as follows:
+isabelle Foo
+\medskip This is a simple batch mode example, printing a certain
+theorem of \texttt{FOL}:
+isabelle -e "prth allE;" -q -r FOL
+Note that the output text will be usually interspered with some
+garbage produced by the {\ML} compiler.