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