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