src/Doc/System/Sessions.thy
author haftmann
Mon Feb 06 20:56:34 2017 +0100 (2017-02-06)
changeset 64990 c6a7de505796
parent 64308 b00508facb4f
child 65374 a5b38d8d3c1e
permissions -rw-r--r--
more explicit errors in pathological cases
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@61575
     2
wenzelm@48578
     3
theory Sessions
wenzelm@48578
     4
imports Base
wenzelm@48578
     5
begin
wenzelm@48578
     6
wenzelm@58618
     7
chapter \<open>Isabelle sessions and build management \label{ch:session}\<close>
wenzelm@48584
     8
wenzelm@61575
     9
text \<open>
wenzelm@61575
    10
  An Isabelle \<^emph>\<open>session\<close> consists of a collection of related theories that may
wenzelm@61575
    11
  be associated with formal documents (\chref{ch:present}). There is also a
wenzelm@61575
    12
  notion of \<^emph>\<open>persistent heap\<close> image to capture the state of a session,
wenzelm@61575
    13
  similar to object-code in compiled programming languages. Thus the concept
wenzelm@61575
    14
  of session resembles that of a ``project'' in common IDE environments, but
wenzelm@61575
    15
  the specific name emphasizes the connection to interactive theorem proving:
wenzelm@61575
    16
  the session wraps-up the results of user-interaction with the prover in a
wenzelm@61575
    17
  persistent form.
wenzelm@48584
    18
wenzelm@61575
    19
  Application sessions are built on a given parent session, which may be built
wenzelm@61575
    20
  recursively on other parents. Following this path in the hierarchy
wenzelm@61575
    21
  eventually leads to some major object-logic session like \<open>HOL\<close>, which itself
wenzelm@61575
    22
  is based on \<open>Pure\<close> as the common root of all sessions.
wenzelm@48584
    23
wenzelm@61575
    24
  Processing sessions may take considerable time. Isabelle build management
wenzelm@61575
    25
  helps to organize this efficiently. This includes support for parallel build
wenzelm@61575
    26
  jobs, in addition to the multithreaded theory and proof checking that is
wenzelm@61575
    27
  already provided by the prover process itself.
wenzelm@61575
    28
\<close>
wenzelm@48604
    29
wenzelm@48578
    30
wenzelm@58618
    31
section \<open>Session ROOT specifications \label{sec:session-root}\<close>
wenzelm@48578
    32
wenzelm@61575
    33
text \<open>
wenzelm@61575
    34
  Session specifications reside in files called \<^verbatim>\<open>ROOT\<close> within certain
wenzelm@61575
    35
  directories, such as the home locations of registered Isabelle components or
wenzelm@61575
    36
  additional project directories given by the user.
wenzelm@48579
    37
wenzelm@61575
    38
  The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
wenzelm@61575
    39
  of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
wenzelm@61575
    40
  forms like identifiers, names, quoted strings, verbatim text, nested
wenzelm@61575
    41
  comments etc. The grammar for @{syntax session_chapter} and @{syntax
wenzelm@61575
    42
  session_entry} is given as syntax diagram below; each ROOT file may contain
wenzelm@61575
    43
  multiple specifications like this. Chapters help to organize browser info
wenzelm@61575
    44
  (\secref{sec:info}), but have no formal meaning. The default chapter is
wenzelm@61575
    45
  ``\<open>Unsorted\<close>''.
wenzelm@48579
    46
wenzelm@61575
    47
  Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
wenzelm@61575
    48
  \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
wenzelm@61575
    49
  file of that name.
wenzelm@48579
    50
wenzelm@55112
    51
  @{rail \<open>
wenzelm@51417
    52
    @{syntax_def session_chapter}: @'chapter' @{syntax name}
wenzelm@51417
    53
    ;
wenzelm@51417
    54
wenzelm@48579
    55
    @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
wenzelm@48579
    56
    ;
wenzelm@56533
    57
    body: description? options? (theories+) \<newline> files? (document_files*)
wenzelm@48579
    58
    ;
wenzelm@48738
    59
    spec: @{syntax name} groups? dir?
wenzelm@48579
    60
    ;
wenzelm@48579
    61
    groups: '(' (@{syntax name} +) ')'
wenzelm@48579
    62
    ;
wenzelm@48579
    63
    dir: @'in' @{syntax name}
wenzelm@48579
    64
    ;
wenzelm@48579
    65
    description: @'description' @{syntax text}
wenzelm@48579
    66
    ;
wenzelm@48579
    67
    options: @'options' opts
wenzelm@48579
    68
    ;
wenzelm@48605
    69
    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
wenzelm@48605
    70
    ;
wenzelm@48605
    71
    value: @{syntax name} | @{syntax real}
wenzelm@48579
    72
    ;
wenzelm@48739
    73
    theories: @'theories' opts? ( @{syntax name} * )
wenzelm@48579
    74
    ;
wenzelm@56533
    75
    files: @'files' (@{syntax name}+)
wenzelm@56533
    76
    ;
wenzelm@56533
    77
    document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
wenzelm@55112
    78
  \<close>}
wenzelm@48579
    79
wenzelm@61575
    80
  \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
wenzelm@61575
    81
  parent session \<open>B\<close>, with its content given in \<open>body\<close> (theories and auxiliary
wenzelm@61575
    82
  source files). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
wenzelm@48579
    83
  applications: only Isabelle/Pure can bootstrap itself from nothing.
wenzelm@48579
    84
wenzelm@61575
    85
  All such session specifications together describe a hierarchy (tree) of
wenzelm@61575
    86
  sessions, with globally unique names. The new session name \<open>A\<close> should be
wenzelm@61575
    87
  sufficiently long and descriptive to stand on its own in a potentially large
wenzelm@61575
    88
  library.
wenzelm@48579
    89
wenzelm@61575
    90
  \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where
wenzelm@61575
    91
  the new session is a member. Group names are uninterpreted and merely follow
wenzelm@61575
    92
  certain conventions. For example, the Isabelle distribution tags some
wenzelm@61575
    93
  important sessions by the group name called ``\<open>main\<close>''. Other projects may
wenzelm@61575
    94
  invent their own conventions, but this requires some care to avoid clashes
wenzelm@48604
    95
  within this unchecked name space.
wenzelm@48579
    96
wenzelm@61575
    97
  \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit
wenzelm@61575
    98
  directory for this session; by default this is the current directory of the
wenzelm@61575
    99
  \<^verbatim>\<open>ROOT\<close> file.
wenzelm@48579
   100
wenzelm@61575
   101
  All theories and auxiliary source files are located relatively to the
wenzelm@61575
   102
  session directory. The prover process is run within the same as its current
wenzelm@61575
   103
  working directory.
wenzelm@48579
   104
wenzelm@61575
   105
  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
wenzelm@61575
   106
  session.
wenzelm@48579
   107
wenzelm@61575
   108
  \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
wenzelm@61575
   109
  (\secref{sec:system-options}) that are used when processing this session,
wenzelm@61575
   110
  but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
wenzelm@61575
   111
  true\<close> for Boolean options.
wenzelm@61575
   112
wenzelm@61575
   113
  \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
wenzelm@61575
   114
  are processed within an environment that is augmented by the given options,
wenzelm@61575
   115
  in addition to the global session options given before. Any number of blocks
wenzelm@61575
   116
  of \isakeyword{theories} may be given. Options are only active for each
wenzelm@48604
   117
  \isakeyword{theories} block separately.
wenzelm@48579
   118
wenzelm@61575
   119
  \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
wenzelm@61575
   120
  in the processing of this session. This should cover anything outside the
wenzelm@61575
   121
  formal content of the theory sources. In contrast, files that are loaded
wenzelm@61575
   122
  formally within a theory, e.g.\ via @{command "ML_file"}, need not be
wenzelm@51055
   123
  declared again.
wenzelm@48579
   124
wenzelm@61575
   125
  \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
wenzelm@61575
   126
  source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
wenzelm@61575
   127
  {\LaTeX}. Only these explicitly given files are copied from the base
wenzelm@61575
   128
  directory to the document output directory, before formal document
wenzelm@61575
   129
  processing is started (see also \secref{sec:tool-document}). The local path
wenzelm@61575
   130
  structure of the \<open>files\<close> is preserved, which allows to reconstruct the
wenzelm@61575
   131
  original directory hierarchy of \<open>base_dir\<close>.
wenzelm@56533
   132
wenzelm@61493
   133
  \<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
wenzelm@61575
   134
  \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\
wenzelm@61575
   135
  document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the
wenzelm@61575
   136
  session root directory.
wenzelm@58618
   137
\<close>
wenzelm@48579
   138
wenzelm@51055
   139
wenzelm@58618
   140
subsubsection \<open>Examples\<close>
wenzelm@48580
   141
wenzelm@61575
   142
text \<open>
wenzelm@63680
   143
  See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
wenzelm@63680
   144
  although it uses relatively complex quasi-hierarchic naming conventions like
wenzelm@63680
   145
  \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
wenzelm@63680
   146
  names that are relatively long and descriptive, as in the Archive of Formal
wenzelm@63680
   147
  Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example.
wenzelm@61575
   148
\<close>
wenzelm@48578
   149
wenzelm@48578
   150
wenzelm@58618
   151
section \<open>System build options \label{sec:system-options}\<close>
wenzelm@48578
   152
wenzelm@61575
   153
text \<open>
wenzelm@63680
   154
  See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
wenzelm@61575
   155
  distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
wenzelm@61575
   156
  editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
wenzelm@48693
   157
wenzelm@61575
   158
  The following options are particularly relevant to build Isabelle sessions,
wenzelm@61575
   159
  in particular with document preparation (\chref{ch:present}).
wenzelm@51055
   160
wenzelm@61575
   161
    \<^item> @{system_option_def "browser_info"} controls output of HTML browser
wenzelm@61575
   162
    info, see also \secref{sec:info}.
wenzelm@51055
   163
wenzelm@61575
   164
    \<^item> @{system_option_def "document"} specifies the document output format,
wenzelm@61575
   165
    see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
wenzelm@61575
   166
    practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
wenzelm@61575
   167
    \<^verbatim>\<open>document=pdf\<close>.
wenzelm@51055
   168
wenzelm@61575
   169
    \<^item> @{system_option_def "document_output"} specifies an alternative
wenzelm@61575
   170
    directory for generated output of the document preparation system; the
wenzelm@61575
   171
    default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
wenzelm@61575
   172
    explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
wenzelm@61575
   173
    default configuration with output readily available to the author of the
wenzelm@61575
   174
    document.
wenzelm@51055
   175
wenzelm@61575
   176
    \<^item> @{system_option_def "document_variants"} specifies document variants as
wenzelm@61575
   177
    a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
wenzelm@61575
   178
    document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
wenzelm@51055
   179
wenzelm@61575
   180
    For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
wenzelm@61575
   181
    two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
wenzelm@61575
   182
    called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
wenzelm@51055
   183
wenzelm@61575
   184
    Document variant names are just a matter of conventions. It is also
wenzelm@61575
   185
    possible to use different document variant names (without tags) for
wenzelm@61575
   186
    different document root entries, see also \secref{sec:tool-document}.
wenzelm@51055
   187
wenzelm@61575
   188
    \<^item> @{system_option_def "threads"} determines the number of worker threads
wenzelm@61575
   189
    for parallel checking of theories and proofs. The default \<open>0\<close> means that a
wenzelm@61575
   190
    sensible maximum value is determined by the underlying hardware. For
wenzelm@61575
   191
    machines with many cores or with hyperthreading, this is often requires
wenzelm@61575
   192
    manual adjustment (on the command-line or within personal settings or
wenzelm@61575
   193
    preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
wenzelm@51055
   194
wenzelm@63827
   195
    \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
wenzelm@63827
   196
    space management. This is relevant for big sessions that may exhaust the
wenzelm@63827
   197
    small 32-bit address space of the ML process (which is used by default).
wenzelm@63827
   198
    When the option is enabled for some \isakeyword{theories} block, a full
wenzelm@63827
   199
    sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
wenzelm@63827
   200
    specified theories.
wenzelm@63827
   201
wenzelm@61575
   202
    \<^item> @{system_option_def "condition"} specifies a comma-separated list of
wenzelm@61575
   203
    process environment variables (or Isabelle settings) that are required for
wenzelm@61575
   204
    the subsequent theories to be processed. Conditions are considered
wenzelm@61575
   205
    ``true'' if the corresponding environment value is defined and non-empty.
wenzelm@51055
   206
wenzelm@61602
   207
    \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"}
wenzelm@61602
   208
    specify a real wall-clock timeout for the session as a whole: the two
wenzelm@61602
   209
    values are multiplied and taken as the number of seconds. Typically,
wenzelm@61602
   210
    @{system_option "timeout"} is given for individual sessions, and
wenzelm@61602
   211
    @{system_option "timeout_scale"} as global adjustment to overall hardware
wenzelm@61602
   212
    performance.
wenzelm@61602
   213
wenzelm@61602
   214
    The timer is controlled outside the ML process by the JVM that runs
wenzelm@61602
   215
    Isabelle/Scala. Thus it is relatively reliable in canceling processes that
wenzelm@61602
   216
    get out of control, even if there is a deadlock without CPU time usage.
wenzelm@51055
   217
wenzelm@64308
   218
    \<^item> @{system_option_def "profiling"} specifies a mode for global ML
wenzelm@64308
   219
    profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
wenzelm@64308
   220
    @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
wenzelm@64308
   221
    Results appear near the bottom of the session log file.
wenzelm@64308
   222
wenzelm@61575
   223
  The @{tool_def options} tool prints Isabelle system options. Its
wenzelm@48693
   224
  command-line usage is:
wenzelm@61407
   225
  @{verbatim [display]
wenzelm@61407
   226
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
wenzelm@48693
   227
wenzelm@48693
   228
  Options are:
wenzelm@48693
   229
    -b           include $ISABELLE_BUILD_OPTIONS
wenzelm@52735
   230
    -g OPTION    get value of OPTION
wenzelm@50531
   231
    -l           list options
wenzelm@48693
   232
    -x FILE      export to FILE in YXML format
wenzelm@48693
   233
wenzelm@50531
   234
  Report Isabelle system options, augmented by MORE_OPTIONS given as
wenzelm@61407
   235
  arguments NAME=VAL or NAME.\<close>}
wenzelm@48693
   236
wenzelm@61575
   237
  The command line arguments provide additional system options of the form
wenzelm@61575
   238
  \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options.
wenzelm@61575
   239
wenzelm@61575
   240
  Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones
wenzelm@61575
   241
  of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
wenzelm@48693
   242
wenzelm@61575
   243
  Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all
wenzelm@61575
   244
  options with their declaration and current value.
wenzelm@48693
   245
wenzelm@61575
   246
  Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
wenzelm@61575
   247
  of printing it in human-readable form.
wenzelm@58618
   248
\<close>
wenzelm@48578
   249
wenzelm@48578
   250
wenzelm@58618
   251
section \<open>Invoking the build process \label{sec:tool-build}\<close>
wenzelm@48578
   252
wenzelm@61575
   253
text \<open>
wenzelm@61575
   254
  The @{tool_def build} tool invokes the build process for Isabelle sessions.
wenzelm@61575
   255
  It manages dependencies between sessions, related sources of theories and
wenzelm@61575
   256
  auxiliary files, and target heap images. Accordingly, it runs instances of
wenzelm@61575
   257
  the prover process with optional document preparation. Its command-line
wenzelm@61575
   258
  usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
wenzelm@61572
   259
  \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
wenzelm@61407
   260
  @{verbatim [display]
wenzelm@61407
   261
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
wenzelm@48578
   262
wenzelm@48578
   263
  Options are:
wenzelm@48737
   264
    -D DIR       include session directory and select its sessions
wenzelm@64265
   265
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
wenzelm@49131
   266
    -R           operate on requirements of selected sessions
wenzelm@60106
   267
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@48578
   268
    -a           select all sessions
wenzelm@48578
   269
    -b           build heap images
wenzelm@48595
   270
    -c           clean build
wenzelm@48737
   271
    -d DIR       include session directory
wenzelm@48578
   272
    -g NAME      select session group NAME
wenzelm@48578
   273
    -j INT       maximum number of parallel jobs (default 1)
wenzelm@59891
   274
    -k KEYWORD   check theory sources for conflicts with proposed keywords
wenzelm@48903
   275
    -l           list session source files
wenzelm@48578
   276
    -n           no build -- test dependencies only
wenzelm@52056
   277
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@48578
   278
    -s           system build mode: produce output in ISABELLE_HOME
wenzelm@48578
   279
    -v           verbose
wenzelm@60106
   280
    -x NAME      exclude session NAME and all descendants
wenzelm@48578
   281
wenzelm@62596
   282
  Build and manage Isabelle sessions, depending on implicit settings:
wenzelm@62596
   283
wenzelm@48578
   284
  ISABELLE_BUILD_OPTIONS="..."
wenzelm@48578
   285
wenzelm@48578
   286
  ML_PLATFORM="..."
wenzelm@48578
   287
  ML_HOME="..."
wenzelm@48578
   288
  ML_SYSTEM="..."
wenzelm@61407
   289
  ML_OPTIONS="..."\<close>}
wenzelm@48578
   290
wenzelm@61406
   291
  \<^medskip>
wenzelm@61575
   292
  Isabelle sessions are defined via session ROOT files as described in
wenzelm@61575
   293
  (\secref{sec:session-root}). The totality of sessions is determined by
wenzelm@61575
   294
  collecting such specifications from all Isabelle component directories
wenzelm@61575
   295
  (\secref{sec:components}), augmented by more directories given via options
wenzelm@61575
   296
  \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session
wenzelm@61503
   297
  \<^verbatim>\<open>ROOT\<close> file with several session specifications.
wenzelm@48578
   298
wenzelm@61575
   299
  Any session root directory may refer recursively to further directories of
wenzelm@61575
   300
  the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
wenzelm@61575
   301
  helps to organize large collections of session specifications, or to make
wenzelm@61575
   302
  \<^verbatim>\<open>-d\<close> command line options persistent (say within
wenzelm@61503
   303
  \<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
wenzelm@48684
   304
wenzelm@61406
   305
  \<^medskip>
wenzelm@61575
   306
  The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close>
wenzelm@61575
   307
  given as command-line arguments, or session groups that are given via one or
wenzelm@61575
   308
  more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> selects all sessions. The build tool
wenzelm@61575
   309
  takes session dependencies into account: the set of selected sessions is
wenzelm@61575
   310
  completed by including all ancestors.
wenzelm@48578
   311
wenzelm@61406
   312
  \<^medskip>
wenzelm@61575
   313
  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
wenzelm@61575
   314
  descendents of excluded sessions are removed from the selection as specified
wenzelm@61575
   315
  above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
wenzelm@61575
   316
  specified by session group membership.
wenzelm@59892
   317
wenzelm@61406
   318
  \<^medskip>
wenzelm@61575
   319
  Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
wenzelm@61575
   320
  requirements: all ancestor sessions excluding the original selection. This
wenzelm@61575
   321
  allows to prepare the stage for some build process with different options,
wenzelm@61575
   322
  before running the main build itself (without option \<^verbatim>\<open>-R\<close>).
wenzelm@49131
   323
wenzelm@61406
   324
  \<^medskip>
wenzelm@61575
   325
  Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined
wenzelm@61575
   326
  in the given directories.
wenzelm@48737
   327
wenzelm@61406
   328
  \<^medskip>
wenzelm@61406
   329
  The build process depends on additional options
wenzelm@61575
   330
  (\secref{sec:system-options}) that are passed to the prover eventually. The
wenzelm@61575
   331
  settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
wenzelm@61602
   332
  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
wenzelm@61602
   333
  Moreover, the environment of system build options may be augmented on the
wenzelm@61602
   334
  command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which abbreviates
wenzelm@61602
   335
  \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
wenzelm@61602
   336
  the command-line are applied in the given order.
wenzelm@48578
   337
wenzelm@61406
   338
  \<^medskip>
wenzelm@61575
   339
  Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
wenzelm@61575
   340
  sessions. By default, images are only saved for inner nodes of the hierarchy
wenzelm@61575
   341
  of sessions, as required for other sessions to continue later on.
wenzelm@48578
   342
wenzelm@61406
   343
  \<^medskip>
wenzelm@61575
   344
  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
wenzelm@61575
   345
  performing the specified build operation.
wenzelm@48595
   346
wenzelm@61406
   347
  \<^medskip>
wenzelm@61575
   348
  Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
wenzelm@61575
   349
  (including optional cleanup). Note that the return code always indicates the
wenzelm@61575
   350
  status of the set of selected sessions.
wenzelm@48595
   351
wenzelm@61406
   352
  \<^medskip>
wenzelm@61575
   353
  Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
wenzelm@61575
   354
  processes). Each prover process is subject to a separate limit of parallel
wenzelm@61575
   355
  worker threads, cf.\ system option @{system_option_ref threads}.
wenzelm@48578
   356
wenzelm@61406
   357
  \<^medskip>
wenzelm@64265
   358
  Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
wenzelm@64265
   359
  performance tuning on Linux servers with separate CPU/memory modules.
wenzelm@64265
   360
wenzelm@64265
   361
  \<^medskip>
wenzelm@61575
   362
  Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
wenzelm@63669
   363
  and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
wenzelm@63669
   364
  default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting
wenzelm@63669
   365
  ISABELLE_HOME_USER}, i.e.\ the user's home directory).
wenzelm@48578
   366
wenzelm@61406
   367
  \<^medskip>
wenzelm@61575
   368
  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
wenzelm@61575
   369
  the source files that contribute to a session.
wenzelm@59891
   370
wenzelm@61406
   371
  \<^medskip>
wenzelm@61575
   372
  Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
wenzelm@61575
   373
  uses allowed). The theory sources are checked for conflicts wrt.\ this
wenzelm@61575
   374
  hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
wenzelm@61575
   375
  that need to be quoted.
wenzelm@61575
   376
\<close>
wenzelm@59891
   377
wenzelm@48578
   378
wenzelm@58618
   379
subsubsection \<open>Examples\<close>
wenzelm@48578
   380
wenzelm@58618
   381
text \<open>
wenzelm@48578
   382
  Build a specific logic image:
wenzelm@61407
   383
  @{verbatim [display] \<open>isabelle build -b HOLCF\<close>}
wenzelm@48578
   384
wenzelm@61406
   385
  \<^smallskip>
wenzelm@61406
   386
  Build the main group of logic images:
wenzelm@61407
   387
  @{verbatim [display] \<open>isabelle build -b -g main\<close>}
wenzelm@48578
   388
wenzelm@61406
   389
  \<^smallskip>
wenzelm@61575
   390
  Provide a general overview of the status of all Isabelle sessions, without
wenzelm@61575
   391
  building anything:
wenzelm@61407
   392
  @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
wenzelm@48578
   393
wenzelm@61406
   394
  \<^smallskip>
wenzelm@61575
   395
  Build all sessions with HTML browser info and PDF document preparation:
wenzelm@61407
   396
  @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
wenzelm@48578
   397
wenzelm@61406
   398
  \<^smallskip>
wenzelm@61575
   399
  Build all sessions with a maximum of 8 parallel prover processes and 4
wenzelm@61575
   400
  worker threads each (on a machine with many cores):
wenzelm@61407
   401
  @{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
wenzelm@48595
   402
wenzelm@61406
   403
  \<^smallskip>
wenzelm@61575
   404
  Build some session images with cleanup of their descendants, while retaining
wenzelm@61575
   405
  their ancestry:
wenzelm@61407
   406
  @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
wenzelm@48595
   407
wenzelm@61406
   408
  \<^smallskip>
wenzelm@61406
   409
  Clean all sessions without building anything:
wenzelm@61407
   410
  @{verbatim [display] \<open>isabelle build -a -n -c\<close>}
wenzelm@48737
   411
wenzelm@61406
   412
  \<^smallskip>
wenzelm@61575
   413
  Build all sessions from some other directory hierarchy, according to the
wenzelm@61575
   414
  settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle
wenzelm@61575
   415
  environment:
wenzelm@61407
   416
  @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
wenzelm@49131
   417
wenzelm@61406
   418
  \<^smallskip>
wenzelm@61575
   419
  Inform about the status of all sessions required for AFP, without building
wenzelm@61575
   420
  anything yet:
wenzelm@61407
   421
  @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
wenzelm@58618
   422
\<close>
wenzelm@48578
   423
wenzelm@48578
   424
end