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