doc-src/System/basics.tex
 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:
+\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}.
+
+  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
+  \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.
+
+for this session. Typically this is used by some user interface to
+enable output of mathematical symbols from a special screen font, for
+  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
+
+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.
+