doc-src/System/Thy/Sessions.thy
author wenzelm
Tue Aug 14 15:42:58 2012 +0200 (2012-08-14)
changeset 48805 c3ea910b3581
parent 48739 3a6c03b15916
child 48814 d488a5f25bf6
permissions -rw-r--r--
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
     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 (see also
     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 a single @{syntax session_entry} is given as
    42   syntax diagram below; each ROOT file may contain multiple session
    43   specifications like this.
    44 
    45   Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
    46   mode @{verbatim "isabelle-root"} for session ROOT files.
    47 
    48   @{rail "
    49     @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
    50     ;
    51     body: description? options? ( theories * ) files?
    52     ;
    53     spec: @{syntax name} groups? dir?
    54     ;
    55     groups: '(' (@{syntax name} +) ')'
    56     ;
    57     dir: @'in' @{syntax name}
    58     ;
    59     description: @'description' @{syntax text}
    60     ;
    61     options: @'options' opts
    62     ;
    63     opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
    64     ;
    65     value: @{syntax name} | @{syntax real}
    66     ;
    67     theories: @'theories' opts? ( @{syntax name} * )
    68     ;
    69     files: @'files' ( @{syntax name} + )
    70     "}
    71 
    72   \begin{description}
    73 
    74   \item \isakeyword{session}~@{text "A = B + body"} defines a new
    75   session @{text "A"} based on parent session @{text "B"}, with its
    76   content given in @{text body} (theories and auxiliary source files).
    77   Note that a parent (like @{text "HOL"}) is mandatory in practical
    78   applications: only Isabelle/Pure can bootstrap itself from nothing.
    79 
    80   All such session specifications together describe a hierarchy (tree)
    81   of sessions, with globally unique names.  The new session name
    82   @{text "A"} should be sufficiently long to stand on its own in a
    83   potentially large library.
    84 
    85   \item \isakeyword{session}~@{text "A (groups)"} indicates a
    86   collection of groups where the new session is a member.  Group names
    87   are uninterpreted and merely follow certain conventions.  For
    88   example, the Isabelle distribution tags some important sessions by
    89   the group name called ``@{text "main"}''.  Other projects may invent
    90   their own conventions, but this requires some care to avoid clashes
    91   within this unchecked name space.
    92 
    93   \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
    94   specifies an explicit directory for this session; by default this is
    95   the current directory of the @{verbatim ROOT} file.
    96 
    97   All theories and auxiliary source files are located relatively to
    98   the session directory.  The prover process is run within the same as
    99   its current working directory.
   100 
   101   \item \isakeyword{description}~@{text "text"} is a free-form
   102   annotation for this session.
   103 
   104   \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
   105   separate options (\secref{sec:system-options}) that are used when
   106   processing this session, but \emph{without} propagation to child
   107   sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for
   108   Boolean options.
   109 
   110   \item \isakeyword{theories}~@{text "options names"} specifies a
   111   block of theories that are processed within an environment that is
   112   augmented by the given options, in addition to the global session
   113   options given before.  Any number of blocks of \isakeyword{theories}
   114   may be given.  Options are only active for each
   115   \isakeyword{theories} block separately.
   116 
   117   \item \isakeyword{files}~@{text "files"} lists additional source
   118   files that are involved in the processing of this session.  This
   119   should cover anything outside the formal content of the theory
   120   sources, say some auxiliary {\TeX} files that are required for
   121   document processing.  In contrast, files that are specified in
   122   formal theory headers as @{keyword "uses"} need not be declared
   123   again.
   124 
   125   \end{description}
   126 *}
   127 
   128 subsubsection {* Examples *}
   129 
   130 text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
   131   relevant situations, but it uses relatively complex quasi-hierarchic
   132   naming conventions like @{text "HOL\<dash>SPARK"}, @{text
   133   "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
   134   unqualified names that are relatively long and descriptive, as in
   135   the Archive of Formal Proofs (\url{http://afp.sf.net}), for
   136   example. *}
   137 
   138 
   139 section {* System build options \label{sec:system-options} *}
   140 
   141 text {* See @{file "~~/etc/options"} for the main defaults provided by
   142   the Isabelle distribution.  Isabelle/jEdit (\secref{sec:tool-jedit})
   143   includes a simple editing mode @{verbatim "isabelle-options"} for
   144   this file-format.
   145 
   146   The @{tool_def options} tool prints Isabelle system options.  Its
   147   command-line usage is:
   148 \begin{ttbox}
   149 Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
   150 
   151   Options are:
   152     -b           include $ISABELLE_BUILD_OPTIONS
   153     -x FILE      export to FILE in YXML format
   154 
   155   Print Isabelle system options, augmented by MORE_OPTIONS given as
   156   arguments NAME=VAL or NAME.
   157 \end{ttbox}
   158 
   159   The command line arguments provide additional system options of the
   160   form @{text "name"}@{verbatim "="}@{text "value"} or @{text name}
   161   for Boolean options.
   162 
   163   Option @{verbatim "-b"} augments the implicit environment of system
   164   options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
   165   \secref{sec:tool-build}.
   166 
   167   Option @{verbatim "-x"} specifies a file to export the result in
   168   YXML format, instead of printing it in human-readable form.
   169 *}
   170 
   171 
   172 section {* Invoking the build process \label{sec:tool-build} *}
   173 
   174 text {* The @{tool_def build} tool invokes the build process for
   175   Isabelle sessions.  It manages dependencies between sessions,
   176   related sources of theories and auxiliary files, and target heap
   177   images.  Accordingly, it runs instances of the prover process with
   178   optional document preparation.  Its command-line usage
   179   is:\footnote{Isabelle/Scala provides the same functionality via
   180   \texttt{isabelle.Build.build}.}
   181 \begin{ttbox}
   182 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   183 
   184   Options are:
   185     -D DIR       include session directory and select its sessions
   186     -a           select all sessions
   187     -b           build heap images
   188     -c           clean build
   189     -d DIR       include session directory
   190     -g NAME      select session group NAME
   191     -j INT       maximum number of parallel jobs (default 1)
   192     -n           no build -- test dependencies only
   193     -o OPTION    override session configuration OPTION
   194                  (via NAME=VAL or NAME)
   195     -s           system build mode: produce output in ISABELLE_HOME
   196     -v           verbose
   197 
   198   Build and manage Isabelle sessions, depending on implicit
   199   ISABELLE_BUILD_OPTIONS="..."
   200 
   201   ML_PLATFORM="..."
   202   ML_HOME="..."
   203   ML_SYSTEM="..."
   204   ML_OPTIONS="..."
   205 \end{ttbox}
   206 
   207   \medskip Isabelle sessions are defined via session ROOT files as
   208   described in (\secref{sec:session-root}).  The totality of sessions
   209   is determined by collecting such specifications from all Isabelle
   210   component directories (\secref{sec:components}), augmented by more
   211   directories given via options @{verbatim "-d"}~@{text "DIR"} on the
   212   command line.  Each such directory may contain a session
   213   \texttt{ROOT} file with several session specifications.
   214 
   215   Any session root directory may refer recursively to further
   216   directories of the same kind, by listing them in a catalog file
   217   @{verbatim "ROOTS"} line-by-line.  This helps to organize large
   218   collections of session specifications, or to make @{verbatim "-d"}
   219   command line options persistent (say within @{verbatim
   220   "$ISABELLE_HOME_USER/ROOTS"}).
   221 
   222   \medskip The subset of sessions to be managed is determined via
   223   individual @{text "SESSIONS"} given as command-line arguments, or
   224   session groups that are given via one or more options @{verbatim
   225   "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
   226   The build tool takes session dependencies into account: the set of
   227   selected sessions is completed by including all ancestors.
   228 
   229   \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but
   230   selects all sessions that are defined in the given directories.
   231 
   232   \medskip The build process depends on additional options
   233   (\secref{sec:system-options}) that are passed to the prover
   234   eventually.  The settings variable @{setting_ref
   235   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
   236   \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
   237   the environment of system build options may be augmented on the
   238   command line via @{verbatim "-o"}~@{text "name"}@{verbatim
   239   "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which
   240   abbreviates @{verbatim "-o"}~@{text "name"}@{verbatim"=true"} for
   241   Boolean options.  Multiple occurrences of @{verbatim "-o"} on the
   242   command-line are applied in the given order.
   243 
   244   \medskip Option @{verbatim "-b"} ensures that heap images are
   245   produced for all selected sessions.  By default, images are only
   246   saved for inner nodes of the hierarchy of sessions, as required for
   247   other sessions to continue later on.
   248 
   249   \medskip Option @{verbatim "-c"} cleans all descendants of the
   250   selected sessions before performing the specified build operation.
   251 
   252   \medskip Option @{verbatim "-n"} omits the actual build process
   253   after the preparatory stage (including optional cleanup).  Note that
   254   the return code always indicates the status of the set of selected
   255   sessions.
   256 
   257   \medskip Option @{verbatim "-j"} specifies the maximum number of
   258   parallel build jobs (prover processes).  Each prover process is
   259   subject to a separate limit of parallel worker threads, cf.\ system
   260   option @{system_option_ref threads}.
   261 
   262   \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
   263   means that resulting heap images and log files are stored in
   264   @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
   265   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   266   ISABELLE_HOME_USER}, i.e.\ the user's home directory).
   267 
   268   \medskip Option @{verbatim "-v"} enables verbose mode.
   269 *}
   270 
   271 subsubsection {* Examples *}
   272 
   273 text {*
   274   Build a specific logic image:
   275 \begin{ttbox}
   276 isabelle build -b HOLCF
   277 \end{ttbox}
   278 
   279   \smallskip Build the main group of logic images:
   280 \begin{ttbox}
   281 isabelle build -b -g main
   282 \end{ttbox}
   283 
   284   \smallskip Provide a general overview of the status of all Isabelle
   285   sessions, without building anything:
   286 \begin{ttbox}
   287 isabelle build -a -n -v
   288 \end{ttbox}
   289 
   290   \smallskip Build all sessions with HTML browser info and PDF
   291   document preparation:
   292 \begin{ttbox}
   293 isabelle build -a -o browser_info -o document=pdf
   294 \end{ttbox}
   295 
   296   \smallskip Build all sessions with a maximum of 8 parallel prover
   297   processes and 4 worker threads each (on a machine with many cores):
   298 \begin{ttbox}
   299 isabelle build -a -j8 -o threads=4
   300 \end{ttbox}
   301 
   302   \smallskip Build some session images with cleanup of their
   303   descendants, while retaining their ancestry:
   304 \begin{ttbox}
   305 isabelle build -b -c HOL-Boogie HOL-SPARK
   306 \end{ttbox}
   307 
   308   \smallskip Clean all sessions without building anything:
   309 \begin{ttbox}
   310 isabelle build -a -n -c
   311 \end{ttbox}
   312 
   313   \smallskip Build all sessions from some other directory hierarchy,
   314   according to the settings variable @{verbatim "AFP"} that happens to
   315   be defined inside the Isabelle environment:
   316 \begin{ttbox}
   317 isabelle build -D '$AFP'
   318 \end{ttbox}
   319 *}
   320 
   321 
   322 section {* Preparing session root directories \label{sec:tool-mkroot} *}
   323 
   324 text {* The @{tool_def mkroot} tool configures a given directory as
   325   session root, with some @{verbatim ROOT} file and optional document
   326   source directory.  Its usage is:
   327 \begin{ttbox}
   328 Usage: isabelle mkroot [OPTIONS] [DIR]
   329 
   330   Options are:
   331     -d           enable document preparation
   332     -n NAME      alternative session name (default: DIR base name)
   333 
   334   Prepare session root DIR (default: current directory).
   335 \end{ttbox}
   336 
   337   The results are placed in the given directory @{text dir}, which
   338   refers to the current directory by default.  The @{tool mkroot} tool
   339   is conservative in the sense that it does not overwrite existing
   340   files or directories.  Earlier attempts to generate a session root
   341   need to be deleted manually.
   342 
   343   \medskip Option @{verbatim "-d"} indicates that the session shall be
   344   accompanied by a formal document, with @{text dir}@{verbatim
   345   "/document/root.tex"} as its {\LaTeX} entry point (see also
   346   \chref{ch:present}).
   347 
   348   Option @{verbatim "-n"} allows to specify an alternative session
   349   name; otherwise the base name of the given directory is used.
   350 
   351   \medskip The implicit Isabelle settings variable @{setting
   352   ISABELLE_LOGIC} specifies the parent session, and @{setting
   353   ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
   354   into the generated @{verbatim ROOT} file.  *}
   355 
   356 
   357 subsubsection {* Examples *}
   358 
   359 text {* Produce session @{verbatim Test} within a separate directory
   360   of the same name:
   361 \begin{ttbox}
   362 isabelle mkroot Test && isabelle build -D Test
   363 \end{ttbox}
   364 
   365   \medskip Upgrade the current directory into a session ROOT with
   366   document preparation, and build it:
   367 \begin{ttbox}
   368 isabelle mkroot -d && isabelle build -D .
   369 \end{ttbox}
   370 *}
   371 
   372 end