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