7 chapter \<open>Isabelle sessions and build management \label{ch:session}\<close>
10 An Isabelle \<^emph>\<open>session\<close> consists of a collection of related theories that may
11 be associated with formal documents (\chref{ch:present}). There is also a
12 notion of \<^emph>\<open>persistent heap\<close> image to capture the state of a session,
13 similar to object-code in compiled programming languages. Thus the concept
14 of session resembles that of a ``project'' in common IDE environments, but
15 the specific name emphasizes the connection to interactive theorem proving:
16 the session wraps-up the results of user-interaction with the prover in a
19 Application sessions are built on a given parent session, which may be built
20 recursively on other parents. Following this path in the hierarchy
21 eventually leads to some major object-logic session like \<open>HOL\<close>, which itself
22 is based on \<open>Pure\<close> as the common root of all sessions.
24 Processing sessions may take considerable time. Isabelle build management
25 helps to organize this efficiently. This includes support for parallel build
26 jobs, in addition to the multithreaded theory and proof checking that is
27 already provided by the prover process itself.
31 section \<open>Session ROOT specifications \label{sec:session-root}\<close>
34 Session specifications reside in files called \<^verbatim>\<open>ROOT\<close> within certain
35 directories, such as the home locations of registered Isabelle components or
36 additional project directories given by the user.
38 The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
39 of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
40 forms like identifiers, names, quoted strings, verbatim text, nested
41 comments etc. The grammar for @{syntax session_chapter} and @{syntax
42 session_entry} is given as syntax diagram below; each ROOT file may contain
43 multiple specifications like this. Chapters help to organize browser info
44 (\secref{sec:info}), but have no formal meaning. The default chapter is
45 ``\<open>Unsorted\<close>''.
47 Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
48 \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
52 @{syntax_def session_chapter}: @'chapter' @{syntax name}
55 @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
56 (@{syntax system_name} '+')? description? options? \<newline>
57 (sessions?) (theories*) (document_files*) \<newline> (export_files*)
59 groups: '(' (@{syntax name} +) ')'
61 dir: @'in' @{syntax embedded}
63 description: @'description' @{syntax text}
65 options: @'options' opts
67 opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
69 value: @{syntax name} | @{syntax real}
71 sessions: @'sessions' (@{syntax system_name}+)
73 theories: @'theories' opts? (theory_entry+)
75 theory_entry: @{syntax system_name} ('(' @'global' ')')?
77 document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+)
79 export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline>
83 \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
84 parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and
85 theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
86 applications: only Isabelle/Pure can bootstrap itself from nothing.
88 All such session specifications together describe a hierarchy (graph) of
89 sessions, with globally unique names. The new session name \<open>A\<close> should be
90 sufficiently long and descriptive to stand on its own in a potentially large
93 \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where
94 the new session is a member. Group names are uninterpreted and merely follow
95 certain conventions. For example, the Isabelle distribution tags some
96 important sessions by the group name called ``\<open>main\<close>''. Other projects may
97 invent their own conventions, but this requires some care to avoid clashes
98 within this unchecked name space.
100 \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit
101 directory for this session; by default this is the current directory of the
102 \<^verbatim>\<open>ROOT\<close> file.
104 All theory files are located relatively to the session directory. The prover
105 process is run within the same as its current working directory.
107 \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
110 \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
111 (\secref{sec:system-options}) that are used when processing this session,
112 but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
113 true\<close> for Boolean options.
115 \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
116 the current name space of theories. This allows to refer to a theory \<open>A\<close>
117 from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again
118 into the current ML process, which is in contrast to a theory that is
119 already present in the \<^emph>\<open>parent\<close> session.
121 Theories that are imported from other sessions are excluded from the current
124 \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
125 are processed within an environment that is augmented by the given options,
126 in addition to the global session options given before. Any number of blocks
127 of \isakeyword{theories} may be given. Options are only active for each
128 \isakeyword{theories} block separately.
130 A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
131 literally in other session specifications or theory imports --- the normal
132 situation is to qualify theory names by the session name; this ensures
133 globally unique names in big session graphs. Global theories are usually the
134 entry points to major logic sessions: \<open>Pure\<close>, \<open>Main\<close>, \<open>Complex_Main\<close>,
135 \<open>HOLCF\<close>, \<open>IFOL\<close>, \<open>FOL\<close>, \<open>ZF\<close>, \<open>ZFC\<close> etc. Regular Isabelle applications
136 should not claim any global theory names.
138 \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
139 source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
140 {\LaTeX}. Only these explicitly given files are copied from the base
141 directory to the document output directory, before formal document
142 processing is started (see also \secref{sec:tool-document}). The local path
143 structure of the \<open>files\<close> is preserved, which allows to reconstruct the
144 original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is
145 \<^verbatim>\<open>document\<close> within the session root directory.
147 \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number]
148 patterns\<close> writes theory exports to the file-system: the \<open>target_dir\<close>
149 specification is relative to the session root directory; its default is
150 \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref export}
151 (\secref{sec:tool-export}). The number given in brackets (default: 0)
152 specifies elements that should be pruned from each name: it allows to reduce
153 the resulting directory hierarchy at the danger of overwriting files due to
158 subsubsection \<open>Examples\<close>
161 See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
162 although it uses relatively complex quasi-hierarchic naming conventions like
163 \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
164 names that are relatively long and descriptive, as in the Archive of Formal
165 Proofs (\<^url>\<open>https://isa-afp.org\<close>), for example.
169 section \<open>System build options \label{sec:system-options}\<close>
172 See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
173 distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
174 editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
176 The following options are particularly relevant to build Isabelle sessions,
177 in particular with document preparation (\chref{ch:present}).
179 \<^item> @{system_option_def "browser_info"} controls output of HTML browser
180 info, see also \secref{sec:info}.
182 \<^item> @{system_option_def "document"} specifies the document output format,
183 see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
184 practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
185 \<^verbatim>\<open>document=pdf\<close>.
187 \<^item> @{system_option_def "document_output"} specifies an alternative
188 directory for generated output of the document preparation system; the
189 default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
190 explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
191 default configuration with output readily available to the author of the
194 \<^item> @{system_option_def "document_variants"} specifies document variants as
195 a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
196 document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
198 For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
199 two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
200 called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
202 Document variant names are just a matter of conventions. It is also
203 possible to use different document variant names (without tags) for
204 different document root entries, see also \secref{sec:tool-document}.
206 \<^item> @{system_option_def "document_tags"} specifies alternative command tags
207 as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a
208 specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other commands. This
209 is occasionally useful to control the global visibility of commands via
210 session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>).
212 \<^item> @{system_option_def "threads"} determines the number of worker threads
213 for parallel checking of theories and proofs. The default \<open>0\<close> means that a
214 sensible maximum value is determined by the underlying hardware. For
215 machines with many cores or with hyperthreading, this is often requires
216 manual adjustment (on the command-line or within personal settings or
217 preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
219 \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
220 space management. This is relevant for big sessions that may exhaust the
221 small 32-bit address space of the ML process (which is used by default).
222 When the option is enabled for some \isakeyword{theories} block, a full
223 sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
226 \<^item> @{system_option_def "condition"} specifies a comma-separated list of
227 process environment variables (or Isabelle settings) that are required for
228 the subsequent theories to be processed. Conditions are considered
229 ``true'' if the corresponding environment value is defined and non-empty.
231 \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"}
232 specify a real wall-clock timeout for the session as a whole: the two
233 values are multiplied and taken as the number of seconds. Typically,
234 @{system_option "timeout"} is given for individual sessions, and
235 @{system_option "timeout_scale"} as global adjustment to overall hardware
238 The timer is controlled outside the ML process by the JVM that runs
239 Isabelle/Scala. Thus it is relatively reliable in canceling processes that
240 get out of control, even if there is a deadlock without CPU time usage.
242 \<^item> @{system_option_def "profiling"} specifies a mode for global ML
243 profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
244 \<^ML>\<open>profile_time\<close> and \<^verbatim>\<open>allocations\<close> for \<^ML>\<open>profile_allocations\<close>.
245 Results appear near the bottom of the session log file.
247 The @{tool_def options} tool prints Isabelle system options. Its
248 command-line usage is:
250 \<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
253 -b include $ISABELLE_BUILD_OPTIONS
254 -g OPTION get value of OPTION
256 -x FILE export to FILE in YXML format
258 Report Isabelle system options, augmented by MORE_OPTIONS given as
259 arguments NAME=VAL or NAME.\<close>}
261 The command line arguments provide additional system options of the form
262 \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options.
264 Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones
265 of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
267 Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all
268 options with their declaration and current value.
270 Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
271 of printing it in human-readable form.
275 section \<open>Invoking the build process \label{sec:tool-build}\<close>
278 The @{tool_def build} tool invokes the build process for Isabelle sessions.
279 It manages dependencies between sessions, related sources of theories and
280 auxiliary files, and target heap images. Accordingly, it runs instances of
281 the prover process with optional document preparation. Its command-line
282 usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
283 \<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
285 \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
288 -B NAME include session NAME and all descendants
289 -D DIR include session directory and select its sessions
290 -N cyclic shuffling of NUMA CPU nodes (performance tuning)
291 -R operate on requirements of selected sessions
292 -S soft build: only observe changes of sources, not heap images
293 -X NAME exclude sessions from group NAME and all descendants
294 -a select all sessions
297 -d DIR include session directory
299 -g NAME select session group NAME
300 -j INT maximum number of parallel jobs (default 1)
301 -k KEYWORD check theory sources for conflicts with proposed keywords
302 -l list session source files
303 -n no build -- test dependencies only
304 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
305 -s system build mode: produce output in ISABELLE_HOME
307 -x NAME exclude session NAME and all descendants
309 Build and manage Isabelle sessions, depending on implicit settings:
311 ISABELLE_BUILD_OPTIONS="..."
316 ML_OPTIONS="..."\<close>}
319 Isabelle sessions are defined via session ROOT files as described in
320 (\secref{sec:session-root}). The totality of sessions is determined by
321 collecting such specifications from all Isabelle component directories
322 (\secref{sec:components}), augmented by more directories given via options
323 \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session
324 \<^verbatim>\<open>ROOT\<close> file with several session specifications.
326 Any session root directory may refer recursively to further directories of
327 the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
328 helps to organize large collections of session specifications, or to make
329 \<^verbatim>\<open>-d\<close> command line options persistent (e.g.\ in
330 \<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
333 The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close>
334 given as command-line arguments, or session groups that are given via one or
335 more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> selects all sessions. The build tool
336 takes session dependencies into account: the set of selected sessions is
337 completed by including all ancestors.
340 One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions to be included (all
341 descendants wrt.\ the session parent or import graph).
344 One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded (all
345 descendants wrt.\ the session parent or import graph). Option \<^verbatim>\<open>-X\<close> is
346 analogous to this, but excluded sessions are specified by session group
350 Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
351 requirements: all ancestor sessions excluding the original selection. This
352 allows to prepare the stage for some build process with different options,
353 before running the main build itself (without option \<^verbatim>\<open>-R\<close>).
356 Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined
357 in the given directories.
360 Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to
361 those sessions that have changed sources (according to actually imported
362 theories). The status of heap images is ignored.
365 The build process depends on additional options
366 (\secref{sec:system-options}) that are passed to the prover eventually. The
367 settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
368 additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>.
369 Moreover, the environment of system build options may be augmented on the
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
371 \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on
372 the command-line are applied in the given order.
375 Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
376 sessions. By default, images are only saved for inner nodes of the hierarchy
377 of sessions, as required for other sessions to continue later on.
380 Option \<^verbatim>\<open>-c\<close> cleans the selected sessions (all descendants wrt.\ the session
381 parent or import graph) before performing the specified build operation.
384 Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
388 Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
389 (including optional cleanup). Note that the return code always indicates the
390 status of the set of selected sessions.
393 Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
394 processes). Each prover process is subject to a separate limit of parallel
395 worker threads, cf.\ system option @{system_option_ref threads}.
398 Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
399 performance tuning on Linux servers with separate CPU/memory modules.
402 Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that session images are
403 stored in \<^path>\<open>$ISABELLE_HEAPS_SYSTEM\<close> instead of \<^path>\<open>$ISABELLE_HEAPS\<close>.
406 Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
407 the source files that contribute to a session.
410 Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
411 uses allowed). The theory sources are checked for conflicts wrt.\ this
412 hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
413 that need to be quoted.
417 subsubsection \<open>Examples\<close>
420 Build a specific logic image:
421 @{verbatim [display] \<open>isabelle build -b HOLCF\<close>}
424 Build the main group of logic images:
425 @{verbatim [display] \<open>isabelle build -b -g main\<close>}
428 Build all descendants (and requirements) of \<^verbatim>\<open>FOL\<close> and \<^verbatim>\<open>ZF\<close>:
429 @{verbatim [display] \<open>isabelle build -B FOL -B ZF\<close>}
432 Build all sessions where sources have changed (ignoring heaps):
433 @{verbatim [display] \<open>isabelle build -a -S\<close>}
436 Provide a general overview of the status of all Isabelle sessions, without
438 @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
441 Build all sessions with HTML browser info and PDF document preparation:
442 @{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
445 Build all sessions with a maximum of 8 parallel prover processes and 4
446 worker threads each (on a machine with many cores):
447 @{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
450 Build some session images with cleanup of their descendants, while retaining
452 @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
455 Clean all sessions without building anything:
456 @{verbatim [display] \<open>isabelle build -a -n -c\<close>}
459 Build all sessions from some other directory hierarchy, according to the
460 settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle
462 @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
465 Inform about the status of all sessions required for AFP, without building
467 @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
471 section \<open>Maintain theory imports wrt.\ session structure\<close>
474 The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
475 session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
476 \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
477 \<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
480 -B NAME include session NAME and all descendants
481 -D DIR include session directory and select its sessions
482 -I operation: report session imports
483 -M operation: Mercurial repository check for theory files
484 -R operate on requirements of selected sessions
485 -U operation: update theory imports to use session qualifiers
486 -X NAME exclude sessions from group NAME and all descendants
487 -a select all sessions
488 -d DIR include session directory
489 -g NAME select session group NAME
490 -i incremental update according to session graph structure
491 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
493 -x NAME exclude session NAME and all descendants
495 Maintain theory imports wrt. session structure. At least one operation
496 needs to be specified (see options -I -M -U).\<close>}
499 The selection of sessions and session directories works as for @{tool build}
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
501 \secref{sec:tool-build}).
504 Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
505 (see \secref{sec:tool-build}).
508 Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
511 Option \<^verbatim>\<open>-I\<close> determines reports session imports:
513 \<^descr>[Potential session imports] are derived from old-style use of theory
514 files from other sessions via the directory structure. After declaring
515 those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
516 proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
517 example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
518 \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
519 \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
521 \<^descr>[Actual session imports] are derived from the session qualifiers of all
522 currently imported theories. This helps to minimize dependencies in the
523 session import structure to what is actually required.
526 Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
527 the underlying session directories; non-repository directories are ignored.
528 This helps to find files that are accidentally ignored, e.g.\ due to
529 rearrangements of the session structure.
532 Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
533 to canonical session-qualified theory names, according to the theory name
534 space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
536 Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
537 following to the session graph structure in bottom-up order. This may
538 lead to more accurate results in complex session hierarchies.
541 subsubsection \<open>Examples\<close>
544 Determine potential session imports for some project directory:
545 @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
548 Mercurial repository check for some project directory:
549 @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
552 Incremental update of theory imports for some project directory:
553 @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
557 section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
560 The @{tool_def "export"} tool retrieves theory exports from the session
561 database. Its command-line usage is: @{verbatim [display]
562 \<open>Usage: isabelle export [OPTIONS] SESSION
565 -O DIR output directory for exported files (default: "export")
566 -d DIR include session directory
568 -n no build of session
569 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
570 -p NUM prune path of exported files by NUM elements
571 -s system build mode for session image
572 -x PATTERN extract files matching pattern (e.g.\ "*:**" for all)
574 List or export theory exports for SESSION: named blobs produced by
575 isabelle build. Option -l or -x is required; option -x may be repeated.
577 The PATTERN language resembles glob patterns in the shell, with ? and *
578 (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
579 and variants {pattern1,pattern2,pattern3}.\<close>}
582 The specified session is updated via @{tool build}
583 (\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close>. The
584 option \<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a
585 potentially outdated session database is used!
588 Option \<^verbatim>\<open>-l\<close> lists all stored exports, with compound names
589 \<open>theory\<close>\<^verbatim>\<open>:\<close>\<open>name\<close>.
592 Option \<^verbatim>\<open>-x\<close> extracts stored exports whose compound name matches the given
593 pattern. Note that wild cards ``\<^verbatim>\<open>?\<close>'' and ``\<^verbatim>\<open>*\<close>'' do not match the
594 separators ``\<^verbatim>\<open>:\<close>'' and ``\<^verbatim>\<open>/\<close>''; the wild card \<^verbatim>\<open>**\<close> matches over directory
595 name hierarchies separated by ``\<^verbatim>\<open>/\<close>''. Thus the pattern ``\<^verbatim>\<open>*:**\<close>'' matches
596 \<^emph>\<open>all\<close> theory exports. Multiple options \<^verbatim>\<open>-x\<close> refer to the union of all
599 Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the
600 default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its
601 own sub-directory hierarchy, using the session-qualified theory name.
603 Option \<^verbatim>\<open>-p\<close> specifies the number of elements that should be pruned from
604 each name: it allows to reduce the resulting directory hierarchy at the
605 danger of overwriting files due to loss of uniqueness.
609 section \<open>Dump PIDE session database \label{sec:tool-dump}\<close>
612 The @{tool_def "dump"} tool dumps information from the cumulative PIDE
613 session database (which is processed on the spot). Its command-line usage
614 is: @{verbatim [display]
615 \<open>Usage: isabelle dump [OPTIONS] [SESSIONS ...]
618 -A NAMES dump named aspects (default: ...)
619 -B NAME include session NAME and all descendants
620 -D DIR include session directory and select its sessions
621 -O DIR output directory for dumped files (default: "dump")
622 -R operate on requirements of selected sessions
623 -X NAME exclude sessions from group NAME and all descendants
624 -a select all sessions
625 -d DIR include session directory
626 -g NAME select session group NAME
627 -l NAME logic session name (default ISABELLE_LOGIC="HOL")
628 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
629 -s system build mode for logic image
631 -x NAME exclude session NAME and all descendants
633 Dump cumulative PIDE session database, with the following aspects:
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
637 remaining command-line arguments specify sessions as in @{tool build}
638 (\secref{sec:tool-build}): the cumulative PIDE database of all their loaded
639 theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close>
640 in the current directory).
642 \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
643 its theories are not processed again, and their PIDE session database is
644 excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
645 the logic image (\secref{sec:tool-build}).
647 \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
648 (\secref{sec:tool-build}).
650 \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
652 \<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated
653 list. The default is to dump all known aspects, as given in the command-line
654 usage of the tool. The underlying Isabelle/Scala function
655 \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
656 final PIDE state and document version. This allows to imitate Prover IDE
657 rendering under program control.
661 subsubsection \<open>Examples\<close>
664 Dump all Isabelle/ZF sessions (which are rather small):
665 @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
668 Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
670 @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
673 Dump all sessions connected to HOL-Analysis, including a full bootstrap of
674 Isabelle/HOL from Isabelle/Pure:
675 @{verbatim [display] \<open>isabelle dump -v -l Pure -B HOL-Analysis\<close>}
677 This results in uniform PIDE markup for everything, except for the
678 Isabelle/Pure bootstrap process itself. Producing that on the spot requires
679 several GB of heap space, both for the Isabelle/Scala and Isabelle/ML
680 process (in 64bit mode). Here are some relevant settings (\secref{sec:boot})
681 for such ambitious applications:
683 \<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
684 ML_OPTIONS="--minheap 4G --maxheap 32G"
689 section \<open>Update theory sources based on PIDE markup \label{sec:tool-update}\<close>
692 The @{tool_def "update"} tool updates theory sources based on markup that is
693 produced from a running PIDE session (similar to @{tool dump}
694 \secref{sec:tool-dump}). Its command-line usage is: @{verbatim [display]
695 \<open>Usage: isabelle update [OPTIONS] [SESSIONS ...]
698 -B NAME include session NAME and all descendants
699 -D DIR include session directory and select its sessions
700 -R operate on requirements of selected sessions
701 -X NAME exclude sessions from group NAME and all descendants
702 -a select all sessions
703 -d DIR include session directory
704 -g NAME select session group NAME
705 -l NAME logic session name (default ISABELLE_LOGIC="HOL")
706 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
707 -s system build mode for logic image
708 -u OPT overide update option: shortcut for "-o update_OPT"
710 -x NAME exclude session NAME and all descendants
712 Update theory sources based on PIDE markup.\<close>}
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
715 remaining command-line arguments specify sessions as in @{tool build}
716 (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}).
718 \<^medskip> Options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-s\<close> specify the underlying logic image is in @{tool
719 dump} (\secref{sec:tool-dump}).
721 \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
723 \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
724 (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close>
725 options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for
726 ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
728 \<^medskip> The following update options are supported:
730 \<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax
731 (types, terms, etc.)~to use cartouches, instead of double-quoted strings
732 or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x =
733 x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>assume
734 A\<close>'' is replaced by ``\<^theory_text>\<open>assume \<open>A\<close>\<close>''.
736 \<^item> @{system_option update_mixfix_cartouches} to update mixfix templates to
737 use cartouches instead of double-quoted strings. For example, ``\<^theory_text>\<open>(infixl
738 \<doublequote>+\<doublequote> 65)\<close>'' is replaced by ``\<^theory_text>\<open>(infixl \<open>+\<close>
741 \<^item> @{system_option update_control_cartouches} to update antiquotations to
742 use the compact form with control symbol and cartouche argument. For
743 example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by
744 ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.)
746 \<^item> @{system_option update_path_cartouches} to update file-system paths to
747 use cartouches: this depends on language markup provided by semantic
748 processing of parsed input.
750 It is also possible to produce custom updates in Isabelle/ML, by reporting
751 \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement
752 text. This operation should be made conditional on specific system options,
753 similar to the ones above. Searching the above option names in ML sources of
754 \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples.
756 Updates can be in conflict by producing nested or overlapping edits: this
757 may require to run @{tool update} multiple times.
761 subsubsection \<open>Examples\<close>
764 Update some cartouche notation in all theory sources required for session
765 \<^verbatim>\<open>HOL-Analysis\<close>:
767 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l Pure HOL-Analysis\<close>}
769 \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> ---
770 its image is taken as starting point and its sources are not touched:
772 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Analysis -B HOL-Analysis\<close>}
774 \<^smallskip> This two-stage approach reduces resource requirements of the running PIDE
775 session: a base image like \<^verbatim>\<open>HOL-Analysis\<close> (or \<^verbatim>\<open>HOL\<close>, \<^verbatim>\<open>HOL-Library\<close>) is
776 more compact than importing all required theory (and ML) source files from
777 \<^verbatim>\<open>Pure\<close>.
779 \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
780 separately with special options as follows:
782 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
783 -o record_proofs=2\<close>}
785 \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing
786 Isabelle/ML heap sizes for very big PIDE processes that include many
787 sessions, notably from the Archive of Formal Proofs.