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: