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