doc-src/System/Thy/Sessions.thy
author wenzelm
Sat Jul 28 19:37:35 2012 +0200 (2012-07-28)
changeset 48580 9df76dd45900
parent 48579 0b95a13ed90a
child 48582 c6bed330fc07
permissions -rw-r--r--
some description of main build options;
wenzelm@48578
     1
theory Sessions
wenzelm@48578
     2
imports Base
wenzelm@48578
     3
begin
wenzelm@48578
     4
wenzelm@48578
     5
chapter {* Isabelle sessions and build management *}
wenzelm@48578
     6
wenzelm@48578
     7
text {* FIXME *}
wenzelm@48578
     8
wenzelm@48578
     9
section {* Session ROOT specifications \label{sec:session-root} *}
wenzelm@48578
    10
wenzelm@48579
    11
text {* Session specifications reside in files called @{verbatim ROOT}
wenzelm@48579
    12
  within certain directories, such as the home locations of registered
wenzelm@48579
    13
  Isabelle components or additional project directories given by the
wenzelm@48579
    14
  user.
wenzelm@48579
    15
wenzelm@48579
    16
  The ROOT file format follows the lexical conventions of the
wenzelm@48579
    17
  \emph{outer syntax} of Isabelle/Isar, see also
wenzelm@48579
    18
  \cite{isabelle-isar-ref}.  This defines common forms like
wenzelm@48579
    19
  identifiers, names, quoted strings, verbatim text, nested comments
wenzelm@48579
    20
  etc.  The grammar for a single @{syntax session_entry} is given as
wenzelm@48579
    21
  syntax diagram below; each ROOT file may contain multiple session
wenzelm@48579
    22
  specifications like this.
wenzelm@48579
    23
wenzelm@48579
    24
  Note that Isabelle/jEdit \secref{sec:tool-jedit} includes a simple
wenzelm@48579
    25
  editing mode for session ROOT files.
wenzelm@48579
    26
wenzelm@48579
    27
  @{rail "
wenzelm@48579
    28
    @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
wenzelm@48579
    29
    ;
wenzelm@48579
    30
    body: description? options? ( theories * ) files?
wenzelm@48579
    31
    ;
wenzelm@48579
    32
    spec: @{syntax name} '!'? groups? dir?
wenzelm@48579
    33
    ;
wenzelm@48579
    34
    groups: '(' (@{syntax name} +) ')'
wenzelm@48579
    35
    ;
wenzelm@48579
    36
    dir: @'in' @{syntax name}
wenzelm@48579
    37
    ;
wenzelm@48579
    38
    description: @'description' @{syntax text}
wenzelm@48579
    39
    ;
wenzelm@48579
    40
    options: @'options' opts
wenzelm@48579
    41
    ;
wenzelm@48579
    42
    opts: '[' ( (@{syntax name} '=' @{syntax name} | @{syntax name}) + ',' ) ']'
wenzelm@48579
    43
    ;
wenzelm@48579
    44
    theories: @'theories' opts? ( @{syntax name} + )
wenzelm@48579
    45
    ;
wenzelm@48579
    46
    files: @'files' ( @{syntax name} + )
wenzelm@48579
    47
    "}
wenzelm@48579
    48
wenzelm@48579
    49
  \begin{description}
wenzelm@48579
    50
wenzelm@48579
    51
  \item \isakeyword{session}~@{text "A = B + body"} defines a new
wenzelm@48579
    52
  session @{text "A"} based on parent session @{text "B"}, with its
wenzelm@48579
    53
  content given in @{text body} (theories and auxiliary source files).
wenzelm@48579
    54
  Note that a parent (like @{text "HOL"}) is mandatory in practical
wenzelm@48579
    55
  applications: only Isabelle/Pure can bootstrap itself from nothing.
wenzelm@48579
    56
wenzelm@48579
    57
  All such session specifications together describe a hierarchy (tree)
wenzelm@48579
    58
  of sessions, with globally unique names.  By default, names are
wenzelm@48579
    59
  derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"}
wenzelm@48579
    60
  above.  Cumulatively, this leads to session paths of the form @{text
wenzelm@48579
    61
  "X\<dash>Y\<dash>Z\<dash>W"}.  Note that in the specification,
wenzelm@48579
    62
  @{text B} is already such a fully-qualified name, while @{text "A"}
wenzelm@48579
    63
  is the new base name.
wenzelm@48579
    64
wenzelm@48579
    65
  \item \isakeyword{session}~@{text "A! = B"} indicates a fresh start
wenzelm@48579
    66
  in the naming scheme: the session is called just @{text "A"} instead
wenzelm@48579
    67
  of @{text "B\<dash>A"}.  Here the name @{text "A"} should be
wenzelm@48579
    68
  sufficiently long to stand on its own in a potentially large
wenzelm@48579
    69
  library.
wenzelm@48579
    70
wenzelm@48579
    71
  \item \isakeyword{session}~@{text "A (groups)"} indicates a
wenzelm@48579
    72
  collection of groups where the new session is a member.  Group names
wenzelm@48579
    73
  are uninterpreted and merely follow certain conventions.  For
wenzelm@48579
    74
  example, the Isabelle distribution tags some important sessions by
wenzelm@48579
    75
  the group name @{text "main"}.  Other projects may invent their own
wenzelm@48579
    76
  conventions, which requires some care to avoid clashes within this
wenzelm@48579
    77
  unchecked name space.
wenzelm@48579
    78
wenzelm@48579
    79
  \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
wenzelm@48579
    80
  specifies an explicit directory for this session.  By default,
wenzelm@48579
    81
  \isakeyword{session}~@{text "A"} abbreviates
wenzelm@48579
    82
  \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}.  This
wenzelm@48579
    83
  accommodates the common scheme where some base directory contains
wenzelm@48579
    84
  several sessions in sub-directories of corresponding names.  Another
wenzelm@48579
    85
  common scheme is \isakeyword{session}~@{text
wenzelm@48579
    86
  "A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current
wenzelm@48579
    87
  directory of the ROOT file.
wenzelm@48579
    88
wenzelm@48579
    89
  All theories and auxiliary source files are located relatively to
wenzelm@48579
    90
  the session directory.  The prover process is run within the same as
wenzelm@48579
    91
  its current working directory.
wenzelm@48579
    92
wenzelm@48579
    93
  \item \isakeyword{description}~@{text "text"} is a free-form
wenzelm@48579
    94
  annotation for this session.
wenzelm@48579
    95
wenzelm@48579
    96
  \item \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
wenzelm@48579
    97
  separate options that are used when processing this session, but
wenzelm@48579
    98
  \emph{without} propagation to child sessions; see also
wenzelm@48579
    99
  \secref{sec:system-options}.  Note that @{text "z"} abbreviates
wenzelm@48579
   100
  @{text "z = true"} for Boolean options.
wenzelm@48579
   101
wenzelm@48579
   102
  \item \isakeyword{theories}~@{text "options names"} specifies a
wenzelm@48579
   103
  block of theories that are processed within an environment that is
wenzelm@48579
   104
  augmented further by the given options, in addition to the global
wenzelm@48579
   105
  session options given before.  Any number of blocks of
wenzelm@48579
   106
  \isakeyword{theories} may be given.  Options are only active for
wenzelm@48579
   107
  each \isakeyword{theories} block separately.
wenzelm@48579
   108
wenzelm@48579
   109
  \item \isakeyword{files}~@{text "files"} lists additional source
wenzelm@48579
   110
  files that are somehow involved in the processing of this session.
wenzelm@48579
   111
  This should cover anything outside the formal content of the theory
wenzelm@48579
   112
  sources, say some auxiliary {\TeX} files that are required for
wenzelm@48579
   113
  document processing.  In contrast, files that are specified in
wenzelm@48579
   114
  formal theory headers as @{keyword "uses"} need not be declared
wenzelm@48579
   115
  again.
wenzelm@48579
   116
wenzelm@48579
   117
  \end{description}
wenzelm@48580
   118
*}
wenzelm@48579
   119
wenzelm@48580
   120
subsubsection {* Examples *}
wenzelm@48580
   121
wenzelm@48580
   122
text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
wenzelm@48580
   123
  relevant situations. *}
wenzelm@48578
   124
wenzelm@48578
   125
wenzelm@48578
   126
section {* System build options \label{sec:system-options} *}
wenzelm@48578
   127
wenzelm@48580
   128
text {* See @{file "~~/etc/options"} for the main defaults provided by
wenzelm@48580
   129
  the Isabelle distribution.
wenzelm@48580
   130
wenzelm@48580
   131
  Note that Isabelle/jEdit \secref{sec:tool-jedit} includes a simple
wenzelm@48580
   132
  editing mode @{verbatim "isabelle-options"} for this file-format.
wenzelm@48580
   133
*}
wenzelm@48578
   134
wenzelm@48578
   135
wenzelm@48578
   136
section {* Invoking the build process \label{sec:tool-build} *}
wenzelm@48578
   137
wenzelm@48578
   138
text {* The @{tool_def build} utility invokes the build process for
wenzelm@48578
   139
  Isabelle sessions.  It manages dependencies between sessions,
wenzelm@48578
   140
  related sources of theories and auxiliary files, and target heap
wenzelm@48578
   141
  images.  Accordingly, it runs instances of the prover process with
wenzelm@48578
   142
  optional document preparation.  Its command-line usage
wenzelm@48578
   143
  is:\footnote{Isabelle/Scala provides the same functionality via
wenzelm@48578
   144
  \texttt{isabelle.Build.build}.}
wenzelm@48578
   145
\begin{ttbox} Usage: isabelle build [OPTIONS] [SESSIONS ...]
wenzelm@48578
   146
wenzelm@48578
   147
  Options are:
wenzelm@48578
   148
    -a           select all sessions
wenzelm@48578
   149
    -b           build heap images
wenzelm@48578
   150
    -d DIR       include session directory with ROOT file
wenzelm@48578
   151
    -g NAME      select session group NAME
wenzelm@48578
   152
    -j INT       maximum number of parallel jobs (default 1)
wenzelm@48578
   153
    -n           no build -- test dependencies only
wenzelm@48578
   154
    -o OPTION    override session configuration OPTION
wenzelm@48578
   155
                 (via NAME=VAL or NAME)
wenzelm@48578
   156
    -s           system build mode: produce output in ISABELLE_HOME
wenzelm@48578
   157
    -v           verbose
wenzelm@48578
   158
wenzelm@48578
   159
  Build and manage Isabelle sessions, depending on implicit
wenzelm@48578
   160
  ISABELLE_BUILD_OPTIONS="..."
wenzelm@48578
   161
wenzelm@48578
   162
  ML_PLATFORM="..."
wenzelm@48578
   163
  ML_HOME="..."
wenzelm@48578
   164
  ML_SYSTEM="..."
wenzelm@48578
   165
  ML_OPTIONS="..."
wenzelm@48578
   166
\end{ttbox}
wenzelm@48578
   167
wenzelm@48578
   168
  \medskip Isabelle sessions are defined via session ROOT files as
wenzelm@48578
   169
  described in (\secref{sec:session-root}).  The totality of sessions
wenzelm@48578
   170
  is determined by collecting such specifications from all Isabelle
wenzelm@48578
   171
  component directories (\secref{sec:components}), augmented by more
wenzelm@48578
   172
  directories given via options @{verbatim "-d"}~@{text "DIR"} on the
wenzelm@48578
   173
  command line.  Each such directory may contain a session
wenzelm@48578
   174
  \texttt{ROOT} file and an additional catalog file @{verbatim
wenzelm@48578
   175
  "etc/sessions"} with further sub-directories (list of lines).  Note
wenzelm@48578
   176
  that a single \texttt{ROOT} file usually defines many sessions;
wenzelm@48578
   177
  catalogs are are only required for extra scalability and modularity
wenzelm@48578
   178
  of large libraries.
wenzelm@48578
   179
wenzelm@48578
   180
  \medskip The subset of sessions to be managed is selected via
wenzelm@48578
   181
  individual @{text "SESSIONS"} given as command-line arguments, or
wenzelm@48578
   182
  session groups that are specified via one or more options @{verbatim
wenzelm@48578
   183
  "-g"}~@{text "NAME"}.  Option @{verbatim "-a"} selects all sessions.
wenzelm@48578
   184
  The build tool takes the hierarchy of sessions into account: the
wenzelm@48578
   185
  selected set of sessions is completed by including all ancestors
wenzelm@48578
   186
  according to the dependency structure.
wenzelm@48578
   187
wenzelm@48578
   188
  \medskip The build process depends on additional options that are
wenzelm@48578
   189
  passed to the prover session eventually, see also
wenzelm@48578
   190
  (\secref{sec:system-options}).  The settings variable @{setting_ref
wenzelm@48578
   191
  ISABELLE_BUILD_OPTIONS} allows to provide additional defaults.
wenzelm@48578
   192
  Moreover, the environment of system build options may be augmented
wenzelm@48578
   193
  on the command line via @{verbatim "-o"}~@{text "NAME=VALUE"} or
wenzelm@48578
   194
  @{verbatim "-o"}~@{text "NAME"}, which abbreviates @{verbatim
wenzelm@48578
   195
  "-o"}~@{text "NAME=true"} for Boolean options.  Multiple occurrences
wenzelm@48578
   196
  of @{verbatim "-o"} on the command-line are applied in the given
wenzelm@48578
   197
  order.
wenzelm@48578
   198
wenzelm@48578
   199
  \medskip Option @{verbatim "-b"} ensures that heap images are
wenzelm@48578
   200
  produced for all selected sessions.  By default, images are only
wenzelm@48578
   201
  saved for inner nodes of the hierarchy of sessions, as required for
wenzelm@48578
   202
  other sessions to continue later on.
wenzelm@48578
   203
wenzelm@48578
   204
  \medskip Option @{verbatim "-j"} specifies the maximum number of
wenzelm@48578
   205
  parallel build jobs (prover processes).  Note that each process is
wenzelm@48578
   206
  subject to a separate limit of parallel threads, cf.\ system option
wenzelm@48578
   207
  @{system_option_ref threads}.
wenzelm@48578
   208
wenzelm@48578
   209
  \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
wenzelm@48578
   210
  means that resulting heap images and log files are stored in
wenzelm@48578
   211
  @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
wenzelm@48578
   212
  @{setting ISABELLE_OUTPUT} (which is normally in @{setting
wenzelm@48578
   213
  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
wenzelm@48578
   214
wenzelm@48578
   215
  \medskip Option @{verbatim "-n"} omits the actual build process
wenzelm@48578
   216
  after performing all dependency checks.  The return code indicates
wenzelm@48578
   217
  the status of the set of selected sessions.
wenzelm@48578
   218
wenzelm@48578
   219
  \medskip Option @{verbatim "-v"} enables verbose mode.
wenzelm@48578
   220
*}
wenzelm@48578
   221
wenzelm@48578
   222
subsubsection {* Examples *}
wenzelm@48578
   223
wenzelm@48578
   224
text {*
wenzelm@48578
   225
  Build a specific logic image:
wenzelm@48578
   226
\begin{ttbox}
wenzelm@48578
   227
isabelle build -b HOLCF
wenzelm@48578
   228
\end{ttbox}
wenzelm@48578
   229
wenzelm@48578
   230
  Build the main group of logic images (as determined by the session
wenzelm@48578
   231
  ROOT specifications of the Isabelle distribution):
wenzelm@48578
   232
\begin{ttbox}
wenzelm@48578
   233
isabelle build -b -g main
wenzelm@48578
   234
\end{ttbox}
wenzelm@48578
   235
wenzelm@48578
   236
  Provide a general overview of the status of all Isabelle sessions,
wenzelm@48578
   237
  without building anything:
wenzelm@48578
   238
\begin{ttbox}
wenzelm@48578
   239
isabelle build -a -n -v
wenzelm@48578
   240
\end{ttbox}
wenzelm@48578
   241
wenzelm@48578
   242
  Build all sessions with HTML browser info and PDF document
wenzelm@48578
   243
  preparation:
wenzelm@48578
   244
\begin{ttbox}
wenzelm@48578
   245
isabelle build -a -o browser_info -o document=pdf
wenzelm@48578
   246
\end{ttbox}
wenzelm@48578
   247
wenzelm@48578
   248
  Build all sessions with a maximum of 8 prover processes and 4
wenzelm@48578
   249
  threads each (on a machine with many cores):
wenzelm@48578
   250
wenzelm@48578
   251
\begin{ttbox}
wenzelm@48578
   252
isabelle build -a -j8 -o threads=4
wenzelm@48578
   253
\end{ttbox}
wenzelm@48578
   254
*}
wenzelm@48578
   255
wenzelm@48578
   256
end