doc-src/System/basics.tex
author wenzelm
Sat May 17 13:54:30 2008 +0200 (2008-05-17)
changeset 26928 ca87aff1ad2d
parent 25628 94bb4a85d35d
permissions -rw-r--r--
structure Display: less pervasive operations;
     1 
     2 % $Id$
     3 
     4 \chapter{The Isabelle system environment}
     5 
     6 This manual describes Isabelle together with related tools and user interfaces
     7 as seen from an outside (system oriented) view.  See also the
     8 \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} and the
     9 \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the actual Isabelle
    10 commands and related functions.
    11 
    12 \medskip The Isabelle system environment emerges from a few general concepts.
    13 \begin{itemize}
    14 \item The \emph{Isabelle settings mechanism} provides environment variables to
    15   all Isabelle programs (including tools and user interfaces).
    16 \item The \emph{Isabelle tools wrapper} (\ttindex{isatool}) provides a generic
    17   startup platform for Isabelle related utilities.  Thus tools automatically
    18   benefit from the settings mechanism.
    19 \item The raw \emph{Isabelle process} (\ttindex{isabelle} or
    20   \texttt{isabelle-process}) runs logic sessions either interactively or in
    21   batch mode.  In particular, this view abstracts over the invocation of the
    22   actual {\ML} system to be used.
    23 \item The \emph{Isabelle interface wrapper} (\ttindex{Isabelle} or
    24   \texttt{isabelle-interface}) provides some abstraction over the actual user
    25   interface to be used.  The de-facto standard interface for Isabelle is
    26   Proof~General \cite{proofgeneral}.
    27 \end{itemize}
    28 
    29 \medskip The beginning user would probably just run the default user interface
    30 (by invoking the capital \texttt{Isabelle}).  This assumes that the system has
    31 already been installed, of course.  In case you have to do this yourself, see
    32 the \ttindex{INSTALL} file in the top-level directory of the distribution of
    33 how to proceed; binary packages for various system components are available as
    34 well.
    35 
    36 
    37 \section{Isabelle settings} \label{sec:settings}
    38 
    39 The Isabelle system heavily depends on the \emph{settings
    40   mechanism}\indexbold{settings}.  Essentially, this is a statically scoped
    41 collection of environment variables, such as \texttt{ISABELLE_HOME},
    42 \texttt{ML_SYSTEM}, \texttt{ML_HOME}.  These variables are \emph{not} intended
    43 to be set directly from the shell, though.  Isabelle employs a somewhat more
    44 sophisticated scheme of \emph{settings files} --- one for site-wide defaults,
    45 another for additional user-specific modifications.  With all configuration
    46 variables in at most two places, this scheme is more maintainable and
    47 user-friendly than global shell environment variables.
    48 
    49 In particular, we avoid the typical situation where prospective users of a
    50 software package are told to put several things into their shell startup
    51 scripts, before being able to actually run the program. Isabelle requires none
    52 such administrative chores of its end-users --- the executables can be invoked
    53 straight away.\footnote{Occasionally, users would still want to put the
    54   Isabelle \texttt{bin} directory into their shell's search path, but this is
    55   not required.}
    56 
    57 
    58 \subsection{Building the environment}
    59 
    60 Whenever any of the Isabelle executables is run, their settings environment is
    61 put together as follows.
    62 
    63 \begin{enumerate}
    64 \item The special variable \settdx{ISABELLE_HOME} is determined automatically
    65   from the location of the binary that has been run.
    66   
    67   You should not try to set \texttt{ISABELLE_HOME} manually. Also note that
    68   the Isabelle executables either have to be run from their original location
    69   in the distribution directory, or via the executable objects created by the
    70   \texttt{install} utility (see \S\ref{sec:tool-install}).  Just doing a plain
    71   copy of the \texttt{bin} files will not work!
    72   
    73 \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
    74   with the auto-export option for variables enabled.
    75   
    76   This file holds a rather long list of shell variable assigments, thus
    77   providing the site-wide default settings.  The Isabelle distribution already
    78   contains a global settings file with sensible defaults for most variables.
    79   When installing the system, only a few of these may have to be adapted
    80   (probably \texttt{ML_SYSTEM} etc.).
    81   
    82 \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
    83   run in the same way as the site default settings. Note that the variable
    84   \texttt{ISABELLE_HOME_USER} has already been set before --- usually to
    85   \texttt{\~\relax/isabelle}.
    86   
    87   Thus individual users may override the site-wide defaults. See also file
    88   \texttt{etc/user-settings.sample} in the distribution.  Typically, a user
    89   settings file would contain only a few lines, just the assigments that are
    90   really changed.  One should definitely \emph{not} start with a full copy the
    91   basic \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very annoying
    92   maintainance problems later, when the Isabelle installation is updated or
    93   changed otherwise.
    94 
    95 \end{enumerate}
    96 
    97 Note that settings files are actually full GNU bash scripts. So one may use
    98 complex shell commands, such as \texttt{if} or \texttt{case} statements to set
    99 variables depending on the system architecture or other environment variables.
   100 Such advanced features should be added only with great care, though. In
   101 particular, external environment references should be kept at a minimum.
   102 
   103 \medskip A few variables are somewhat special:
   104 \begin{itemize}
   105 \item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to the
   106   absolute path names of the \texttt{isabelle-process} and \texttt{isatool}
   107   executables, respectively.
   108   
   109 \item \settdx{ISABELLE_OUTPUT} will have the identifiers of the
   110   Isabelle distribution (cf.\ \texttt{ISABELLE_IDENTIFIER}) and the
   111   {\ML} system (cf.\ \texttt{ML_IDENTIFIER}) appended automatically to
   112   its value.
   113 \end{itemize}
   114 
   115 \medskip The Isabelle settings scheme is conceptually simple, but not
   116 completely trivial.  For debugging purposes, the resulting environment may be
   117 inspected with the \texttt{getenv} utility, see \S\ref{sec:tool-getenv}.
   118 
   119 
   120 \subsection{Common variables}
   121 
   122 This is a reference of common Isabelle settings variables. Note that the list
   123 is somewhat open-ended. Third-party utilities or interfaces may add their own
   124 selection. Variables that are special in some sense are marked with *.
   125 
   126 \begin{description}
   127 \item[\settdx{ISABELLE_HOME}*] is the location of the top-level Isabelle
   128   distribution directory. This is automatically determined from the Isabelle
   129   executable that has been invoked.  Do not attempt to set
   130   \texttt{ISABELLE_HOME} yourself from the shell.
   131   
   132 \item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of
   133   \texttt{ISABELLE_HOME}. The default value is \texttt{\~\relax/isabelle},
   134   under rare circumstances this may be changed in the global setting file.
   135   Typically, the \texttt{ISABELLE_HOME_USER} directory mimics
   136   \texttt{ISABELLE_HOME} to some extend. In particular, site-wide defaults may
   137   be overridden by a private \texttt{etc/settings}.
   138   
   139 \item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to the full
   140   path names of the \texttt{isabelle-process} and \texttt{isatool}
   141   executables, respectively.  Thus other tools and scripts need not assume
   142   that the Isabelle \texttt{bin} directory is on the current search path of
   143   the shell.
   144   
   145 \item[\settdx{ISABELLE_IDENTIFIER}*] refers to the name of this
   146   Isabelle distribution, e.g.\ ``\texttt{Isabelle2007}''.
   147 
   148 \item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
   149   \settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
   150   system to be used for Isabelle.  There is only a fixed set of admissable
   151   \texttt{ML_SYSTEM} names (see the \texttt{etc/settings} file of the
   152   distribution).
   153   
   154   The actual compiler binary will be run from the directory \texttt{ML_HOME},
   155   with \texttt{ML_OPTIONS} as first arguments on the command line.  The
   156   optional \texttt{ML_PLATFORM} may specify the binary format of ML heap
   157   images, which is useful for cross-platform installations.  The value of
   158   \texttt{ML_IDENTIFIER} is automatically obtained by composing the values of
   159   \texttt{ML_SYSTEM}, \texttt{ML_PLATFORM} and the Isabelle version values.
   160   
   161 \item[\settdx{ISABELLE_PATH}] is a list of directories (separated by colons)
   162   where Isabelle logic images may reside.  When looking up heaps files, the
   163   value of \texttt{ML_IDENTIFIER} is appended to each component internally.
   164   
   165 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should
   166   be stored by default. The {\ML} system and Isabelle version identifier is
   167   appended here, too.
   168   
   169 \item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory browser
   170   information (HTML text, graph data, and printable documents) is stored (see
   171   also \S\ref{sec:info}).  The default value is
   172   \texttt{\$ISABELLE_HOME_USER/browser_info}.
   173   
   174 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is
   175   given explicitely by the user.  The default value is \texttt{HOL}.
   176   
   177 \item[\settdx{ISABELLE_LINE_EDITOR}] specifies the default line editor
   178   for \texttt{isatool tty} (see also \S\ref{sec:tool-tty}).
   179 
   180 \item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command
   181   line of any \texttt{isatool usedir} invocation (see also
   182   \S\ref{sec:tool-usedir}). This typically contains compilation options for
   183   object-logics --- \texttt{usedir} is the basic utility for managing logic
   184   sessions (cf.\ the \texttt{IsaMakefile}s in the distribution).
   185 
   186 \item[\settdx{ISABELLE_FILE_IDENT}] specifies a shell command for
   187   producing a source file identification, based on the actual content
   188   instead of the full physical path and date stamp (which is the
   189   default). A typical identification would produce a ``digest'' of the
   190   text, using a cryptographic hash function like SHA-1, for example.
   191   
   192 \item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX},
   193   \settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related
   194   tools for Isabelle document preparation (see also \S\ref{sec:tool-latex}).
   195   
   196 \item[\settdx{ISABELLE_TOOLS}] is a colon separated list of directories that
   197   are scanned by \texttt{isatool} for external utility programs (see also
   198   \S\ref{sec:isatool}).
   199   
   200 \item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories with
   201   documentation files.
   202   
   203 \item[\settdx{ISABELLE_DOC_FORMAT}] specifies the preferred document format,
   204   typically \texttt{dvi} or \texttt{pdf}.
   205   
   206 \item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying
   207   \texttt{dvi} files.
   208   
   209 \item[\settdx{PDF_VIEWER}] specifies the command to be used for displaying
   210   \texttt{pdf} files.
   211   
   212 \item[\settdx{PRINT_COMMAND}] specifies the standard printer spool command,
   213   which is expected to accept \texttt{ps} files.
   214   
   215 \item[\settdx{ISABELLE_TMP_PREFIX}*] is the prefix from which any running
   216   \texttt{isabelle} process derives an individual directory for temporary
   217   files.  The default is somewhere in \texttt{/tmp}.
   218   
   219 \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the actual
   220   user interface that the capital \texttt{Isabelle} or
   221   \texttt{isabelle-interface} should invoke.  See \S\ref{sec:interface} for
   222   more details.
   223 
   224 \end{description}
   225 
   226 
   227 \section{The Isabelle tools wrapper} \label{sec:isatool}
   228 
   229 All Isabelle related utilities are called via a common wrapper ---
   230 \ttindex{isatool}:
   231 \begin{ttbox}
   232 Usage: isatool TOOL [ARGS ...]
   233 
   234   Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
   235   for more specific help.
   236 
   237   Available tools are:
   238 
   239     browser - Isabelle graph browser
   240     \dots
   241 \end{ttbox}
   242 In principle, Isabelle tools are ordinary executable scripts that are run
   243 within the Isabelle settings environment, see \S\ref{sec:settings}.  The set
   244 of available tools is collected by \texttt{isatool} from the directories
   245 listed in the \texttt{ISABELLE_TOOLS} setting.  Do not try to call the scripts
   246 directly from the shell.  Neither should you add the tool directories to your
   247 shell's search path!
   248 
   249 
   250 \subsubsection*{Examples}
   251 
   252 Show the list of available documentation of the current Isabelle installation
   253 like this:
   254 \begin{ttbox}
   255   isatool doc
   256 \end{ttbox}
   257 
   258 View a certain document as follows:
   259 \begin{ttbox}
   260   isatool doc isar-ref
   261 \end{ttbox}
   262 
   263 Create an Isabelle session derived from HOL (see also \S\ref{sec:tool-mkdir}
   264 and \S\ref{sec:tool-make}):
   265 \begin{ttbox}
   266   isatool mkdir HOL Test && isatool make
   267 \end{ttbox}
   268 Note that \texttt{isatool mkdir} is usually only invoked once; existing
   269 sessions (including document output etc.) are then updated by \texttt{isatool
   270   make} alone.
   271 
   272 
   273 \section{The raw Isabelle process}
   274 
   275 The \ttindex{isabelle} (or \ttindex{isabelle-process}) executable runs
   276 bare-bones Isabelle logic sessions --- either interactively or in batch mode.
   277 It provides an abstraction over the underlying {\ML} system, and over the
   278 actual heap file locations.  Its usage is:
   279 \begin{ttbox}
   280 Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
   281 
   282   Options are:
   283     -C           tell ML system to copy output image
   284     -I           startup Isar interaction mode
   285     -P           startup Proof General interaction mode
   286     -S           secure mode -- disallow critical operations
   287     -W           startup process wrapper (interaction via external program)
   288     -X           startup PGIP interaction mode
   289     -c           tell ML system to compress output image
   290     -e MLTEXT    pass MLTEXT to the ML session
   291     -f           pass 'Session.finish();' to the ML session
   292     -m MODE      add print mode for output
   293     -q           non-interactive session
   294     -r           open heap file read-only
   295     -u           pass 'use"ROOT.ML";' to the ML session
   296     -w           reset write permissions on OUTPUT
   297 
   298   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
   299   These are either names to be searched in the Isabelle path, or
   300   actual file names (containing at least one /).
   301   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   302 \end{ttbox}
   303 Input files without path specifications are looked up in the
   304 \texttt{ISABELLE_PATH} setting, which may consist of multiple components
   305 separated by colons --- these are tried in the given order with the value of
   306 \texttt{ML_IDENTIFIER} appended internally.  In a similar way, base names are
   307 relative to the directory specified by \texttt{ISABELLE_OUTPUT}.  In any case,
   308 actual file locations may also be given by including at least one slash
   309 (\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
   310 directory).
   311 
   312 
   313 \subsection*{Options}
   314 
   315 If the input heap file does not have write permission bits set, or the
   316 \texttt{-r} option is given explicitely, then the session started will be
   317 read-only.  That is, the {\ML} world cannot be committed back into the image
   318 file.  Otherwise, a writable session enables commits into either the input
   319 file, or into another output heap file (if that is given as the second
   320 argument on the command line).
   321 
   322 The read-write state of sessions is determined at startup only, it cannot be
   323 changed intermediately. Also note that heap images may require considerable
   324 amounts of disk space (approximately 40--80~MB). Users are responsible for
   325 themselves to dispose their heap files when they are no longer needed.
   326 
   327 \medskip The \texttt{-w} option makes the output heap file read-only after
   328 terminating.  Thus subsequent invocations cause the logic image to be
   329 read-only automatically.
   330 
   331 \medskip The \texttt{-c} option tells the underlying ML system to compress the
   332 output heap (fully transparently).  On Poly/ML for example, the image is
   333 garbage collected and all stored values are maximally shared, resulting in up
   334 to 50\% less disk space consumption.
   335 
   336 \medskip The \texttt{-C} option tells the ML system to produce a completely
   337 self-contained output image, probably including a copy of the ML runtime
   338 system itself.
   339 
   340 \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
   341 the Isabelle session from the command line. Multiple \texttt{-e}'s are
   342 evaluated in the given order. Strange things may happen when errorneous {\ML}
   343 code is provided. Also make sure that the {\ML} commands are terminated
   344 properly by semicolon.
   345 
   346 \medskip The \texttt{-u} option is a shortcut for \texttt{-e} passing
   347 ``\texttt{use"ROOT.ML";}'' to the {\ML} session.  The \texttt{-f} option
   348 passes ``\texttt{Session.finish();}'', which is intended mainly for
   349 administrative purposes.
   350 
   351 \medskip The \texttt{-m} option adds identifiers of print modes to be made
   352 active for this session. Typically, this is used by some user interface, e.g.\ 
   353 to enable output of proper mathematical symbols.
   354 
   355 \medskip Isabelle normally enters an interactive top-level loop (after
   356 processing the \texttt{-e} texts). The \texttt{-q} option inhibits
   357 interaction, thus providing a pure batch mode facility.
   358 
   359 \medskip The \texttt{-I} option makes Isabelle enter Isar interaction
   360 mode on startup, instead of the primitive {\ML} top-level.  The
   361 \texttt{-P} option configures the top-level loop for interaction with
   362 the Proof~General user interface, and the \texttt{-X} option enables
   363 XML-based PGIP communication.  The \texttt{-W} option makes Isabelle
   364 enter a special process wrapper for interaction via an external
   365 program; the protocol is a stripped-down version of Proof~General the
   366 interaction mode.
   367 
   368 \medskip The \texttt{-S} option makes the Isabelle process more secure
   369 by disabling some critical operations, notably runtime compilation and
   370 evaluation of ML source code.
   371 
   372 
   373 \subsection*{Examples}
   374 
   375 Run an interactive session of the default object-logic (as specified
   376 by the \texttt{ISABELLE_LOGIC} setting) like this:
   377 \begin{ttbox}
   378 isabelle
   379 \end{ttbox}
   380 Usually \texttt{ISABELLE_LOGIC} refers to one of the standard logic
   381 images, which are read-only by default.  A writable session --- based
   382 on \texttt{FOL}, but output to \texttt{Foo} (in the directory
   383 specified by the \texttt{ISABELLE_OUTPUT} setting) --- may be invoked
   384 as follows:
   385 \begin{ttbox}
   386 isabelle FOL Foo
   387 \end{ttbox}
   388 Ending this session normally (e.g.\ by typing control-D) dumps the whole {\ML}
   389 system state into \texttt{Foo}. Be prepared for several tens of megabytes.
   390 
   391 The \texttt{Foo} session may be continued later (still in writable
   392 state) by:
   393 \begin{ttbox}
   394 isabelle Foo
   395 \end{ttbox}
   396 A read-only \texttt{Foo} session may be started by:
   397 \begin{ttbox}
   398 isabelle -r Foo
   399 \end{ttbox}
   400 
   401 \medskip Note that manual session management like this does \emph{not} provide
   402 proper setup for theory presentation.  This would require the \texttt{usedir}
   403 utility, see \S\ref{sec:tool-usedir}.
   404 
   405 \bigskip The next example demonstrates batch execution of Isabelle. We print a
   406 certain theorem of \texttt{FOL}:
   407 \begin{ttbox}
   408 isabelle -e "prth allE;" -q -r FOL
   409 \end{ttbox}
   410 Note that the output text will be interspersed with additional junk messages
   411 by the {\ML} runtime environment.
   412 
   413 
   414 \section{The Isabelle interface wrapper}\label{sec:interface}
   415 
   416 Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
   417 \ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
   418 uniform way for end-users to invoke a certain interface; which one to start is
   419 determined by the \settdx{ISABELLE_INTERFACE} setting variable, which should
   420 give a full path specification to the actual executable.  Also note that the
   421 \texttt{install} utility provides some options to install desktop environment
   422 icons (see \S\ref{sec:tool-install}).
   423 
   424 Presently, the most prominent Isabelle interface is
   425 Proof~General~\cite{proofgeneral}\index{user interface!Proof General}.  There
   426 are separate versions for the raw ML top-level and the proper Isabelle/Isar
   427 interpreter loop.  The Proof~General distribution includes separate interface
   428 wrapper scripts (in \texttt{ProofGeneral/isa} and \texttt{ProofGeneral/isar})
   429 for either of these.  The canonical settings for Isabelle/Isar are as follows:
   430 \begin{ttbox}
   431 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
   432 PROOFGENERAL_OPTIONS=""
   433 \end{ttbox}
   434 Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
   435 the Proof~General Lisp packages.  There are some options available, such as
   436 \texttt{-l} for passing the logic image to be used by default, or \texttt{-m}
   437 to tune the standard print mode.  The \texttt{-I} option allows to switch
   438 between the Isar and ML view, independently of the interface script being
   439 used.
   440   
   441 \medskip Note that the world may be also seen the other way round: Emacs may
   442 be started first (with proper setup of Proof~General mode), and
   443 \texttt{isabelle} run from within.  This requires further Emacs Lisp
   444 configuration, see the Proof~General documentation \cite{proofgeneral} for
   445 more information.
   446 
   447 %%% Local Variables:
   448 %%% mode: latex
   449 %%% TeX-master: "system"
   450 %%% End: