src/Doc/System/Sessions.thy
author wenzelm
Fri May 17 19:04:52 2013 +0200 (2013-05-17)
changeset 52056 fc458f304f93
parent 51417 d266f9329368
child 52735 842b5e7dcac8
permissions -rw-r--r--
added isabelle-process option -o;
     1 theory Sessions
     2 imports Base
     3 begin
     4 
     5 chapter {* Isabelle sessions and build management \label{ch:session} *}
     6 
     7 text {* An Isabelle \emph{session} consists of a collection of related
     8   theories that may be associated with formal documents
     9   (\chref{ch:present}).  There is also a notion of \emph{persistent
    10   heap} image to capture the state of a session, similar to
    11   object-code in compiled programming languages.  Thus the concept of
    12   session resembles that of a ``project'' in common IDE environments,
    13   but the specific name emphasizes the connection to interactive
    14   theorem proving: the session wraps-up the results of
    15   user-interaction with the prover in a persistent form.
    16 
    17   Application sessions are built on a given parent session, which may
    18   be built recursively on other parents.  Following this path in the
    19   hierarchy eventually leads to some major object-logic session like
    20   @{text "HOL"}, which itself is based on @{text "Pure"} as the common
    21   root of all sessions.
    22 
    23   Processing sessions may take considerable time.  Isabelle build
    24   management helps to organize this efficiently.  This includes
    25   support for parallel build jobs, in addition to the multithreaded
    26   theory and proof checking that is already provided by the prover
    27   process itself.  *}
    28 
    29 
    30 section {* Session ROOT specifications \label{sec:session-root} *}
    31 
    32 text {* Session specifications reside in files called @{verbatim ROOT}
    33   within certain directories, such as the home locations of registered
    34   Isabelle components or additional project directories given by the
    35   user.
    36 
    37   The ROOT file format follows the lexical conventions of the
    38   \emph{outer syntax} of Isabelle/Isar, see also
    39   \cite{isabelle-isar-ref}.  This defines common forms like
    40   identifiers, names, quoted strings, verbatim text, nested comments
    41   etc.  The grammar for @{syntax session_chapter} and @{syntax
    42   session_entry} is given as syntax diagram below; each ROOT file may
    43   contain multiple specifications like this.  Chapters help to
    44   organize browser info (\secref{sec:info}), but have no formal
    45   meaning.  The default chapter is ``@{text "Unsorted"}''.
    46 
    47   Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
    48   mode @{verbatim "isabelle-root"} for session ROOT files, which is
    49   enabled by default for any file of that name.
    50 
    51   @{rail "
    52     @{syntax_def session_chapter}: @'chapter' @{syntax name}
    53     ;
    54 
    55     @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
    56     ;
    57     body: description? options? ( theories + ) files?
    58     ;
    59     spec: @{syntax name} groups? dir?
    60     ;
    61     groups: '(' (@{syntax name} +) ')'
    62     ;
    63     dir: @'in' @{syntax name}
    64     ;
    65     description: @'description' @{syntax text}
    66     ;
    67     options: @'options' opts
    68     ;
    69     opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
    70     ;
    71     value: @{syntax name} | @{syntax real}
    72     ;
    73     theories: @'theories' opts? ( @{syntax name} * )
    74     ;
    75     files: @'files' ( @{syntax name} + )
    76     "}
    77 
    78   \begin{description}
    79 
    80   \item \isakeyword{session}~@{text "A = B + body"} defines a new
    81   session @{text "A"} based on parent session @{text "B"}, with its
    82   content given in @{text body} (theories and auxiliary source files).
    83   Note that a parent (like @{text "HOL"}) is mandatory in practical
    84   applications: only Isabelle/Pure can bootstrap itself from nothing.
    85 
    86   All such session specifications together describe a hierarchy (tree)
    87   of sessions, with globally unique names.  The new session name
    88   @{text "A"} should be sufficiently long and descriptive to stand on
    89   its own in a potentially large library.
    90 
    91   \item \isakeyword{session}~@{text "A (groups)"} indicates a
    92   collection of groups where the new session is a member.  Group names
    93   are uninterpreted and merely follow certain conventions.  For
    94   example, the Isabelle distribution tags some important sessions by
    95   the group name called ``@{text "main"}''.  Other projects may invent
    96   their own conventions, but this requires some care to avoid clashes
    97   within this unchecked name space.
    98 
    99   \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
   100   specifies an explicit directory for this session; by default this is
   101   the current directory of the @{verbatim ROOT} file.
   102 
   103   All theories and auxiliary source files are located relatively to
   104   the session directory.  The prover process is run within the same as
   105   its current working directory.
   106 
   107   \item \isakeyword{description}~@{text "text"} is a free-form
   108   annotation for this session.
   109 
   110   \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
   111   separate options (\secref{sec:system-options}) that are used when
   112   processing this session, but \emph{without} propagation to child
   113   sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for
   114   Boolean options.
   115 
   116   \item \isakeyword{theories}~@{text "options names"} specifies a
   117   block of theories that are processed within an environment that is
   118   augmented by the given options, in addition to the global session
   119   options given before.  Any number of blocks of \isakeyword{theories}
   120   may be given.  Options are only active for each
   121   \isakeyword{theories} block separately.
   122 
   123   \item \isakeyword{files}~@{text "files"} lists additional source
   124   files that are involved in the processing of this session.  This
   125   should cover anything outside the formal content of the theory
   126   sources, say some auxiliary {\TeX} files that are required for
   127   document processing.  In contrast, files that are loaded formally
   128   within a theory, e.g.\ via @{keyword "ML_file"}, need not be
   129   declared again.
   130 
   131   \end{description}
   132 *}
   133 
   134 
   135 subsubsection {* Examples *}
   136 
   137 text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
   138   relevant situations, although it uses relatively complex
   139   quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},
   140   @{text "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
   141   unqualified names that are relatively long and descriptive, as in
   142   the Archive of Formal Proofs (\url{http://afp.sf.net}), for
   143   example. *}
   144 
   145 
   146 section {* System build options \label{sec:system-options} *}
   147 
   148 text {* See @{file "~~/etc/options"} for the main defaults provided by
   149   the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
   150   includes a simple editing mode @{verbatim "isabelle-options"} for
   151   this file-format.
   152 
   153   The following options are particulary relevant to build Isabelle
   154   sessions, in particular with document preparation
   155   (\chref{ch:present}).
   156 
   157   \begin{itemize}
   158 
   159   \item @{system_option_def "browser_info"} controls output of HTML
   160   browser info, see also \secref{sec:info}.
   161 
   162   \item @{system_option_def "document"} specifies the document output
   163   format, see @{tool document} option @{verbatim "-o"} in
   164   \secref{sec:tool-document}.  In practice, the most relevant values
   165   are @{verbatim "document=false"} or @{verbatim "document=pdf"}.
   166 
   167   \item @{system_option_def "document_output"} specifies an
   168   alternative directory for generated output of the document
   169   preparation system; the default is within the @{setting
   170   "ISABELLE_BROWSER_INFO"} hierarchy as explained in
   171   \secref{sec:info}.  See also @{tool mkroot}, which generates a
   172   default configuration with output readily available to the author of
   173   the document.
   174 
   175   \item @{system_option_def "document_variants"} specifies document
   176   variants as a colon-separated list of @{text "name=tags"} entries,
   177   corresponding to @{tool document} options @{verbatim "-n"} and
   178   @{verbatim "-t"}.
   179 
   180   For example, @{verbatim
   181   "document_variants=document:outline=/proof,/ML"} indicates two
   182   documents: the one called @{verbatim document} with default tags,
   183   and the other called @{verbatim outline} where proofs and ML
   184   sections are folded.
   185 
   186   Document variant names are just a matter of conventions.  It is also
   187   possible to use different document variant names (without tags) for
   188   different document root entries, see also
   189   \secref{sec:tool-document}.
   190 
   191   \item @{system_option_def "document_graph"} tells whether the
   192   generated document files should include a theory graph (cf.\
   193   \secref{sec:browse} and \secref{sec:info}).  The resulting EPS or
   194   PDF file can be included as graphics in {\LaTeX}.
   195 
   196   Note that this option is usually determined as static parameter of
   197   some session (e.g.\ within its @{verbatim ROOT} file) and \emph{not}
   198   given globally or on the command line of @{tool build}.
   199 
   200   \item @{system_option_def "threads"} determines the number of worker
   201   threads for parallel checking of theories and proofs.  The default
   202   @{text "0"} means that a sensible maximum value is determined by the
   203   underlying hardware.  For machines with many cores or with
   204   hyperthreading, this is often requires manual adjustment (on the
   205   command-line or within personal settings or preferences, not within
   206   a session @{verbatim ROOT}).
   207 
   208   \item @{system_option_def "condition"} specifies a comma-separated
   209   list of process environment variables (or Isabelle settings) that
   210   are required for the subsequent theories to be processed.
   211   Conditions are considered ``true'' if the corresponding environment
   212   value is defined and non-empty.
   213 
   214   For example, the @{verbatim "condition=ISABELLE_FULL_TEST"} may be
   215   used to guard extraordinary theories, which are meant to be enabled
   216   explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"}
   217   before invoking @{tool build}.
   218 
   219   \item @{system_option_def "timeout"} specifies a real wall-clock
   220   timeout (in seconds) for the session as a whole.  The timer is
   221   controlled outside the ML process by the JVM that runs
   222   Isabelle/Scala.  Thus it is relatively reliable in canceling
   223   processes that get out of control, even if there is a deadlock
   224   without CPU time usage.
   225 
   226   \end{itemize}
   227 
   228   The @{tool_def options} tool prints Isabelle system options.  Its
   229   command-line usage is:
   230 \begin{ttbox}
   231 Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
   232 
   233   Options are:
   234     -b           include $ISABELLE_BUILD_OPTIONS
   235     -l           list options
   236     -x FILE      export to FILE in YXML format
   237 
   238   Report Isabelle system options, augmented by MORE_OPTIONS given as
   239   arguments NAME=VAL or NAME.
   240 \end{ttbox}
   241 
   242   The command line arguments provide additional system options of the
   243   form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
   244   for Boolean options.
   245 
   246   Option @{verbatim "-b"} augments the implicit environment of system
   247   options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
   248   \secref{sec:tool-build}.
   249 
   250   Option @{verbatim "-x"} specifies a file to export the result in
   251   YXML format, instead of printing it in human-readable form.
   252 *}
   253 
   254 
   255 section {* Invoking the build process \label{sec:tool-build} *}
   256 
   257 text {* The @{tool_def build} tool invokes the build process for
   258   Isabelle sessions.  It manages dependencies between sessions,
   259   related sources of theories and auxiliary files, and target heap
   260   images.  Accordingly, it runs instances of the prover process with
   261   optional document preparation.  Its command-line usage
   262   is:\footnote{Isabelle/Scala provides the same functionality via
   263   \texttt{isabelle.Build.build}.}
   264 \begin{ttbox}
   265 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   266 
   267   Options are:
   268     -D DIR       include session directory and select its sessions
   269     -R           operate on requirements of selected sessions
   270     -a           select all sessions
   271     -b           build heap images
   272     -c           clean build
   273     -d DIR       include session directory
   274     -g NAME      select session group NAME
   275     -j INT       maximum number of parallel jobs (default 1)
   276     -l           list session source files
   277     -n           no build -- test dependencies only
   278     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   279     -s           system build mode: produce output in ISABELLE_HOME
   280     -v           verbose
   281 
   282   Build and manage Isabelle sessions, depending on implicit
   283   ISABELLE_BUILD_OPTIONS="..."
   284 
   285   ML_PLATFORM="..."
   286   ML_HOME="..."
   287   ML_SYSTEM="..."
   288   ML_OPTIONS="..."
   289 \end{ttbox}
   290 
   291   \medskip Isabelle sessions are defined via session ROOT files as
   292   described in (\secref{sec:session-root}).  The totality of sessions
   293   is determined by collecting such specifications from all Isabelle
   294   component directories (\secref{sec:components}), augmented by more
   295   directories given via options @{verbatim "-d"}~@{text "DIR"} on the
   296   command line.  Each such directory may contain a session
   297   \texttt{ROOT} file with several session specifications.
   298 
   299   Any session root directory may refer recursively to further
   300   directories of the same kind, by listing them in a catalog file
   301   @{verbatim "ROOTS"} line-by-line.  This helps to organize large
   302   collections of session specifications, or to make @{verbatim "-d"}
   303   command line options persistent (say within @{verbatim
   304   "$ISABELLE_HOME_USER/ROOTS"}).
   305 
   306   \medskip The subset of sessions to be managed is determined via
   307   individual @{text "SESSIONS"} given as command-line arguments, or
   308   session groups that are given via one or more options @{verbatim
   309   "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
   310   The build tool takes session dependencies into account: the set of
   311   selected sessions is completed by including all ancestors.
   312 
   313   \medskip Option @{verbatim "-R"} reverses the selection in the sense
   314   that it refers to its requirements: all ancestor sessions excluding
   315   the original selection.  This allows to prepare the stage for some
   316   build process with different options, before running the main build
   317   itself (without option @{verbatim "-R"}).
   318 
   319   \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
   320   selects all sessions that are defined in the given directories.
   321 
   322   \medskip The build process depends on additional options
   323   (\secref{sec:system-options}) that are passed to the prover
   324   eventually.  The settings variable @{setting_ref
   325   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
   326   \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
   327   the environment of system build options may be augmented on the
   328   command line via @{verbatim "-o"}~@{text "name"}@{verbatim
   329   "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
   330   abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
   331   Boolean options.  Multiple occurrences of @{verbatim "-o"} on the
   332   command-line are applied in the given order.
   333 
   334   \medskip Option @{verbatim "-b"} ensures that heap images are
   335   produced for all selected sessions.  By default, images are only
   336   saved for inner nodes of the hierarchy of sessions, as required for
   337   other sessions to continue later on.
   338 
   339   \medskip Option @{verbatim "-c"} cleans all descendants of the
   340   selected sessions before performing the specified build operation.
   341 
   342   \medskip Option @{verbatim "-n"} omits the actual build process
   343   after the preparatory stage (including optional cleanup).  Note that
   344   the return code always indicates the status of the set of selected
   345   sessions.
   346 
   347   \medskip Option @{verbatim "-j"} specifies the maximum number of
   348   parallel build jobs (prover processes).  Each prover process is
   349   subject to a separate limit of parallel worker threads, cf.\ system
   350   option @{system_option_ref threads}.
   351 
   352   \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
   353   means that resulting heap images and log files are stored in
   354   @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
   355   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   356   ISABELLE_HOME_USER}, i.e.\ the user's home directory).
   357 
   358   \medskip Option @{verbatim "-v"} increases the general level of
   359   verbosity.  Option @{verbatim "-l"} lists the source files that
   360   contribute to a session.
   361 *}
   362 
   363 subsubsection {* Examples *}
   364 
   365 text {*
   366   Build a specific logic image:
   367 \begin{ttbox}
   368 isabelle build -b HOLCF
   369 \end{ttbox}
   370 
   371   \smallskip Build the main group of logic images:
   372 \begin{ttbox}
   373 isabelle build -b -g main
   374 \end{ttbox}
   375 
   376   \smallskip Provide a general overview of the status of all Isabelle
   377   sessions, without building anything:
   378 \begin{ttbox}
   379 isabelle build -a -n -v
   380 \end{ttbox}
   381 
   382   \smallskip Build all sessions with HTML browser info and PDF
   383   document preparation:
   384 \begin{ttbox}
   385 isabelle build -a -o browser_info -o document=pdf
   386 \end{ttbox}
   387 
   388   \smallskip Build all sessions with a maximum of 8 parallel prover
   389   processes and 4 worker threads each (on a machine with many cores):
   390 \begin{ttbox}
   391 isabelle build -a -j8 -o threads=4
   392 \end{ttbox}
   393 
   394   \smallskip Build some session images with cleanup of their
   395   descendants, while retaining their ancestry:
   396 \begin{ttbox}
   397 isabelle build -b -c HOL-Boogie HOL-SPARK
   398 \end{ttbox}
   399 
   400   \smallskip Clean all sessions without building anything:
   401 \begin{ttbox}
   402 isabelle build -a -n -c
   403 \end{ttbox}
   404 
   405   \smallskip Build all sessions from some other directory hierarchy,
   406   according to the settings variable @{verbatim "AFP"} that happens to
   407   be defined inside the Isabelle environment:
   408 \begin{ttbox}
   409 isabelle build -D '$AFP'
   410 \end{ttbox}
   411 
   412   \smallskip Inform about the status of all sessions required for AFP,
   413   without building anything yet:
   414 \begin{ttbox}
   415 isabelle build -D '$AFP' -R -v -n
   416 \end{ttbox}
   417 *}
   418 
   419 
   420 section {* Build dialog *}
   421 
   422 text {* The @{tool_def build_dialog} provides a simple GUI wrapper to
   423   the tool Isabelle @{tool build} tool.  This enables user interfaces
   424   like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made
   425   logic image on startup.  Its command-line usage is:
   426 \begin{ttbox}
   427 Usage: isabelle build_dialog [OPTIONS] LOGIC
   428 
   429   Options are:
   430     -L OPTION    default logic via system option
   431     -d DIR       include session directory
   432     -l NAME      logic session name
   433     -s           system build mode: produce output in ISABELLE_HOME
   434 
   435   Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC).
   436 \end{ttbox}
   437 
   438   \medskip Option @{verbatim "-l"} specifies an explicit logic session
   439   name.  Option @{verbatim "-L"} specifies a system option name as
   440   fall-back to determine the logic session name.  If both are omitted
   441   or have empty value, @{setting ISABELLE_LOGIC} is used as default.
   442 
   443   \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same
   444   meaning as for the command-line @{tool build} tool itself.  *}
   445 
   446 end