doc-src/System/basics.tex

renamed addss to addSss, unsafe_addss to addss, extended auto_tac

% $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.