doc-src/System/basics.tex
changeset 3278 636322bfd057
parent 3262 7115da553895
child 4540 24fcf5ecae88
equal deleted 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.