doc-src/System/basics.tex
 changeset 3278 636322bfd057 parent 3262 7115da553895 child 4540 24fcf5ecae88
equal inserted replaced
3277:d95d209ae1c2 3278:636322bfd057
    53 maintainable and user-friendly than ordinary shell environment
    53 maintainable and user-friendly than ordinary shell environment
    54 variables.
    54 variables.
    55
    55
    56 In particular, we avoid the typical situation where prospective users
    56 In particular, we avoid the typical situation where prospective users
    57 of a software package are told to put this and that in their shell
    57 of a software package are told to put this and that in their shell
    58 startup scripts. Isabelle requires none such administrative chores of
    58 startup scripts, before being able to actually run it. Isabelle
    59 its end-users --- the executables can be run straight away. Usually,
    59 requires none such administrative chores of its end-users --- the
    60 users would want to put the Isabelle \texttt{bin} directory into their
    60 executables can be invoked straight away. Usually, users would just
    61 shell's search path, of course.
    61 want to put the Isabelle \texttt{bin} directory into their shell's

    62 search path, of course.
    62
    63
    63
    64
    64 \subsection{Building the environment}
    65 \subsection{Building the environment}
    65
    66
    66 Whenever any of the Isabelle executables is run, their settings
    67 Whenever any of the Isabelle executables is run, their settings
    76   somewhere else just won't work!
    77   somewhere else just won't work!
    77
    78
    78 \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a  79 \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a
    79   shell script with the auto-export option for variables enabled.
    80   shell script with the auto-export option for variables enabled.
    80
    81
    81   This file typically contains a rather long list of assigments
    82   This file typically contains a rather long list of shell variable
    82   \texttt{FOO="bar"}, thus providing the site-wide default settings.
    83   assigments, thus providing the site-wide default settings.  The
    83   The Isabelle distribution already contains a global settings file
    84   Isabelle distribution already contains a global settings file with
    84   with sensible defaults for most variables. When installing the
    85   sensible defaults for most variables. When installing the system,
    85   system, only a few of these have to be adapted (most likely
    86   only a few of these have to be adapted (most likely
    86   \texttt{ML_SYSTEM} etc.).
    87   \texttt{ML_SYSTEM} etc.).
    87
    88
    88 \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it  89 \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it
    89   exists) is run the same way as the site default settings. The
    90   exists) is run the same way as the site default settings. The
    90   variable \texttt{ISABELLE_HOME_USER} has already been set before ---
    91   variable \texttt{ISABELLE_HOME_USER} has already been set before ---
    91   usually to \texttt{\~\relax/isabelle}.
    92   usually to \texttt{\~\relax/isabelle}.
    92
    93
    93   Thus individual users may override the site-wide defaults. See also
    94   Thus individual users may override the site-wide defaults. See also
    94   file \texttt{etc/user-settings.sample} in the distribution.
    95   file \texttt{etc/user-settings.sample} in the distribution.
    95   Typically, user settings are a few lines only, just containing the
    96   Typically, user settings should be a few lines only, just containing
    96   assigments that are really needed.  One should definitely \emph{not}
    97   the assigments that are really needed.  One should definitely
    97   start with a full copy the central
    98   \emph{not} start with a full copy the central
    98   \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very  99 \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very
    99   annoying maintainance problems later, when the Isabelle installation
   100   annoying maintainance problems later, when the Isabelle installation
   100   is updated or changed otherwise.
   101   is updated or changed otherwise.
   101
   102
   102 \end{enumerate}
   103 \end{enumerate}
   169   is appended here, too.
   170   is appended here, too.
   170
   171
   171 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
   172 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
   172   none is given explicitely by the user --- e.g.\ when running
   173   none is given explicitely by the user --- e.g.\ when running
   173   \texttt{isabelle} directly, or some user interface.
   174   \texttt{isabelle} directly, or some user interface.
   174
   175
   175 \item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitely prefixed to the
   176 \item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the
   176   command line of any \texttt{isatool usedir} invocation (see also
   177   command line of any \texttt{isatool usedir} invocation (see also
   177   \S\ref{sec:tool-usedir}). This typically contains compilation
   178   \S\ref{sec:tool-usedir}). This typically contains compilation
   178   options for object-logics --- \texttt{usedir} is the basic utility
   179   options for object-logics --- \texttt{usedir} is the basic utility
   179   that builds them (cf.\ the \texttt{IsaMakefile}s in the
   180   that builds them (cf.\ the \texttt{IsaMakefile}s in the
   180   distribution).
   181   distribution).
   222   file names (then containing at least one /).
   223   file names (then containing at least one /).
   223   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   224   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   224 \end{ttbox}
   225 \end{ttbox}
   225 Input files without path specifications are looked up in the
   226 Input files without path specifications are looked up in the
   226 \texttt{ISABELLE_PATH} setting, which may consist of multiple
   227 \texttt{ISABELLE_PATH} setting, which may consist of multiple
   227 components separated by colons --- these are tried in order.  Short
   228 components separated by colons --- these are tried in order.
   228 output names are relative to the directory specified by
   229 Likewise, short output names are relative to the directory specified
   229 \texttt{ISABELLE_OUTPUT} setting.  In any case, actual file locations
   230 by \texttt{ISABELLE_OUTPUT}.  In any case, actual file locations may
   230 may also be given by including at least one \texttt{/} in the name
   231 also be given by including at least one \texttt{/} in the name (hint:
   231 (hint: use \texttt{./} to refer to the current directory).
   232 use \texttt{./} to refer to the current directory).
   232
   233
   233
   234
   234 \subsection*{Options}
   235 \subsection*{Options}
   235
   236
   236 If the input heap file does not have write permission bits set, or the
   237 If the input heap file does not have write permission bits set, or the
   252 terminated properly by semicolon.
   253 terminated properly by semicolon.
   253
   254
   254 \medskip The \texttt{-m} option adds identifiers of print modes to be
   255 \medskip The \texttt{-m} option adds identifiers of print modes to be
   255 made active for this session. Typically, this is used by some user
   256 made active for this session. Typically, this is used by some user
   256 interface, for example to enable output of mathematical symbols from a
   257 interface, for example to enable output of mathematical symbols from a
   257 special screen font. See also \S\ref{sec:tool-installfonts} about
   258 special screen font.
   258 fonts and the \emph{Isabelle Reference Manual} about print modes in

   259 general.

   260
   259
   261 \medskip Isabelle normally enters an interactice {\ML} top-level loop
   260 \medskip Isabelle normally enters an interactice {\ML} top-level loop
   262 (after processing the \texttt{-e} texts). The \texttt{-q} option
   261 (after processing the \texttt{-e} texts). The \texttt{-q} option
   263 inhibits this, thus providing a pure batch mode facility.
   262 inhibits this, thus providing a pure batch mode facility.
   264
   263
   290 A read-only \texttt{Foo} session may be started by:
   289 A read-only \texttt{Foo} session may be started by:
   291 \begin{ttbox}
   290 \begin{ttbox}
   292 isabelle -r Foo
   291 isabelle -r Foo
   293 \end{ttbox}
   292 \end{ttbox}
   294 One may also use something like \texttt{chmod~-w} on the logic image
   293 One may also use something like \texttt{chmod~-w} on the logic image
   295 to have them read-only automatically.
   294 to have it read-only automatically.
   296
   295
   297 \medskip The next example demonstrates batch execution of Isabelle. We
   296 \medskip The next example demonstrates batch execution of Isabelle. We
   298 print a certain theorem of \texttt{FOL}:
   297 print a certain theorem of \texttt{FOL}:
   299 \begin{ttbox}
   298 \begin{ttbox}
   300 isabelle -e "prth allE;" -q -r FOL
   299 isabelle -e "prth allE;" -q -r FOL
   303 garbage produced by the {\ML} compiler.
   302 garbage produced by the {\ML} compiler.
   304
   303
   305
   304
   306 \section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
   305 \section{The Isabelle tools wrapper --- \texttt{isatool}} \label{sec:isatool}
   307
   306
   308 FIXME
   307 All Isabelle related utilities are called via a common wrapper ---

   308 \ttindex{isatool}:

   309 \begin{ttbox}

   310 Usage: isatool TOOL [ARGS ...]

   311

   312   Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL

   313   for more specific help.

   314

   315   Available tools are:

   316

   317     doc - view Isabelle documentation

   318     $$\vdots$$

   319 \end{ttbox}

   320 Basically, Isabelle tools are ordinary executable scripts.  These are

   321 run within the same settings environment as Isabelle proper, though,

   322 see \S\ref{sec:settings}.  The set of available tools is collected by

   323 isatool from the directories listed in the \texttt{ISABELLE_TOOLS}

   324 setting.  Do not try to call the scripts directly. Neither should you

   325 add the tools directories to your shell's search path.

   326

   327

   328 \medskip See chapter~\ref{ch:tools} for descriptions of most utilities

   329 that come with the Isabelle distributions. Third-parties may add their

   330 own, of course.

   331
   309
   332
   310 \section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface}
   333 \section{The Isabelle interface wrapper --- \texttt{Isabelle}} \label{sec:interface}
   311
   334
   312 FIXME
   335 Isabelle is a generic theorem prover, even w.r.t.\ its user interface.

   336 The \ttindex{Isabelle} command (note the capital \texttt{I}) provides

   337 a uniform way for end-users to invoke a certain interface. Which one

   338 to actually start is determined by the \settdx{ISABELLE_INTERFACE}

   339 setting variable. Currently, the following are recognized:

   340 \begin{ttdescription}

   341 \item[none] is just a pass-through to \texttt{isabelle}. Thus

   342   \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.

   343

   344 \item[xterm] refers to a simple xterm-based interface which is part of

   345   the Isabelle distribution.

   346

   347 \item[emacs] refers to David Aspinall's \emph{Isamode} for emacs.

   348   Isabelle just provides a wrapper for this, the actual Isamode

   349   distribution is available elsewhere.

   350 \end{ttdescription}

   351

   352 The factory default for \texttt{ISABELLE_INTERFACE} is \texttt{xterm}.

   353 This interface runs \texttt{isabelle} within its own xterm window.

   354 Usually, display of mathematical symbols from the Isabelle font is

   355 also enabled (see \S\ref{sec:tool-installfonts} for font configuration

   356 issues).  Furthermore, different kinds of identifiers in logical terms

   357 are highlighted appropriately, e.g.\ free variables in bold and bound

   358 variables underlined.

   359

   360 There are some more options available.  Just pass \texttt{-?} to the

   361 \texttt{xterm} interface to have its usage printed.