author wenzelm
Wed Jan 22 17:02:05 2014 +0100 (2014-01-22)
changeset 55112 b1a5d603fd12
parent 54705 0dff3326d12a
child 56533 cd8b6d849b6a
permissions -rw-r--r--
prefer rail cartouche -- avoid back-slashed quotes;
proper documentation of \<newline> syntax;
     1 theory Sessions
     2 imports Base
     3 begin
     5 chapter {* Isabelle sessions and build management \label{ch:session} *}
     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.
    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.
    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.  *}
    30 section {* Session ROOT specifications \label{sec:session-root} *}
    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.
    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"}''.
    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.
    51   @{rail \<open>
    52     @{syntax_def session_chapter}: @'chapter' @{syntax name}
    53     ;
    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   \<close>}
    78   \begin{description}
    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.
    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.
    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.
    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.
   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.
   107   \item \isakeyword{description}~@{text "text"} is a free-form
   108   annotation for this session.
   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.
   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.
   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.
   131   \end{description}
   132 *}
   135 subsubsection {* Examples *}
   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 ""}), for
   143   example. *}
   146 section {* System build options \label{sec:system-options} *}
   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.
   153   The following options are particulary relevant to build Isabelle
   154   sessions, in particular with document preparation
   155   (\chref{ch:present}).
   157   \begin{itemize}
   159   \item @{system_option_def "browser_info"} controls output of HTML
   160   browser info, see also \secref{sec:info}.
   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"}.
   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.
   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"}.
   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.
   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}.
   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}.
   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}.
   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}).
   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.
   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}.
   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.
   226   \end{itemize}
   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 ...]
   233   Options are:
   234     -b           include $ISABELLE_BUILD_OPTIONS
   235     -g OPTION    get value of OPTION
   236     -l           list options
   237     -x FILE      export to FILE in YXML format
   239   Report Isabelle system options, augmented by MORE_OPTIONS given as
   240   arguments NAME=VAL or NAME.
   241 \end{ttbox}
   243   The command line arguments provide additional system options of the
   244   form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
   245   for Boolean options.
   247   Option @{verbatim "-b"} augments the implicit environment of system
   248   options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
   249   \secref{sec:tool-build}.
   251   Option @{verbatim "-g"} prints the value of the given option.
   252   Option @{verbatim "-l"} lists all options with their declaration and
   253   current value.
   255   Option @{verbatim "-x"} specifies a file to export the result in
   256   YXML format, instead of printing it in human-readable form.
   257 *}
   260 section {* Invoking the build process \label{sec:tool-build} *}
   262 text {* The @{tool_def build} tool invokes the build process for
   263   Isabelle sessions.  It manages dependencies between sessions,
   264   related sources of theories and auxiliary files, and target heap
   265   images.  Accordingly, it runs instances of the prover process with
   266   optional document preparation.  Its command-line usage
   267   is:\footnote{Isabelle/Scala provides the same functionality via
   268   \texttt{}.}
   269 \begin{ttbox}
   270 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   272   Options are:
   273     -D DIR       include session directory and select its sessions
   274     -R           operate on requirements of selected sessions
   275     -a           select all sessions
   276     -b           build heap images
   277     -c           clean build
   278     -d DIR       include session directory
   279     -g NAME      select session group NAME
   280     -j INT       maximum number of parallel jobs (default 1)
   281     -l           list session source files
   282     -n           no build -- test dependencies only
   283     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   284     -s           system build mode: produce output in ISABELLE_HOME
   285     -v           verbose
   287   Build and manage Isabelle sessions, depending on implicit
   290   ML_PLATFORM="..."
   291   ML_HOME="..."
   292   ML_SYSTEM="..."
   293   ML_OPTIONS="..."
   294 \end{ttbox}
   296   \medskip Isabelle sessions are defined via session ROOT files as
   297   described in (\secref{sec:session-root}).  The totality of sessions
   298   is determined by collecting such specifications from all Isabelle
   299   component directories (\secref{sec:components}), augmented by more
   300   directories given via options @{verbatim "-d"}~@{text "DIR"} on the
   301   command line.  Each such directory may contain a session
   302   \texttt{ROOT} file with several session specifications.
   304   Any session root directory may refer recursively to further
   305   directories of the same kind, by listing them in a catalog file
   306   @{verbatim "ROOTS"} line-by-line.  This helps to organize large
   307   collections of session specifications, or to make @{verbatim "-d"}
   308   command line options persistent (say within @{verbatim
   311   \medskip The subset of sessions to be managed is determined via
   312   individual @{text "SESSIONS"} given as command-line arguments, or
   313   session groups that are given via one or more options @{verbatim
   314   "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
   315   The build tool takes session dependencies into account: the set of
   316   selected sessions is completed by including all ancestors.
   318   \medskip Option @{verbatim "-R"} reverses the selection in the sense
   319   that it refers to its requirements: all ancestor sessions excluding
   320   the original selection.  This allows to prepare the stage for some
   321   build process with different options, before running the main build
   322   itself (without option @{verbatim "-R"}).
   324   \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
   325   selects all sessions that are defined in the given directories.
   327   \medskip The build process depends on additional options
   328   (\secref{sec:system-options}) that are passed to the prover
   329   eventually.  The settings variable @{setting_ref
   330   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
   331   \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
   332   the environment of system build options may be augmented on the
   333   command line via @{verbatim "-o"}~@{text "name"}@{verbatim
   334   "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
   335   abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
   336   Boolean options.  Multiple occurrences of @{verbatim "-o"} on the
   337   command-line are applied in the given order.
   339   \medskip Option @{verbatim "-b"} ensures that heap images are
   340   produced for all selected sessions.  By default, images are only
   341   saved for inner nodes of the hierarchy of sessions, as required for
   342   other sessions to continue later on.
   344   \medskip Option @{verbatim "-c"} cleans all descendants of the
   345   selected sessions before performing the specified build operation.
   347   \medskip Option @{verbatim "-n"} omits the actual build process
   348   after the preparatory stage (including optional cleanup).  Note that
   349   the return code always indicates the status of the set of selected
   350   sessions.
   352   \medskip Option @{verbatim "-j"} specifies the maximum number of
   353   parallel build jobs (prover processes).  Each prover process is
   354   subject to a separate limit of parallel worker threads, cf.\ system
   355   option @{system_option_ref threads}.
   357   \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
   358   means that resulting heap images and log files are stored in
   359   @{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location
   360   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   361   ISABELLE_HOME_USER}, i.e.\ the user's home directory).
   363   \medskip Option @{verbatim "-v"} increases the general level of
   364   verbosity.  Option @{verbatim "-l"} lists the source files that
   365   contribute to a session.
   366 *}
   368 subsubsection {* Examples *}
   370 text {*
   371   Build a specific logic image:
   372 \begin{ttbox}
   373 isabelle build -b HOLCF
   374 \end{ttbox}
   376   \smallskip Build the main group of logic images:
   377 \begin{ttbox}
   378 isabelle build -b -g main
   379 \end{ttbox}
   381   \smallskip Provide a general overview of the status of all Isabelle
   382   sessions, without building anything:
   383 \begin{ttbox}
   384 isabelle build -a -n -v
   385 \end{ttbox}
   387   \smallskip Build all sessions with HTML browser info and PDF
   388   document preparation:
   389 \begin{ttbox}
   390 isabelle build -a -o browser_info -o document=pdf
   391 \end{ttbox}
   393   \smallskip Build all sessions with a maximum of 8 parallel prover
   394   processes and 4 worker threads each (on a machine with many cores):
   395 \begin{ttbox}
   396 isabelle build -a -j8 -o threads=4
   397 \end{ttbox}
   399   \smallskip Build some session images with cleanup of their
   400   descendants, while retaining their ancestry:
   401 \begin{ttbox}
   402 isabelle build -b -c HOL-Algebra HOL-Word
   403 \end{ttbox}
   405   \smallskip Clean all sessions without building anything:
   406 \begin{ttbox}
   407 isabelle build -a -n -c
   408 \end{ttbox}
   410   \smallskip Build all sessions from some other directory hierarchy,
   411   according to the settings variable @{verbatim "AFP"} that happens to
   412   be defined inside the Isabelle environment:
   413 \begin{ttbox}
   414 isabelle build -D '$AFP'
   415 \end{ttbox}
   417   \smallskip Inform about the status of all sessions required for AFP,
   418   without building anything yet:
   419 \begin{ttbox}
   420 isabelle build -D '$AFP' -R -v -n
   421 \end{ttbox}
   422 *}
   424 end