src/Doc/System/Sessions.thy
author wenzelm
Wed Jan 16 17:55:26 2019 +0100 (11 months ago)
changeset 69671 2486792eaf61
parent 69610 10644973cdde
child 69755 2fc85ce1f557
permissions -rw-r--r--
support pruning of export names;
     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> 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
   154   loss of uniqueness.
   155 \<close>
   156 
   157 
   158 subsubsection \<open>Examples\<close>
   159 
   160 text \<open>
   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.
   166 \<close>
   167 
   168 
   169 section \<open>System build options \label{sec:system-options}\<close>
   170 
   171 text \<open>
   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.
   175 
   176   The following options are particularly relevant to build Isabelle sessions,
   177   in particular with document preparation (\chref{ch:present}).
   178 
   179     \<^item> @{system_option_def "browser_info"} controls output of HTML browser
   180     info, see also \secref{sec:info}.
   181 
   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>.
   186 
   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
   192     document.
   193 
   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>.
   197 
   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.
   201 
   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}.
   205 
   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>).
   211 
   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>).
   218 
   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
   224     specified theories.
   225 
   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.
   230 
   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
   236     performance.
   237 
   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.
   241 
   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.
   246 
   247   The @{tool_def options} tool prints Isabelle system options. Its
   248   command-line usage is:
   249   @{verbatim [display]
   250 \<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
   251 
   252   Options are:
   253     -b           include $ISABELLE_BUILD_OPTIONS
   254     -g OPTION    get value of OPTION
   255     -l           list options
   256     -x FILE      export to FILE in YXML format
   257 
   258   Report Isabelle system options, augmented by MORE_OPTIONS given as
   259   arguments NAME=VAL or NAME.\<close>}
   260 
   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.
   263 
   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}.
   266 
   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.
   269 
   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.
   272 \<close>
   273 
   274 
   275 section \<open>Invoking the build process \label{sec:tool-build}\<close>
   276 
   277 text \<open>
   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>
   284   @{verbatim [display]
   285 \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
   286 
   287   Options are:
   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
   295     -b           build heap images
   296     -c           clean build
   297     -d DIR       include session directory
   298     -f           fresh build
   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
   306     -v           verbose
   307     -x NAME      exclude session NAME and all descendants
   308 
   309   Build and manage Isabelle sessions, depending on implicit settings:
   310 
   311   ISABELLE_BUILD_OPTIONS="..."
   312 
   313   ML_PLATFORM="..."
   314   ML_HOME="..."
   315   ML_SYSTEM="..."
   316   ML_OPTIONS="..."\<close>}
   317 
   318   \<^medskip>
   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.
   325 
   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>).
   331 
   332   \<^medskip>
   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.
   338 
   339   \<^medskip>
   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).
   342 
   343   \<^medskip>
   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
   347   membership.
   348 
   349   \<^medskip>
   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>).
   354 
   355   \<^medskip>
   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.
   358 
   359   \<^medskip>
   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.
   363 
   364   \<^medskip>
   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.
   373 
   374   \<^medskip>
   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.
   378 
   379   \<^medskip>
   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.
   382 
   383   \<^medskip>
   384   Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
   385   requirements.
   386 
   387   \<^medskip>
   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.
   391 
   392   \<^medskip>
   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}.
   396 
   397   \<^medskip>
   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.
   400 
   401   \<^medskip>
   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>.
   404 
   405   \<^medskip>
   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.
   408 
   409   \<^medskip>
   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.
   414 \<close>
   415 
   416 
   417 subsubsection \<open>Examples\<close>
   418 
   419 text \<open>
   420   Build a specific logic image:
   421   @{verbatim [display] \<open>isabelle build -b HOLCF\<close>}
   422 
   423   \<^smallskip>
   424   Build the main group of logic images:
   425   @{verbatim [display] \<open>isabelle build -b -g main\<close>}
   426 
   427   \<^smallskip>
   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>}
   430 
   431   \<^smallskip>
   432   Build all sessions where sources have changed (ignoring heaps):
   433   @{verbatim [display] \<open>isabelle build -a -S\<close>}
   434 
   435   \<^smallskip>
   436   Provide a general overview of the status of all Isabelle sessions, without
   437   building anything:
   438   @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
   439 
   440   \<^smallskip>
   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>}
   443 
   444   \<^smallskip>
   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>}
   448 
   449   \<^smallskip>
   450   Build some session images with cleanup of their descendants, while retaining
   451   their ancestry:
   452   @{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
   453 
   454   \<^smallskip>
   455   Clean all sessions without building anything:
   456   @{verbatim [display] \<open>isabelle build -a -n -c\<close>}
   457 
   458   \<^smallskip>
   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
   461   environment:
   462   @{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
   463 
   464   \<^smallskip>
   465   Inform about the status of all sessions required for AFP, without building
   466   anything yet:
   467   @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
   468 \<close>
   469 
   470 
   471 section \<open>Maintain theory imports wrt.\ session structure\<close>
   472 
   473 text \<open>
   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 ...]
   478 
   479   Options are:
   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)
   492     -v           verbose
   493     -x NAME      exclude session NAME and all descendants
   494 
   495   Maintain theory imports wrt. session structure. At least one operation
   496   needs to be specified (see options -I -M -U).\<close>}
   497 
   498   \<^medskip>
   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}).
   502 
   503   \<^medskip>
   504   Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
   505   (see \secref{sec:tool-build}).
   506 
   507   \<^medskip>
   508   Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
   509 
   510   \<^medskip>
   511   Option \<^verbatim>\<open>-I\<close> determines reports session imports:
   512 
   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.
   520 
   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.
   524 
   525   \<^medskip>
   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.
   530 
   531   \<^medskip>
   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.
   535 
   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.
   539 \<close>
   540 
   541 subsubsection \<open>Examples\<close>
   542 
   543 text \<open>
   544   Determine potential session imports for some project directory:
   545   @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
   546 
   547   \<^smallskip>
   548   Mercurial repository check for some project directory:
   549   @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
   550 
   551   \<^smallskip>
   552   Incremental update of theory imports for some project directory:
   553   @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
   554 \<close>
   555 
   556 
   557 section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
   558 
   559 text \<open>
   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
   563 
   564   Options are:
   565     -O DIR       output directory for exported files (default: "export")
   566     -d DIR       include session directory
   567     -l           list exports
   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)
   573 
   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.
   576 
   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>}
   580 
   581   \<^medskip>
   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!
   586 
   587   \<^medskip>
   588   Option \<^verbatim>\<open>-l\<close> lists all stored exports, with compound names
   589   \<open>theory\<close>\<^verbatim>\<open>:\<close>\<open>name\<close>.
   590 
   591   \<^medskip>
   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
   597   specified patterns.
   598 
   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.
   602 
   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.
   606 \<close>
   607 
   608 
   609 section \<open>Dump PIDE session database \label{sec:tool-dump}\<close>
   610 
   611 text \<open>
   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 ...]
   616 
   617   Options are:
   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
   630     -v           verbose
   631     -x NAME      exclude session NAME and all descendants
   632 
   633   Dump cumulative PIDE session database, with the following aspects:
   634     ...\<close>}
   635 
   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).
   641 
   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}).
   646 
   647   \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
   648   (\secref{sec:tool-build}).
   649 
   650   \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
   651 
   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.
   658 \<close>
   659 
   660 
   661 subsubsection \<open>Examples\<close>
   662 
   663 text \<open>
   664   Dump all Isabelle/ZF sessions (which are rather small):
   665   @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
   666 
   667   \<^smallskip>
   668   Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
   669   as starting point:
   670   @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
   671 
   672   \<^smallskip>
   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>}
   676 
   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:
   682   @{verbatim [display]
   683 \<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
   684 ML_OPTIONS="--minheap 4G --maxheap 32G"
   685 \<close>}
   686 \<close>
   687 
   688 
   689 section \<open>Update theory sources based on PIDE markup \label{sec:tool-update}\<close>
   690 
   691 text \<open>
   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 ...]
   696 
   697   Options are:
   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"
   709     -v           verbose
   710     -x NAME      exclude session NAME and all descendants
   711 
   712   Update theory sources based on PIDE markup.\<close>}
   713 
   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}).
   717 
   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}).
   720 
   721   \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
   722 
   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>''.
   727 
   728   \<^medskip> The following update options are supported:
   729 
   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>''.
   735 
   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>
   739     65)\<close>''.
   740 
   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>.)
   745 
   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.
   749 
   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.
   755 
   756   Updates can be in conflict by producing nested or overlapping edits: this
   757   may require to run @{tool update} multiple times.
   758 \<close>
   759 
   760 
   761 subsubsection \<open>Examples\<close>
   762 
   763 text \<open>
   764   Update some cartouche notation in all theory sources required for session
   765   \<^verbatim>\<open>HOL-Analysis\<close>:
   766 
   767   @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l Pure HOL-Analysis\<close>}
   768 
   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:
   771 
   772   @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Analysis -B HOL-Analysis\<close>}
   773 
   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>.
   778 
   779   \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
   780   separately with special options as follows:
   781 
   782   @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
   783   -o record_proofs=2\<close>}
   784 
   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.
   788 \<close>
   789 
   790 end