doc-src/System/Thy/Basics.thy
author wenzelm
Wed Sep 21 22:18:17 2011 +0200 (2011-09-21)
changeset 45028 d608dd8cd409
parent 43564 9864182c6bad
child 47661 012a887997f3
permissions -rw-r--r--
alternative Socket_Channel;
use BinIO for fifos uniformly;
     1 theory Basics
     2 imports Base
     3 begin
     4 
     5 chapter {* The Isabelle system environment *}
     6 
     7 text {*
     8   This manual describes Isabelle together with related tools and user
     9   interfaces as seen from a system oriented view.  See also the
    10   \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
    11   the actual Isabelle input language and related concepts.
    12 
    13   \medskip The Isabelle system environment provides the following
    14   basic infrastructure to integrate tools smoothly.
    15 
    16   \begin{enumerate}
    17 
    18   \item The \emph{Isabelle settings} mechanism provides process
    19   environment variables to all Isabelle executables (including tools
    20   and user interfaces).
    21 
    22   \item The \emph{raw Isabelle process} (@{executable_ref
    23   "isabelle-process"}) runs logic sessions either interactively or in
    24   batch mode.  In particular, this view abstracts over the invocation
    25   of the actual ML system to be used.  Regular users rarely need to
    26   care about the low-level process.
    27 
    28   \item The \emph{Isabelle tools wrapper} (@{executable_ref isabelle})
    29   provides a generic startup environment Isabelle related utilities,
    30   user interfaces etc.  Such tools automatically benefit from the
    31   settings mechanism.
    32 
    33   \end{enumerate}
    34 *}
    35 
    36 
    37 section {* Isabelle settings \label{sec:settings} *}
    38 
    39 text {*
    40   The Isabelle system heavily depends on the \emph{settings
    41   mechanism}\indexbold{settings}.  Essentially, this is a statically
    42   scoped collection of environment variables, such as @{setting
    43   ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
    44   variables are \emph{not} intended to be set directly from the shell,
    45   though.  Isabelle employs a somewhat more sophisticated scheme of
    46   \emph{settings files} --- one for site-wide defaults, another for
    47   additional user-specific modifications.  With all configuration
    48   variables in at most two places, this scheme is more maintainable
    49   and user-friendly than global shell environment variables.
    50 
    51   In particular, we avoid the typical situation where prospective
    52   users of a software package are told to put several things into
    53   their shell startup scripts, before being able to actually run the
    54   program. Isabelle requires none such administrative chores of its
    55   end-users --- the executables can be invoked straight away.
    56   Occasionally, users would still want to put the @{file
    57   "$ISABELLE_HOME/bin"} directory into their shell's search path, but
    58   this is not required.
    59 *}
    60 
    61 
    62 subsection {* Bootstrapping the environment \label{sec:boot} *}
    63 
    64 text {* Isabelle executables need to be run within a proper settings
    65   environment.  This is bootstrapped as described below, on the first
    66   invocation of one of the outer wrapper scripts (such as
    67   @{executable_ref isabelle}).  This happens only once for each
    68   process tree, i.e.\ the environment is passed to subprocesses
    69   according to regular Unix conventions.
    70 
    71   \begin{enumerate}
    72 
    73   \item The special variable @{setting_def ISABELLE_HOME} is
    74   determined automatically from the location of the binary that has
    75   been run.
    76   
    77   You should not try to set @{setting ISABELLE_HOME} manually. Also
    78   note that the Isabelle executables either have to be run from their
    79   original location in the distribution directory, or via the
    80   executable objects created by the @{tool install} utility.  Symbolic
    81   links are admissible, but a plain copy of the @{file
    82   "$ISABELLE_HOME/bin"} files will not work!
    83 
    84   \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
    85   @{executable_ref bash} shell script with the auto-export option for
    86   variables enabled.
    87   
    88   This file holds a rather long list of shell variable assigments,
    89   thus providing the site-wide default settings.  The Isabelle
    90   distribution already contains a global settings file with sensible
    91   defaults for most variables.  When installing the system, only a few
    92   of these may have to be adapted (probably @{setting ML_SYSTEM}
    93   etc.).
    94   
    95   \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
    96   exists) is run in the same way as the site default settings. Note
    97   that the variable @{setting ISABELLE_HOME_USER} has already been set
    98   before --- usually to something like @{verbatim
    99   "$HOME/.isabelle/IsabelleXXXX"}.
   100   
   101   Thus individual users may override the site-wide defaults.  See also
   102   file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
   103   distribution.  Typically, a user settings file would contain only a
   104   few lines, just the assigments that are really changed.  One should
   105   definitely \emph{not} start with a full copy the basic @{file
   106   "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
   107   maintainance problems later, when the Isabelle installation is
   108   updated or changed otherwise.
   109   
   110   \end{enumerate}
   111 
   112   Since settings files are regular GNU @{executable_def bash} scripts,
   113   one may use complex shell commands, such as @{verbatim "if"} or
   114   @{verbatim "case"} statements to set variables depending on the
   115   system architecture or other environment variables.  Such advanced
   116   features should be added only with great care, though. In
   117   particular, external environment references should be kept at a
   118   minimum.
   119 
   120   \medskip A few variables are somewhat special:
   121 
   122   \begin{itemize}
   123 
   124   \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
   125   automatically to the absolute path names of the @{executable
   126   "isabelle-process"} and @{executable isabelle} executables,
   127   respectively.
   128   
   129   \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
   130   the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
   131   the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
   132   to its value.
   133 
   134   \end{itemize}
   135 
   136   \medskip Note that the settings environment may be inspected with
   137   the Isabelle tool @{tool getenv}.  This might help to figure out the
   138   effect of complex settings scripts.
   139 *}
   140 
   141 
   142 subsection{* Common variables *}
   143 
   144 text {*
   145   This is a reference of common Isabelle settings variables. Note that
   146   the list is somewhat open-ended. Third-party utilities or interfaces
   147   may add their own selection. Variables that are special in some
   148   sense are marked with @{text "\<^sup>*"}.
   149 
   150   \begin{description}
   151 
   152   \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
   153   location of the top-level Isabelle distribution directory. This is
   154   automatically determined from the Isabelle executable that has been
   155   invoked.  Do not attempt to set @{setting ISABELLE_HOME} yourself
   156   from the shell!
   157   
   158   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
   159   counterpart of @{setting ISABELLE_HOME}. The default value is
   160   relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
   161   this may be changed in the global setting file.  Typically, the
   162   @{setting ISABELLE_HOME_USER} directory mimics @{setting
   163   ISABELLE_HOME} to some extend. In particular, site-wide defaults may
   164   be overridden by a private @{verbatim
   165   "$ISABELLE_HOME_USER/etc/settings"}.
   166   
   167   \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
   168   set to a symbolic identifier for the underlying hardware and
   169   operating system.  The Isabelle platform identification always
   170   refers to the 32 bit variant, even this is a 64 bit machine.  Note
   171   that the ML or Java runtime may have a different idea, depending on
   172   which binaries are actually run.
   173 
   174   \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
   175   @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
   176   on a platform that supports this; the value is empty for 32 bit.
   177 
   178   \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
   179   ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   180   names of the @{executable "isabelle-process"} and @{executable
   181   isabelle} executables, respectively.  Thus other tools and scripts
   182   need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
   183   on the current search path of the shell.
   184   
   185   \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
   186   to the name of this Isabelle distribution, e.g.\ ``@{verbatim
   187   Isabelle2011}''.
   188 
   189   \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
   190   @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
   191   ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
   192   to be used for Isabelle.  There is only a fixed set of admissable
   193   @{setting ML_SYSTEM} names (see the @{file
   194   "$ISABELLE_HOME/etc/settings"} file of the distribution).
   195   
   196   The actual compiler binary will be run from the directory @{setting
   197   ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
   198   command line.  The optional @{setting ML_PLATFORM} may specify the
   199   binary format of ML heap images, which is useful for cross-platform
   200   installations.  The value of @{setting ML_IDENTIFIER} is
   201   automatically obtained by composing the values of @{setting
   202   ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
   203   
   204   \item[@{setting_def ISABELLE_PATH}] is a list of directories
   205   (separated by colons) where Isabelle logic images may reside.  When
   206   looking up heaps files, the value of @{setting ML_IDENTIFIER} is
   207   appended to each component internally.
   208   
   209   \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
   210   directory where output heap files should be stored by default. The
   211   ML system and Isabelle version identifier is appended here, too.
   212   
   213   \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
   214   theory browser information (HTML text, graph data, and printable
   215   documents) is stored (see also \secref{sec:info}).  The default
   216   value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
   217   
   218   \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
   219   load if none is given explicitely by the user.  The default value is
   220   @{verbatim HOL}.
   221   
   222   \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
   223   line editor for the @{tool_ref tty} interface.
   224 
   225   \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
   226   to the command line of any @{tool_ref usedir} invocation. This
   227   typically contains compilation options for object-logics --- @{tool
   228   usedir} is the basic utility for managing logic sessions (cf.\ the
   229   @{verbatim IsaMakefile}s in the distribution).
   230 
   231   \item[@{setting_def ISABELLE_LATEX}, @{setting_def
   232   ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
   233   ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
   234   document preparation (see also \secref{sec:tool-latex}).
   235   
   236   \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
   237   directories that are scanned by @{executable isabelle} for external
   238   utility programs (see also \secref{sec:isabelle-tool}).
   239   
   240   \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
   241   directories with documentation files.
   242   
   243   \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
   244   document format, typically @{verbatim dvi} or @{verbatim pdf}.
   245   
   246   \item[@{setting_def DVI_VIEWER}] specifies the command to be used
   247   for displaying @{verbatim dvi} files.
   248   
   249   \item[@{setting_def PDF_VIEWER}] specifies the command to be used
   250   for displaying @{verbatim pdf} files.
   251   
   252   \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
   253   spool command, which is expected to accept @{verbatim ps} files.
   254   
   255   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
   256   prefix from which any running @{executable "isabelle-process"}
   257   derives an individual directory for temporary files.  The default is
   258   somewhere in @{verbatim "/tmp"}.
   259   
   260   \end{description}
   261 *}
   262 
   263 
   264 subsection {* Additional components \label{sec:components} *}
   265 
   266 text {* Any directory may be registered as an explicit \emph{Isabelle
   267   component}.  The general layout conventions are that of the main
   268   Isabelle distribution itself, and the following two files (both
   269   optional) have a special meaning:
   270 
   271   \begin{itemize}
   272 
   273   \item @{verbatim "etc/settings"} holds additional settings that are
   274   initialized when bootstrapping the overall Isabelle environment,
   275   cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
   276   @{verbatim bash} script.  It may refer to the component's enclosing
   277   directory via the @{verbatim "COMPONENT"} shell variable.
   278 
   279   For example, the following setting allows to refer to files within
   280   the component later on, without having to hardwire absolute paths:
   281 
   282   \begin{ttbox}
   283   MY_COMPONENT_HOME="$COMPONENT"
   284   \end{ttbox}
   285 
   286   Components can also add to existing Isabelle settings such as
   287   @{setting_def ISABELLE_TOOLS}, in order to provide
   288   component-specific tools that can be invoked by end-users.  For
   289   example:
   290 
   291   \begin{ttbox}
   292   ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
   293   \end{ttbox}
   294 
   295   \item @{verbatim "etc/components"} holds a list of further
   296   sub-components of the same structure.  The directory specifications
   297   given here can be either absolute (with leading @{verbatim "/"}) or
   298   relative to the component's main directory.
   299 
   300   \end{itemize}
   301 
   302   The root of component initialization is @{setting ISABELLE_HOME}
   303   itself.  After initializing all of its sub-components recursively,
   304   @{setting ISABELLE_HOME_USER} is included in the same manner (if
   305   that directory exists).  This allows to install private components
   306   via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
   307   often more convenient to do that programmatically via the
   308   \verb,init_component, shell function in the \verb,etc/settings,
   309   script of \verb,$ISABELLE_HOME_USER, (or any other component
   310   directory).  For example:
   311   \begin{verbatim}
   312   if [ -d "$HOME/screwdriver-2.0" ]
   313   then
   314     init_component "$HOME/screwdriver-2.0"
   315   else
   316   \end{verbatim}
   317 *}
   318 
   319 
   320 section {* The raw Isabelle process *}
   321 
   322 text {*
   323   The @{executable_def "isabelle-process"} executable runs bare-bones
   324   Isabelle logic sessions --- either interactively or in batch mode.
   325   It provides an abstraction over the underlying ML system, and over
   326   the actual heap file locations.  Its usage is:
   327 
   328 \begin{ttbox}
   329 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
   330 
   331   Options are:
   332     -I           startup Isar interaction mode
   333     -P           startup Proof General interaction mode
   334     -S           secure mode -- disallow critical operations
   335     -T ADDR      startup process wrapper, with socket address
   336     -W IN:OUT    startup process wrapper, with input/output fifos
   337     -X           startup PGIP interaction mode
   338     -e MLTEXT    pass MLTEXT to the ML session
   339     -f           pass 'Session.finish();' to the ML session
   340     -m MODE      add print mode for output
   341     -q           non-interactive session
   342     -r           open heap file read-only
   343     -u           pass 'use"ROOT.ML";' to the ML session
   344     -w           reset write permissions on OUTPUT
   345 
   346   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
   347   These are either names to be searched in the Isabelle path, or
   348   actual file names (containing at least one /).
   349   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   350 \end{ttbox}
   351 
   352   Input files without path specifications are looked up in the
   353   @{setting ISABELLE_PATH} setting, which may consist of multiple
   354   components separated by colons --- these are tried in the given
   355   order with the value of @{setting ML_IDENTIFIER} appended
   356   internally.  In a similar way, base names are relative to the
   357   directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
   358   actual file locations may also be given by including at least one
   359   slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
   360   refer to the current directory).
   361 *}
   362 
   363 
   364 subsubsection {* Options *}
   365 
   366 text {*
   367   If the input heap file does not have write permission bits set, or
   368   the @{verbatim "-r"} option is given explicitely, then the session
   369   started will be read-only.  That is, the ML world cannot be
   370   committed back into the image file.  Otherwise, a writable session
   371   enables commits into either the input file, or into another output
   372   heap file (if that is given as the second argument on the command
   373   line).
   374 
   375   The read-write state of sessions is determined at startup only, it
   376   cannot be changed intermediately. Also note that heap images may
   377   require considerable amounts of disk space (approximately
   378   50--200~MB). Users are responsible for themselves to dispose their
   379   heap files when they are no longer needed.
   380 
   381   \medskip The @{verbatim "-w"} option makes the output heap file
   382   read-only after terminating.  Thus subsequent invocations cause the
   383   logic image to be read-only automatically.
   384 
   385   \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
   386   passed to the Isabelle session from the command line. Multiple
   387   @{verbatim "-e"}'s are evaluated in the given order. Strange things
   388   may happen when errorneous ML code is provided. Also make sure that
   389   the ML commands are terminated properly by semicolon.
   390 
   391   \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
   392   "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
   393   The @{verbatim "-f"} option passes ``@{verbatim
   394   "Session.finish();"}'', which is intended mainly for administrative
   395   purposes.
   396 
   397   \medskip The @{verbatim "-m"} option adds identifiers of print modes
   398   to be made active for this session. Typically, this is used by some
   399   user interface, e.g.\ to enable output of proper mathematical
   400   symbols.
   401 
   402   \medskip Isabelle normally enters an interactive top-level loop
   403   (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
   404   option inhibits interaction, thus providing a pure batch mode
   405   facility.
   406 
   407   \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
   408   interaction mode on startup, instead of the primitive ML top-level.
   409   The @{verbatim "-P"} option configures the top-level loop for
   410   interaction with the Proof General user interface, and the
   411   @{verbatim "-X"} option enables XML-based PGIP communication.
   412 
   413   \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
   414   Isabelle enter a special process wrapper for interaction via the
   415   Isabelle/Scala layer, see also @{file
   416   "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
   417   the ML and JVM process is private to the implementation.
   418 
   419   \medskip The @{verbatim "-S"} option makes the Isabelle process more
   420   secure by disabling some critical operations, notably runtime
   421   compilation and evaluation of ML source code.
   422 *}
   423 
   424 
   425 subsubsection {* Examples *}
   426 
   427 text {*
   428   Run an interactive session of the default object-logic (as specified
   429   by the @{setting ISABELLE_LOGIC} setting) like this:
   430 \begin{ttbox}
   431 isabelle-process
   432 \end{ttbox}
   433 
   434   Usually @{setting ISABELLE_LOGIC} refers to one of the standard
   435   logic images, which are read-only by default.  A writable session
   436   --- based on @{verbatim FOL}, but output to @{verbatim Foo} (in the
   437   directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
   438   may be invoked as follows:
   439 \begin{ttbox}
   440 isabelle-process FOL Foo
   441 \end{ttbox}
   442   Ending this session normally (e.g.\ by typing control-D) dumps the
   443   whole ML system state into @{verbatim Foo}. Be prepared for several
   444   tens of megabytes.
   445 
   446   The @{verbatim Foo} session may be continued later (still in
   447   writable state) by:
   448 \begin{ttbox}
   449 isabelle-process Foo
   450 \end{ttbox}
   451   A read-only @{verbatim Foo} session may be started by:
   452 \begin{ttbox}
   453 isabelle-process -r Foo
   454 \end{ttbox}
   455 
   456   \medskip Note that manual session management like this does
   457   \emph{not} provide proper setup for theory presentation.  This would
   458   require the @{tool usedir} utility.
   459 
   460   \bigskip The next example demonstrates batch execution of Isabelle.
   461   We retrieve the @{verbatim FOL} theory value from the theory loader
   462   within ML:
   463 \begin{ttbox}
   464 isabelle-process -e 'theory "FOL";' -q -r FOL
   465 \end{ttbox}
   466   Note that the output text will be interspersed with additional junk
   467   messages by the ML runtime environment.  The @{verbatim "-W"} option
   468   allows to communicate with the Isabelle process via an external
   469   program in a more robust fashion.
   470 *}
   471 
   472 
   473 section {* The Isabelle tools wrapper \label{sec:isabelle-tool} *}
   474 
   475 text {*
   476   All Isabelle related tools and interfaces are called via a common
   477   wrapper --- @{executable isabelle}:
   478 
   479 \begin{ttbox}
   480 Usage: isabelle TOOL [ARGS ...]
   481 
   482   Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   483 
   484   Available tools are:
   485 
   486     browser - Isabelle graph browser
   487     \dots
   488 \end{ttbox}
   489 
   490   In principle, Isabelle tools are ordinary executable scripts that
   491   are run within the Isabelle settings environment, see
   492   \secref{sec:settings}.  The set of available tools is collected by
   493   @{executable isabelle} from the directories listed in the @{setting
   494   ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
   495   from the shell.  Neither should you add the tool directories to your
   496   shell's search path!
   497 *}
   498 
   499 
   500 subsubsection {* Examples *}
   501 
   502 text {*
   503   Show the list of available documentation of the current Isabelle
   504   installation like this:
   505 
   506 \begin{ttbox}
   507   isabelle doc
   508 \end{ttbox}
   509 
   510   View a certain document as follows:
   511 \begin{ttbox}
   512   isabelle doc isar-ref
   513 \end{ttbox}
   514 
   515   Create an Isabelle session derived from HOL (see also
   516   \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
   517 \begin{ttbox}
   518   isabelle mkdir HOL Test && isabelle make
   519 \end{ttbox}
   520   Note that @{verbatim "isabelle mkdir"} is usually only invoked once;
   521   existing sessions (including document output etc.) are then updated
   522   by @{verbatim "isabelle make"} alone.
   523 *}
   524 
   525 end