src/Doc/System/Sessions.thy
author wenzelm
Wed Jan 16 17:55:26 2019 +0100 (10 months ago)
changeset 69671 2486792eaf61
parent 69610 10644973cdde
child 69755 2fc85ce1f557
permissions -rw-r--r--
support pruning of export names;
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@69593
    51
  \<^rail>\<open>
wenzelm@51417
    52
    @{syntax_def session_chapter}: @'chapter' @{syntax name}
wenzelm@51417
    53
    ;
wenzelm@51417
    54
wenzelm@66971
    55
    @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
wenzelm@66971
    56
      (@{syntax system_name} '+')? description? options? \<newline>
wenzelm@68292
    57
      (sessions?) (theories*) (document_files*) \<newline> (export_files*)
wenzelm@48579
    58
    ;
wenzelm@48579
    59
    groups: '(' (@{syntax name} +) ')'
wenzelm@48579
    60
    ;
wenzelm@68808
    61
    dir: @'in' @{syntax embedded}
wenzelm@48579
    62
    ;
wenzelm@48579
    63
    description: @'description' @{syntax text}
wenzelm@48579
    64
    ;
wenzelm@48579
    65
    options: @'options' opts
wenzelm@48579
    66
    ;
wenzelm@48605
    67
    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
wenzelm@48605
    68
    ;
wenzelm@48605
    69
    value: @{syntax name} | @{syntax real}
wenzelm@48579
    70
    ;
wenzelm@66916
    71
    sessions: @'sessions' (@{syntax system_name}+)
wenzelm@65374
    72
    ;
wenzelm@66970
    73
    theories: @'theories' opts? (theory_entry+)
wenzelm@48579
    74
    ;
wenzelm@66916
    75
    theory_entry: @{syntax system_name} ('(' @'global' ')')?
wenzelm@65504
    76
    ;
wenzelm@68808
    77
    document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+)
wenzelm@68292
    78
    ;
wenzelm@69671
    79
    export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline>
wenzelm@69671
    80
      (@{syntax embedded}+)
wenzelm@69593
    81
  \<close>
wenzelm@48579
    82
wenzelm@61575
    83
  \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
wenzelm@66759
    84
  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and
wenzelm@66759
    85
  theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
wenzelm@66759
    86
  applications: only Isabelle/Pure can bootstrap itself from nothing.
wenzelm@48579
    87
wenzelm@65504
    88
  All such session specifications together describe a hierarchy (graph) of
wenzelm@61575
    89
  sessions, with globally unique names. The new session name \<open>A\<close> should be
wenzelm@61575
    90
  sufficiently long and descriptive to stand on its own in a potentially large
wenzelm@61575
    91
  library.
wenzelm@48579
    92
wenzelm@61575
    93
  \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where
wenzelm@61575
    94
  the new session is a member. Group names are uninterpreted and merely follow
wenzelm@61575
    95
  certain conventions. For example, the Isabelle distribution tags some
wenzelm@61575
    96
  important sessions by the group name called ``\<open>main\<close>''. Other projects may
wenzelm@61575
    97
  invent their own conventions, but this requires some care to avoid clashes
wenzelm@48604
    98
  within this unchecked name space.
wenzelm@48579
    99
wenzelm@61575
   100
  \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit
wenzelm@61575
   101
  directory for this session; by default this is the current directory of the
wenzelm@61575
   102
  \<^verbatim>\<open>ROOT\<close> file.
wenzelm@48579
   103
wenzelm@66759
   104
  All theory files are located relatively to the session directory. The prover
wenzelm@66759
   105
  process is run within the same as its current working directory.
wenzelm@48579
   106
wenzelm@61575
   107
  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
wenzelm@61575
   108
  session.
wenzelm@48579
   109
wenzelm@61575
   110
  \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
wenzelm@61575
   111
  (\secref{sec:system-options}) that are used when processing this session,
wenzelm@61575
   112
  but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
wenzelm@61575
   113
  true\<close> for Boolean options.
wenzelm@61575
   114
wenzelm@65504
   115
  \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
wenzelm@65504
   116
  the current name space of theories. This allows to refer to a theory \<open>A\<close>
wenzelm@65504
   117
  from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again
wenzelm@65504
   118
  into the current ML process, which is in contrast to a theory that is
wenzelm@65504
   119
  already present in the \<^emph>\<open>parent\<close> session.
wenzelm@65504
   120
wenzelm@65505
   121
  Theories that are imported from other sessions are excluded from the current
wenzelm@65505
   122
  session document.
wenzelm@65505
   123
wenzelm@61575
   124
  \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
wenzelm@61575
   125
  are processed within an environment that is augmented by the given options,
wenzelm@61575
   126
  in addition to the global session options given before. Any number of blocks
wenzelm@61575
   127
  of \isakeyword{theories} may be given. Options are only active for each
wenzelm@48604
   128
  \isakeyword{theories} block separately.
wenzelm@48579
   129
wenzelm@65374
   130
  A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
wenzelm@66993
   131
  literally in other session specifications or theory imports --- the normal
wenzelm@66993
   132
  situation is to qualify theory names by the session name; this ensures
wenzelm@66993
   133
  globally unique names in big session graphs. Global theories are usually the
wenzelm@66993
   134
  entry points to major logic sessions: \<open>Pure\<close>, \<open>Main\<close>, \<open>Complex_Main\<close>,
wenzelm@66993
   135
  \<open>HOLCF\<close>, \<open>IFOL\<close>, \<open>FOL\<close>, \<open>ZF\<close>, \<open>ZFC\<close> etc. Regular Isabelle applications
wenzelm@66993
   136
  should not claim any global theory names.
wenzelm@65374
   137
wenzelm@61575
   138
  \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
wenzelm@61575
   139
  source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
wenzelm@61575
   140
  {\LaTeX}. Only these explicitly given files are copied from the base
wenzelm@61575
   141
  directory to the document output directory, before formal document
wenzelm@61575
   142
  processing is started (see also \secref{sec:tool-document}). The local path
wenzelm@61575
   143
  structure of the \<open>files\<close> is preserved, which allows to reconstruct the
wenzelm@68292
   144
  original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is
wenzelm@68292
   145
  \<^verbatim>\<open>document\<close> within the session root directory.
wenzelm@56533
   146
wenzelm@69671
   147
  \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number]
wenzelm@69671
   148
  patterns\<close> writes theory exports to the file-system: the \<open>target_dir\<close>
wenzelm@69671
   149
  specification is relative to the session root directory; its default is
wenzelm@69671
   150
  \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref export}
wenzelm@69671
   151
  (\secref{sec:tool-export}). The number given in brackets (default: 0)
wenzelm@69671
   152
  specifies elements that should be pruned from each name: it allows to reduce
wenzelm@69671
   153
  the resulting directory hierarchy at the danger of overwriting files due to
wenzelm@69671
   154
  loss of uniqueness.
wenzelm@58618
   155
\<close>
wenzelm@48579
   156
wenzelm@51055
   157
wenzelm@58618
   158
subsubsection \<open>Examples\<close>
wenzelm@48580
   159
wenzelm@61575
   160
text \<open>
wenzelm@63680
   161
  See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
wenzelm@63680
   162
  although it uses relatively complex quasi-hierarchic naming conventions like
wenzelm@63680
   163
  \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
wenzelm@63680
   164
  names that are relatively long and descriptive, as in the Archive of Formal
lars@67605
   165
  Proofs (\<^url>\<open>https://isa-afp.org\<close>), for example.
wenzelm@61575
   166
\<close>
wenzelm@48578
   167
wenzelm@48578
   168
wenzelm@58618
   169
section \<open>System build options \label{sec:system-options}\<close>
wenzelm@48578
   170
wenzelm@61575
   171
text \<open>
wenzelm@63680
   172
  See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
wenzelm@61575
   173
  distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
wenzelm@61575
   174
  editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
wenzelm@48693
   175
wenzelm@61575
   176
  The following options are particularly relevant to build Isabelle sessions,
wenzelm@61575
   177
  in particular with document preparation (\chref{ch:present}).
wenzelm@51055
   178
wenzelm@61575
   179
    \<^item> @{system_option_def "browser_info"} controls output of HTML browser
wenzelm@61575
   180
    info, see also \secref{sec:info}.
wenzelm@51055
   181
wenzelm@61575
   182
    \<^item> @{system_option_def "document"} specifies the document output format,
wenzelm@61575
   183
    see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
wenzelm@61575
   184
    practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
wenzelm@61575
   185
    \<^verbatim>\<open>document=pdf\<close>.
wenzelm@51055
   186
wenzelm@61575
   187
    \<^item> @{system_option_def "document_output"} specifies an alternative
wenzelm@61575
   188
    directory for generated output of the document preparation system; the
wenzelm@61575
   189
    default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
wenzelm@61575
   190
    explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
wenzelm@61575
   191
    default configuration with output readily available to the author of the
wenzelm@61575
   192
    document.
wenzelm@51055
   193
wenzelm@61575
   194
    \<^item> @{system_option_def "document_variants"} specifies document variants as
wenzelm@61575
   195
    a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
wenzelm@61575
   196
    document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
wenzelm@51055
   197
wenzelm@61575
   198
    For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
wenzelm@61575
   199
    two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
wenzelm@61575
   200
    called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
wenzelm@51055
   201
wenzelm@61575
   202
    Document variant names are just a matter of conventions. It is also
wenzelm@61575
   203
    possible to use different document variant names (without tags) for
wenzelm@61575
   204
    different document root entries, see also \secref{sec:tool-document}.
wenzelm@51055
   205
wenzelm@68513
   206
    \<^item> @{system_option_def "document_tags"} specifies alternative command tags
wenzelm@68513
   207
    as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a
wenzelm@68513
   208
    specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other commands. This
wenzelm@68513
   209
    is occasionally useful to control the global visibility of commands via
wenzelm@68513
   210
    session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>).
wenzelm@67140
   211
wenzelm@61575
   212
    \<^item> @{system_option_def "threads"} determines the number of worker threads
wenzelm@61575
   213
    for parallel checking of theories and proofs. The default \<open>0\<close> means that a
wenzelm@61575
   214
    sensible maximum value is determined by the underlying hardware. For
wenzelm@61575
   215
    machines with many cores or with hyperthreading, this is often requires
wenzelm@61575
   216
    manual adjustment (on the command-line or within personal settings or
wenzelm@61575
   217
    preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
wenzelm@51055
   218
wenzelm@63827
   219
    \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
wenzelm@63827
   220
    space management. This is relevant for big sessions that may exhaust the
wenzelm@63827
   221
    small 32-bit address space of the ML process (which is used by default).
wenzelm@63827
   222
    When the option is enabled for some \isakeyword{theories} block, a full
wenzelm@63827
   223
    sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
wenzelm@63827
   224
    specified theories.
wenzelm@63827
   225
wenzelm@61575
   226
    \<^item> @{system_option_def "condition"} specifies a comma-separated list of
wenzelm@61575
   227
    process environment variables (or Isabelle settings) that are required for
wenzelm@61575
   228
    the subsequent theories to be processed. Conditions are considered
wenzelm@61575
   229
    ``true'' if the corresponding environment value is defined and non-empty.
wenzelm@51055
   230
wenzelm@61602
   231
    \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"}
wenzelm@61602
   232
    specify a real wall-clock timeout for the session as a whole: the two
wenzelm@61602
   233
    values are multiplied and taken as the number of seconds. Typically,
wenzelm@61602
   234
    @{system_option "timeout"} is given for individual sessions, and
wenzelm@61602
   235
    @{system_option "timeout_scale"} as global adjustment to overall hardware
wenzelm@61602
   236
    performance.
wenzelm@61602
   237
wenzelm@61602
   238
    The timer is controlled outside the ML process by the JVM that runs
wenzelm@61602
   239
    Isabelle/Scala. Thus it is relatively reliable in canceling processes that
wenzelm@61602
   240
    get out of control, even if there is a deadlock without CPU time usage.
wenzelm@51055
   241
wenzelm@64308
   242
    \<^item> @{system_option_def "profiling"} specifies a mode for global ML
wenzelm@64308
   243
    profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
wenzelm@69593
   244
    \<^ML>\<open>profile_time\<close> and \<^verbatim>\<open>allocations\<close> for \<^ML>\<open>profile_allocations\<close>.
wenzelm@64308
   245
    Results appear near the bottom of the session log file.
wenzelm@64308
   246
wenzelm@61575
   247
  The @{tool_def options} tool prints Isabelle system options. Its
wenzelm@48693
   248
  command-line usage is:
wenzelm@61407
   249
  @{verbatim [display]
wenzelm@61407
   250
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
wenzelm@48693
   251
wenzelm@48693
   252
  Options are:
wenzelm@48693
   253
    -b           include $ISABELLE_BUILD_OPTIONS
wenzelm@52735
   254
    -g OPTION    get value of OPTION
wenzelm@50531
   255
    -l           list options
wenzelm@48693
   256
    -x FILE      export to FILE in YXML format
wenzelm@48693
   257
wenzelm@50531
   258
  Report Isabelle system options, augmented by MORE_OPTIONS given as
wenzelm@61407
   259
  arguments NAME=VAL or NAME.\<close>}
wenzelm@48693
   260
wenzelm@61575
   261
  The command line arguments provide additional system options of the form
wenzelm@61575
   262
  \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options.
wenzelm@61575
   263
wenzelm@61575
   264
  Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones
wenzelm@61575
   265
  of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
wenzelm@48693
   266
wenzelm@61575
   267
  Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all
wenzelm@61575
   268
  options with their declaration and current value.
wenzelm@48693
   269
wenzelm@61575
   270
  Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
wenzelm@61575
   271
  of printing it in human-readable form.
wenzelm@58618
   272
\<close>
wenzelm@48578
   273
wenzelm@48578
   274
wenzelm@58618
   275
section \<open>Invoking the build process \label{sec:tool-build}\<close>
wenzelm@48578
   276
wenzelm@61575
   277
text \<open>
wenzelm@61575
   278
  The @{tool_def build} tool invokes the build process for Isabelle sessions.
wenzelm@61575
   279
  It manages dependencies between sessions, related sources of theories and
wenzelm@61575
   280
  auxiliary files, and target heap images. Accordingly, it runs instances of
wenzelm@61575
   281
  the prover process with optional document preparation. Its command-line
wenzelm@61575
   282
  usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
wenzelm@61572
   283
  \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
wenzelm@61407
   284
  @{verbatim [display]
wenzelm@61407
   285
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
wenzelm@48578
   286
wenzelm@48578
   287
  Options are:
wenzelm@66737
   288
    -B NAME      include session NAME and all descendants
wenzelm@48737
   289
    -D DIR       include session directory and select its sessions
wenzelm@64265
   290
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
wenzelm@49131
   291
    -R           operate on requirements of selected sessions
wenzelm@66745
   292
    -S           soft build: only observe changes of sources, not heap images
wenzelm@60106
   293
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@48578
   294
    -a           select all sessions
wenzelm@48578
   295
    -b           build heap images
wenzelm@48595
   296
    -c           clean build
wenzelm@48737
   297
    -d DIR       include session directory
wenzelm@66841
   298
    -f           fresh build
wenzelm@48578
   299
    -g NAME      select session group NAME
wenzelm@48578
   300
    -j INT       maximum number of parallel jobs (default 1)
wenzelm@59891
   301
    -k KEYWORD   check theory sources for conflicts with proposed keywords
wenzelm@48903
   302
    -l           list session source files
wenzelm@48578
   303
    -n           no build -- test dependencies only
wenzelm@52056
   304
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@48578
   305
    -s           system build mode: produce output in ISABELLE_HOME
wenzelm@48578
   306
    -v           verbose
wenzelm@60106
   307
    -x NAME      exclude session NAME and all descendants
wenzelm@48578
   308
wenzelm@62596
   309
  Build and manage Isabelle sessions, depending on implicit settings:
wenzelm@62596
   310
wenzelm@48578
   311
  ISABELLE_BUILD_OPTIONS="..."
wenzelm@48578
   312
wenzelm@48578
   313
  ML_PLATFORM="..."
wenzelm@48578
   314
  ML_HOME="..."
wenzelm@48578
   315
  ML_SYSTEM="..."
wenzelm@61407
   316
  ML_OPTIONS="..."\<close>}
wenzelm@48578
   317
wenzelm@61406
   318
  \<^medskip>
wenzelm@61575
   319
  Isabelle sessions are defined via session ROOT files as described in
wenzelm@61575
   320
  (\secref{sec:session-root}). The totality of sessions is determined by
wenzelm@61575
   321
  collecting such specifications from all Isabelle component directories
wenzelm@61575
   322
  (\secref{sec:components}), augmented by more directories given via options
wenzelm@61575
   323
  \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session
wenzelm@61503
   324
  \<^verbatim>\<open>ROOT\<close> file with several session specifications.
wenzelm@48578
   325
wenzelm@61575
   326
  Any session root directory may refer recursively to further directories of
wenzelm@61575
   327
  the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
wenzelm@61575
   328
  helps to organize large collections of session specifications, or to make
wenzelm@66576
   329
  \<^verbatim>\<open>-d\<close> command line options persistent (e.g.\ in
wenzelm@61503
   330
  \<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
wenzelm@48684
   331
wenzelm@61406
   332
  \<^medskip>
wenzelm@61575
   333
  The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close>
wenzelm@61575
   334
  given as command-line arguments, or session groups that are given via one or
wenzelm@61575
   335
  more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> selects all sessions. The build tool
wenzelm@61575
   336
  takes session dependencies into account: the set of selected sessions is
wenzelm@61575
   337
  completed by including all ancestors.
wenzelm@48578
   338
wenzelm@61406
   339
  \<^medskip>
wenzelm@68734
   340
  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions to be included (all
wenzelm@68734
   341
  descendants wrt.\ the session parent or import graph).
wenzelm@66737
   342
wenzelm@66737
   343
  \<^medskip>
wenzelm@68734
   344
  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded (all
wenzelm@68734
   345
  descendants wrt.\ the session parent or import graph). Option \<^verbatim>\<open>-X\<close> is
wenzelm@68734
   346
  analogous to this, but excluded sessions are specified by session group
wenzelm@68734
   347
  membership.
wenzelm@59892
   348
wenzelm@61406
   349
  \<^medskip>
wenzelm@61575
   350
  Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
wenzelm@61575
   351
  requirements: all ancestor sessions excluding the original selection. This
wenzelm@61575
   352
  allows to prepare the stage for some build process with different options,
wenzelm@61575
   353
  before running the main build itself (without option \<^verbatim>\<open>-R\<close>).
wenzelm@49131
   354
wenzelm@61406
   355
  \<^medskip>
wenzelm@61575
   356
  Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined
wenzelm@61575
   357
  in the given directories.
wenzelm@48737
   358
wenzelm@61406
   359
  \<^medskip>
wenzelm@66745
   360
  Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to
wenzelm@66745
   361
  those sessions that have changed sources (according to actually imported
wenzelm@66745
   362
  theories). The status of heap images is ignored.
wenzelm@66745
   363
wenzelm@66745
   364
  \<^medskip>
wenzelm@61406
   365
  The build process depends on additional options
wenzelm@61575
   366
  (\secref{sec:system-options}) that are passed to the prover eventually. The
wenzelm@61575
   367
  settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
wenzelm@61602
   368
  additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
wenzelm@61602
   369
  Moreover, the environment of system build options may be augmented on the
wenzelm@61602
   370
  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
   371
  \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
wenzelm@61602
   372
  the command-line are applied in the given order.
wenzelm@48578
   373
wenzelm@61406
   374
  \<^medskip>
wenzelm@61575
   375
  Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
wenzelm@61575
   376
  sessions. By default, images are only saved for inner nodes of the hierarchy
wenzelm@61575
   377
  of sessions, as required for other sessions to continue later on.
wenzelm@48578
   378
wenzelm@61406
   379
  \<^medskip>
wenzelm@68734
   380
  Option \<^verbatim>\<open>-c\<close> cleans the selected sessions (all descendants wrt.\ the session
wenzelm@68734
   381
  parent or import graph) before performing the specified build operation.
wenzelm@48595
   382
wenzelm@61406
   383
  \<^medskip>
wenzelm@66841
   384
  Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
wenzelm@66841
   385
  requirements.
wenzelm@66841
   386
wenzelm@66841
   387
  \<^medskip>
wenzelm@61575
   388
  Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
wenzelm@61575
   389
  (including optional cleanup). Note that the return code always indicates the
wenzelm@61575
   390
  status of the set of selected sessions.
wenzelm@48595
   391
wenzelm@61406
   392
  \<^medskip>
wenzelm@61575
   393
  Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
wenzelm@61575
   394
  processes). Each prover process is subject to a separate limit of parallel
wenzelm@61575
   395
  worker threads, cf.\ system option @{system_option_ref threads}.
wenzelm@48578
   396
wenzelm@61406
   397
  \<^medskip>
wenzelm@64265
   398
  Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
wenzelm@64265
   399
  performance tuning on Linux servers with separate CPU/memory modules.
wenzelm@64265
   400
wenzelm@64265
   401
  \<^medskip>
wenzelm@68523
   402
  Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that session images are
wenzelm@69593
   403
  stored in \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> instead of \<^path>\<open>$ISABELLE_HEAPS\<close>.
wenzelm@48578
   404
wenzelm@61406
   405
  \<^medskip>
wenzelm@61575
   406
  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
wenzelm@61575
   407
  the source files that contribute to a session.
wenzelm@59891
   408
wenzelm@61406
   409
  \<^medskip>
wenzelm@61575
   410
  Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
wenzelm@61575
   411
  uses allowed). The theory sources are checked for conflicts wrt.\ this
wenzelm@61575
   412
  hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
wenzelm@61575
   413
  that need to be quoted.
wenzelm@61575
   414
\<close>
wenzelm@59891
   415
wenzelm@48578
   416
wenzelm@58618
   417
subsubsection \<open>Examples\<close>
wenzelm@48578
   418
wenzelm@58618
   419
text \<open>
wenzelm@48578
   420
  Build a specific logic image:
wenzelm@61407
   421
  @{verbatim [display] \<open>isabelle build -b HOLCF\<close>}
wenzelm@48578
   422
wenzelm@61406
   423
  \<^smallskip>
wenzelm@61406
   424
  Build the main group of logic images:
wenzelm@61407
   425
  @{verbatim [display] \<open>isabelle build -b -g main\<close>}
wenzelm@48578
   426
wenzelm@61406
   427
  \<^smallskip>
wenzelm@66748
   428
  Build all descendants (and requirements) of \<^verbatim>\<open>FOL\<close> and \<^verbatim>\<open>ZF\<close>:
wenzelm@66748
   429
  @{verbatim [display] \<open>isabelle build -B FOL -B ZF\<close>}
wenzelm@66748
   430
wenzelm@66748
   431
  \<^smallskip>
wenzelm@66748
   432
  Build all sessions where sources have changed (ignoring heaps):
wenzelm@66748
   433
  @{verbatim [display] \<open>isabelle build -a -S\<close>}
wenzelm@66748
   434
wenzelm@66748
   435
  \<^smallskip>
wenzelm@61575
   436
  Provide a general overview of the status of all Isabelle sessions, without
wenzelm@61575
   437
  building anything:
wenzelm@61407
   438
  @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
wenzelm@48578
   439
wenzelm@61406
   440
  \<^smallskip>
wenzelm@61575
   441
  Build all sessions with HTML browser info and PDF document preparation:
wenzelm@61407
   442
  @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
wenzelm@48578
   443
wenzelm@61406
   444
  \<^smallskip>
wenzelm@61575
   445
  Build all sessions with a maximum of 8 parallel prover processes and 4
wenzelm@61575
   446
  worker threads each (on a machine with many cores):
wenzelm@61407
   447
  @{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
wenzelm@48595
   448
wenzelm@61406
   449
  \<^smallskip>
wenzelm@61575
   450
  Build some session images with cleanup of their descendants, while retaining
wenzelm@61575
   451
  their ancestry:
wenzelm@61407
   452
  @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
wenzelm@48595
   453
wenzelm@61406
   454
  \<^smallskip>
wenzelm@61406
   455
  Clean all sessions without building anything:
wenzelm@61407
   456
  @{verbatim [display] \<open>isabelle build -a -n -c\<close>}
wenzelm@48737
   457
wenzelm@61406
   458
  \<^smallskip>
wenzelm@61575
   459
  Build all sessions from some other directory hierarchy, according to the
wenzelm@61575
   460
  settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle
wenzelm@61575
   461
  environment:
wenzelm@61407
   462
  @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
wenzelm@49131
   463
wenzelm@61406
   464
  \<^smallskip>
wenzelm@61575
   465
  Inform about the status of all sessions required for AFP, without building
wenzelm@61575
   466
  anything yet:
wenzelm@61407
   467
  @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
wenzelm@58618
   468
\<close>
wenzelm@48578
   469
wenzelm@66671
   470
wenzelm@66671
   471
section \<open>Maintain theory imports wrt.\ session structure\<close>
wenzelm@66671
   472
wenzelm@66671
   473
text \<open>
wenzelm@66671
   474
  The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
wenzelm@66671
   475
  session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
wenzelm@66671
   476
  \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
wenzelm@66671
   477
\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
wenzelm@66671
   478
wenzelm@66671
   479
  Options are:
wenzelm@66737
   480
    -B NAME      include session NAME and all descendants
wenzelm@66671
   481
    -D DIR       include session directory and select its sessions
wenzelm@66851
   482
    -I           operation: report session imports
wenzelm@66671
   483
    -M           operation: Mercurial repository check for theory files
wenzelm@66671
   484
    -R           operate on requirements of selected sessions
wenzelm@66671
   485
    -U           operation: update theory imports to use session qualifiers
wenzelm@66671
   486
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@66671
   487
    -a           select all sessions
wenzelm@66671
   488
    -d DIR       include session directory
wenzelm@66671
   489
    -g NAME      select session group NAME
wenzelm@66671
   490
    -i           incremental update according to session graph structure
wenzelm@66671
   491
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@66671
   492
    -v           verbose
wenzelm@66671
   493
    -x NAME      exclude session NAME and all descendants
wenzelm@66671
   494
wenzelm@66671
   495
  Maintain theory imports wrt. session structure. At least one operation
wenzelm@66671
   496
  needs to be specified (see options -I -M -U).\<close>}
wenzelm@66671
   497
wenzelm@66671
   498
  \<^medskip>
wenzelm@66671
   499
  The selection of sessions and session directories works as for @{tool build}
wenzelm@66737
   500
  via options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
wenzelm@66671
   501
  \secref{sec:tool-build}).
wenzelm@66671
   502
wenzelm@66671
   503
  \<^medskip>
wenzelm@66671
   504
  Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
wenzelm@66671
   505
  (see \secref{sec:tool-build}).
wenzelm@66671
   506
wenzelm@66671
   507
  \<^medskip>
wenzelm@66671
   508
  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
wenzelm@66671
   509
wenzelm@66671
   510
  \<^medskip>
wenzelm@66851
   511
  Option \<^verbatim>\<open>-I\<close> determines reports session imports:
wenzelm@66851
   512
wenzelm@66851
   513
    \<^descr>[Potential session imports] are derived from old-style use of theory
wenzelm@66851
   514
    files from other sessions via the directory structure. After declaring
wenzelm@66851
   515
    those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
wenzelm@66851
   516
    proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
wenzelm@66851
   517
    example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
wenzelm@66851
   518
    \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
wenzelm@66851
   519
    \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
wenzelm@66851
   520
wenzelm@66851
   521
    \<^descr>[Actual session imports] are derived from the session qualifiers of all
wenzelm@66851
   522
    currently imported theories. This helps to minimize dependencies in the
wenzelm@66851
   523
    session import structure to what is actually required.
wenzelm@66671
   524
wenzelm@66671
   525
  \<^medskip>
wenzelm@66671
   526
  Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
wenzelm@66671
   527
  the underlying session directories; non-repository directories are ignored.
wenzelm@66671
   528
  This helps to find files that are accidentally ignored, e.g.\ due to
wenzelm@66671
   529
  rearrangements of the session structure.
wenzelm@66671
   530
wenzelm@66671
   531
  \<^medskip>
wenzelm@66671
   532
  Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
wenzelm@66671
   533
  to canonical session-qualified theory names, according to the theory name
wenzelm@66671
   534
  space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
wenzelm@66671
   535
wenzelm@66671
   536
  Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
wenzelm@66671
   537
  following to the session graph structure in bottom-up order. This may
wenzelm@66671
   538
  lead to more accurate results in complex session hierarchies.
wenzelm@66671
   539
\<close>
wenzelm@66671
   540
wenzelm@66671
   541
subsubsection \<open>Examples\<close>
wenzelm@66671
   542
wenzelm@66671
   543
text \<open>
wenzelm@66671
   544
  Determine potential session imports for some project directory:
wenzelm@66671
   545
  @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
wenzelm@66671
   546
wenzelm@66671
   547
  \<^smallskip>
wenzelm@66671
   548
  Mercurial repository check for some project directory:
wenzelm@66671
   549
  @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
wenzelm@66671
   550
wenzelm@66671
   551
  \<^smallskip>
wenzelm@66671
   552
  Incremental update of theory imports for some project directory:
wenzelm@66671
   553
  @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
wenzelm@66671
   554
\<close>
wenzelm@66671
   555
wenzelm@68116
   556
wenzelm@68152
   557
section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
wenzelm@68116
   558
wenzelm@68116
   559
text \<open>
wenzelm@68116
   560
  The @{tool_def "export"} tool retrieves theory exports from the session
wenzelm@68116
   561
  database. Its command-line usage is: @{verbatim [display]
wenzelm@68116
   562
\<open>Usage: isabelle export [OPTIONS] SESSION
wenzelm@68116
   563
wenzelm@68116
   564
  Options are:
wenzelm@68314
   565
    -O DIR       output directory for exported files (default: "export")
wenzelm@68116
   566
    -d DIR       include session directory
wenzelm@68116
   567
    -l           list exports
wenzelm@68116
   568
    -n           no build of session
wenzelm@68116
   569
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@69671
   570
    -p NUM       prune path of exported files by NUM elements
wenzelm@68116
   571
    -s           system build mode for session image
wenzelm@68514
   572
    -x PATTERN   extract files matching pattern (e.g.\ "*:**" for all)
wenzelm@68116
   573
wenzelm@68116
   574
  List or export theory exports for SESSION: named blobs produced by
wenzelm@68290
   575
  isabelle build. Option -l or -x is required; option -x may be repeated.
wenzelm@68116
   576
wenzelm@68116
   577
  The PATTERN language resembles glob patterns in the shell, with ? and *
wenzelm@68116
   578
  (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
wenzelm@68116
   579
  and variants {pattern1,pattern2,pattern3}.\<close>}
wenzelm@68116
   580
wenzelm@68116
   581
  \<^medskip>
wenzelm@68116
   582
  The specified session is updated via @{tool build}
wenzelm@68116
   583
  (\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close>. The
wenzelm@68116
   584
  option \<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a
wenzelm@68116
   585
  potentially outdated session database is used!
wenzelm@68116
   586
wenzelm@68116
   587
  \<^medskip>
wenzelm@68116
   588
  Option \<^verbatim>\<open>-l\<close> lists all stored exports, with compound names
wenzelm@68116
   589
  \<open>theory\<close>\<^verbatim>\<open>:\<close>\<open>name\<close>.
wenzelm@68116
   590
wenzelm@68116
   591
  \<^medskip>
wenzelm@68116
   592
  Option \<^verbatim>\<open>-x\<close> extracts stored exports whose compound name matches the given
wenzelm@68116
   593
  pattern. Note that wild cards ``\<^verbatim>\<open>?\<close>'' and ``\<^verbatim>\<open>*\<close>'' do not match the
wenzelm@68116
   594
  separators ``\<^verbatim>\<open>:\<close>'' and ``\<^verbatim>\<open>/\<close>''; the wild card \<^verbatim>\<open>**\<close> matches over directory
wenzelm@68116
   595
  name hierarchies separated by ``\<^verbatim>\<open>/\<close>''. Thus the pattern ``\<^verbatim>\<open>*:**\<close>'' matches
wenzelm@68290
   596
  \<^emph>\<open>all\<close> theory exports. Multiple options \<^verbatim>\<open>-x\<close> refer to the union of all
wenzelm@68290
   597
  specified patterns.
wenzelm@68116
   598
wenzelm@68314
   599
  Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the
wenzelm@68116
   600
  default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its
wenzelm@68116
   601
  own sub-directory hierarchy, using the session-qualified theory name.
wenzelm@69671
   602
wenzelm@69671
   603
  Option \<^verbatim>\<open>-p\<close> specifies the number of elements that should be pruned from
wenzelm@69671
   604
  each name: it allows to reduce the resulting directory hierarchy at the
wenzelm@69671
   605
  danger of overwriting files due to loss of uniqueness.
wenzelm@68116
   606
\<close>
wenzelm@68116
   607
wenzelm@68348
   608
wenzelm@68348
   609
section \<open>Dump PIDE session database \label{sec:tool-dump}\<close>
wenzelm@68348
   610
wenzelm@68348
   611
text \<open>
wenzelm@68348
   612
  The @{tool_def "dump"} tool dumps information from the cumulative PIDE
wenzelm@68348
   613
  session database (which is processed on the spot). Its command-line usage
wenzelm@68348
   614
  is: @{verbatim [display]
wenzelm@68348
   615
\<open>Usage: isabelle dump [OPTIONS] [SESSIONS ...]
wenzelm@68348
   616
wenzelm@68348
   617
  Options are:
wenzelm@68348
   618
    -A NAMES     dump named aspects (default: ...)
wenzelm@68348
   619
    -B NAME      include session NAME and all descendants
wenzelm@68348
   620
    -D DIR       include session directory and select its sessions
wenzelm@68348
   621
    -O DIR       output directory for dumped files (default: "dump")
wenzelm@68348
   622
    -R           operate on requirements of selected sessions
wenzelm@68348
   623
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@68348
   624
    -a           select all sessions
wenzelm@68348
   625
    -d DIR       include session directory
wenzelm@68348
   626
    -g NAME      select session group NAME
wenzelm@68348
   627
    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
wenzelm@68348
   628
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@68348
   629
    -s           system build mode for logic image
wenzelm@68348
   630
    -v           verbose
wenzelm@68348
   631
    -x NAME      exclude session NAME and all descendants
wenzelm@68348
   632
wenzelm@68348
   633
  Dump cumulative PIDE session database, with the following aspects:
wenzelm@68348
   634
    ...\<close>}
wenzelm@68348
   635
wenzelm@68348
   636
  \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
wenzelm@68348
   637
  remaining command-line arguments specify sessions as in @{tool build}
wenzelm@68348
   638
  (\secref{sec:tool-build}): the cumulative PIDE database of all their loaded
wenzelm@68348
   639
  theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close>
wenzelm@68348
   640
  in the current directory).
wenzelm@68348
   641
wenzelm@68348
   642
  \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
wenzelm@68348
   643
  its theories are not processed again, and their PIDE session database is
wenzelm@68348
   644
  excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
wenzelm@68348
   645
  the logic image (\secref{sec:tool-build}).
wenzelm@68348
   646
wenzelm@68348
   647
  \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
wenzelm@68348
   648
  (\secref{sec:tool-build}).
wenzelm@68348
   649
wenzelm@68348
   650
  \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
wenzelm@68348
   651
wenzelm@68348
   652
  \<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated
wenzelm@68348
   653
  list. The default is to dump all known aspects, as given in the command-line
wenzelm@68348
   654
  usage of the tool. The underlying Isabelle/Scala function
wenzelm@68348
   655
  \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
wenzelm@68348
   656
  final PIDE state and document version. This allows to imitate Prover IDE
wenzelm@68348
   657
  rendering under program control.
wenzelm@68348
   658
\<close>
wenzelm@68348
   659
wenzelm@68348
   660
wenzelm@68348
   661
subsubsection \<open>Examples\<close>
wenzelm@68348
   662
wenzelm@68348
   663
text \<open>
wenzelm@68348
   664
  Dump all Isabelle/ZF sessions (which are rather small):
wenzelm@68348
   665
  @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
wenzelm@68348
   666
wenzelm@68348
   667
  \<^smallskip>
wenzelm@68348
   668
  Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
wenzelm@68348
   669
  as starting point:
wenzelm@68348
   670
  @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
wenzelm@68348
   671
wenzelm@68348
   672
  \<^smallskip>
wenzelm@68348
   673
  Dump all sessions connected to HOL-Analysis, including a full bootstrap of
wenzelm@68348
   674
  Isabelle/HOL from Isabelle/Pure:
wenzelm@68348
   675
  @{verbatim [display] \<open>isabelle dump -v -l Pure -B HOL-Analysis\<close>}
wenzelm@68348
   676
wenzelm@68348
   677
  This results in uniform PIDE markup for everything, except for the
wenzelm@68348
   678
  Isabelle/Pure bootstrap process itself. Producing that on the spot requires
wenzelm@68348
   679
  several GB of heap space, both for the Isabelle/Scala and Isabelle/ML
wenzelm@68348
   680
  process (in 64bit mode). Here are some relevant settings (\secref{sec:boot})
wenzelm@68348
   681
  for such ambitious applications:
wenzelm@68348
   682
  @{verbatim [display]
wenzelm@68348
   683
\<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
wenzelm@68348
   684
ML_OPTIONS="--minheap 4G --maxheap 32G"
wenzelm@68348
   685
\<close>}
wenzelm@69599
   686
\<close>
wenzelm@68348
   687
wenzelm@69599
   688
wenzelm@69599
   689
section \<open>Update theory sources based on PIDE markup \label{sec:tool-update}\<close>
wenzelm@69599
   690
wenzelm@69599
   691
text \<open>
wenzelm@69599
   692
  The @{tool_def "update"} tool updates theory sources based on markup that is
wenzelm@69599
   693
  produced from a running PIDE session (similar to @{tool dump}
wenzelm@69599
   694
  \secref{sec:tool-dump}). Its command-line usage is: @{verbatim [display]
wenzelm@69599
   695
\<open>Usage: isabelle update [OPTIONS] [SESSIONS ...]
wenzelm@69599
   696
wenzelm@69599
   697
  Options are:
wenzelm@69599
   698
    -B NAME      include session NAME and all descendants
wenzelm@69599
   699
    -D DIR       include session directory and select its sessions
wenzelm@69599
   700
    -R           operate on requirements of selected sessions
wenzelm@69599
   701
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@69599
   702
    -a           select all sessions
wenzelm@69599
   703
    -d DIR       include session directory
wenzelm@69599
   704
    -g NAME      select session group NAME
wenzelm@69599
   705
    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
wenzelm@69599
   706
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@69599
   707
    -s           system build mode for logic image
wenzelm@69599
   708
    -u OPT       overide update option: shortcut for "-o update_OPT"
wenzelm@69599
   709
    -v           verbose
wenzelm@69599
   710
    -x NAME      exclude session NAME and all descendants
wenzelm@69599
   711
wenzelm@69599
   712
  Update theory sources based on PIDE markup.\<close>}
wenzelm@69599
   713
wenzelm@69599
   714
  \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
wenzelm@69599
   715
  remaining command-line arguments specify sessions as in @{tool build}
wenzelm@69599
   716
  (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}).
wenzelm@69599
   717
wenzelm@69599
   718
  \<^medskip> Options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-s\<close> specify the underlying logic image is in @{tool
wenzelm@69599
   719
  dump} (\secref{sec:tool-dump}).
wenzelm@69599
   720
wenzelm@69599
   721
  \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
wenzelm@69599
   722
wenzelm@69599
   723
  \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
wenzelm@69599
   724
  (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close>
wenzelm@69599
   725
  options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for
wenzelm@69599
   726
  ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
wenzelm@69599
   727
wenzelm@69599
   728
  \<^medskip> The following update options are supported:
wenzelm@69599
   729
wenzelm@69599
   730
    \<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax
wenzelm@69599
   731
    (types, terms, etc.)~to use cartouches, instead of double-quoted strings
wenzelm@69599
   732
    or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x =
wenzelm@69610
   733
    x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>assume
wenzelm@69610
   734
    A\<close>'' is replaced by ``\<^theory_text>\<open>assume \<open>A\<close>\<close>''.
wenzelm@69599
   735
wenzelm@69599
   736
    \<^item> @{system_option update_mixfix_cartouches} to update mixfix templates to
wenzelm@69599
   737
    use cartouches instead of double-quoted strings. For example, ``\<^theory_text>\<open>(infixl
wenzelm@69599
   738
    \<doublequote>+\<doublequote> 65)\<close>'' is replaced by ``\<^theory_text>\<open>(infixl \<open>+\<close>
wenzelm@69599
   739
    65)\<close>''.
wenzelm@69599
   740
wenzelm@69599
   741
    \<^item> @{system_option update_control_cartouches} to update antiquotations to
wenzelm@69599
   742
    use the compact form with control symbol and cartouche argument. For
wenzelm@69599
   743
    example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by
wenzelm@69599
   744
    ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.)
wenzelm@69599
   745
wenzelm@69603
   746
    \<^item> @{system_option update_path_cartouches} to update file-system paths to
wenzelm@69603
   747
    use cartouches: this depends on language markup provided by semantic
wenzelm@69603
   748
    processing of parsed input.
wenzelm@69603
   749
wenzelm@69599
   750
  It is also possible to produce custom updates in Isabelle/ML, by reporting
wenzelm@69599
   751
  \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement
wenzelm@69599
   752
  text. This operation should be made conditional on specific system options,
wenzelm@69599
   753
  similar to the ones above. Searching the above option names in ML sources of
wenzelm@69599
   754
  \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples.
wenzelm@69599
   755
wenzelm@69602
   756
  Updates can be in conflict by producing nested or overlapping edits: this
wenzelm@69602
   757
  may require to run @{tool update} multiple times.
wenzelm@69599
   758
\<close>
wenzelm@69599
   759
wenzelm@69599
   760
wenzelm@69599
   761
subsubsection \<open>Examples\<close>
wenzelm@69599
   762
wenzelm@69599
   763
text \<open>
wenzelm@69599
   764
  Update some cartouche notation in all theory sources required for session
wenzelm@69599
   765
  \<^verbatim>\<open>HOL-Analysis\<close>:
wenzelm@69599
   766
wenzelm@69599
   767
  @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l Pure HOL-Analysis\<close>}
wenzelm@69599
   768
wenzelm@69599
   769
  \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> ---
wenzelm@69599
   770
  its image is taken as starting point and its sources are not touched:
wenzelm@69599
   771
wenzelm@69599
   772
  @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Analysis -B HOL-Analysis\<close>}
wenzelm@69599
   773
wenzelm@69599
   774
  \<^smallskip> This two-stage approach reduces resource requirements of the running PIDE
wenzelm@69599
   775
  session: a base image like \<^verbatim>\<open>HOL-Analysis\<close> (or \<^verbatim>\<open>HOL\<close>, \<^verbatim>\<open>HOL-Library\<close>) is
wenzelm@69599
   776
  more compact than importing all required theory (and ML) source files from
wenzelm@69599
   777
  \<^verbatim>\<open>Pure\<close>.
wenzelm@69599
   778
wenzelm@69599
   779
  \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
wenzelm@69599
   780
  separately with special options as follows:
wenzelm@69599
   781
wenzelm@69599
   782
  @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
wenzelm@69601
   783
  -o record_proofs=2\<close>}
wenzelm@69599
   784
wenzelm@69599
   785
  \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing
wenzelm@69599
   786
  Isabelle/ML heap sizes for very big PIDE processes that include many
wenzelm@69599
   787
  sessions, notably from the Archive of Formal Proofs.
wenzelm@68348
   788
\<close>
wenzelm@68348
   789
wenzelm@48578
   790
end