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