Theory Sessions
theory Sessions
imports Base
begin
chapter ‹Isabelle sessions and build management \label{ch:session}›
text ‹
An Isabelle ∗‹session› consists of a collection of related theories that may
be associated with formal documents (\chref{ch:present}). There is also a
notion of ∗‹persistent heap› image to capture the state of a session,
similar to object-code in compiled programming languages. Thus the concept
of session resembles that of a ``project'' in common IDE environments, but
the specific name emphasizes the connection to interactive theorem proving:
the session wraps-up the results of user-interaction with the prover in a
persistent form.
Application sessions are built on a given parent session, which may be built
recursively on other parents. Following this path in the hierarchy
eventually leads to some major object-logic session like ‹HOL›, which itself
is based on ‹Pure› as the common root of all sessions.
Processing sessions may take considerable time. Isabelle build management
helps to organize this efficiently. This includes support for parallel build
jobs, in addition to the multithreaded theory and proof checking that is
already provided by the prover process itself.
›
section ‹Session ROOT specifications \label{sec:session-root}›
text ‹
Session specifications reside in files called ▩‹ROOT› within certain
directories, such as the home locations of registered Isabelle components or
additional project directories given by the user.
The ROOT file format follows the lexical conventions of the ∗‹outer syntax›
of Isabelle/Isar, see also \<^cite>‹"isabelle-isar-ref"›. This defines common
forms like identifiers, names, quoted strings, verbatim text, nested
comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry}
and @{syntax session_entry} is given as syntax diagram below. Each ROOT file
may contain multiple specifications like this. Chapters help to organize
browser info (\secref{sec:info}), but have no formal meaning. The default
chapter is ``‹Unsorted›''. Chapter definitions, which are optional, allow to
associate additional information.
Isabelle/jEdit \<^cite>‹"isabelle-jedit"› includes a simple editing mode
▩‹isabelle-root› for session ROOT files, which is enabled by default for any
file of that name.
\<^rail>‹
@{syntax_def chapter_def}: @'chapter_definition' @{syntax name} ⏎
groups? description?
;
@{syntax_def chapter_entry}: @'chapter' @{syntax name}
;
@{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' ⏎
(@{syntax system_name} '+')? description? options? ⏎
sessions? directories? (theories*) ⏎
(document_theories?) (document_files*) ⏎
(export_files*) (export_classpath?)
;
groups: '(' (@{syntax name} +) ')'
;
dir: @'in' @{syntax embedded}
;
description: @'description' @{syntax text}
;
options: @'options' opts
;
opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
;
value: @{syntax name} | @{syntax real}
;
sessions: @'sessions' (@{syntax system_name}+)
;
directories: @'directories' (dir+)
;
theories: @'theories' opts? (theory_entry+)
;
theory_entry: @{syntax system_name} ('(' @'global' ')')?
;
document_theories: @'document_theories' (@{syntax name}+)
;
document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+)
;
export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? ⏎
(@{syntax embedded}+)
;
export_classpath: @'export_classpath' (@{syntax embedded}*)
›
➧ \isakeyword{chapter{\isacharunderscorekeyword}definition}~‹A (groups)›
associates a collection of groups with chapter ‹A›. All sessions that belong
to this chapter will automatically become members of these groups.
➧ \isakeyword{session}~‹A = B + body› defines a new session ‹A› based on
parent session ‹B›, with its content given in ‹body› (imported sessions and
theories). Note that a parent (like ‹HOL›) is mandatory in practical
applications: only Isabelle/Pure can bootstrap itself from nothing.
All such session specifications together describe a hierarchy (graph) of
sessions, with globally unique names. The new session name ‹A› should be
sufficiently long and descriptive to stand on its own in a potentially large
library.
➧ \isakeyword{session}~‹A (groups)› indicates a collection of groups where
the new session is a member. Group names are uninterpreted and merely follow
certain conventions. For example, the Isabelle distribution tags some
important sessions by the group name called ``‹main›''. Other projects may
invent their own conventions, but this requires some care to avoid clashes
within this unchecked name space.
➧ \isakeyword{session}~‹A›~\isakeyword{in}~‹dir› specifies an explicit
directory for this session; by default this is the current directory of the
▩‹ROOT› file.
All theory files are located relatively to the session directory. The prover
process is run within the same as its current working directory.
➧ \isakeyword{description}~‹text› is a free-form description for this
session (or chapter), e.g. for presentation purposes.
➧ \isakeyword{options}~‹[x = a, y = b, z]› defines separate options
(\secref{sec:system-options}) that are used when processing this session,
but ∗‹without› propagation to child sessions. Note that ‹z› abbreviates ‹z =
true› for Boolean options.
➧ \isakeyword{sessions}~‹names› specifies sessions that are ∗‹imported› into
the current name space of theories. This allows to refer to a theory ‹A›
from session ‹B› by the qualified name ‹B.A› --- although it is loaded again
into the current ML process, which is in contrast to a theory that is
already present in the ∗‹parent› session.
Theories that are imported from other sessions are excluded from the current
session document.
➧ \isakeyword{directories}~‹dirs› specifies additional directories for
import of theory files via \isakeyword{theories} within ▩‹ROOT› or
⬚‹imports› within a theory; ‹dirs› are relative to the main session
directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~‹dir›). These
directories need to be exclusively assigned to a unique session, without
implicit sharing of file-system locations.
➧ \isakeyword{theories}~‹options names› specifies a block of theories that
are processed within an environment that is augmented by the given options,
in addition to the global session options given before. Any number of blocks
of \isakeyword{theories} may be given. Options are only active for each
\isakeyword{theories} block separately.
A theory name that is followed by ‹(›\isakeyword{global}‹)› is treated
literally in other session specifications or theory imports --- the normal
situation is to qualify theory names by the session name; this ensures
globally unique names in big session graphs. Global theories are usually the
entry points to major logic sessions: ‹Pure›, ‹Main›, ‹Complex_Main›,
‹HOLCF›, ‹IFOL›, ‹FOL›, ‹ZF›, ‹ZFC› etc. Regular Isabelle applications
should not claim any global theory names.
➧ \isakeyword{document_theories}~‹names› specifies theories from other
sessions that should be included in the generated document source directory.
These theories need to be explicit imports in the current session, or
implicit imports from the underlying hierarchy of parent sessions. The
generated ▩‹session.tex› file is not affected: the session's {\LaTeX} setup
needs to ▩‹\input{›‹…›▩‹}› generated ▩‹.tex› files separately.
➧ \isakeyword{document_files}~‹(›\isakeyword{in}~‹base_dir) files› lists
source files for document preparation, typically ▩‹.tex› and ▩‹.sty› for
{\LaTeX}. Only these explicitly given files are copied from the base
directory to the document output directory, before formal document
processing is started (see also \secref{sec:tool-document}). The local path
structure of the ‹files› is preserved, which allows to reconstruct the
original directory hierarchy of ‹base_dir›. The default ‹base_dir› is
▩‹document› within the session root directory.
➧ \isakeyword{export_files}~‹(›\isakeyword{in}~‹target_dir) [number]
patterns› specifies theory exports that may get written to the file-system,
e.g. via @{tool_ref build} with option ▩‹-e› (\secref{sec:tool-build}). The
‹target_dir› specification is relative to the session root directory; its
default is ▩‹export›. Exports are selected via ‹patterns› as in @{tool_ref
export} (\secref{sec:tool-export}). The number given in brackets (default:
0) specifies the prefix of elements that should be removed from each name:
it allows to reduce the resulting directory hierarchy at the danger of
overwriting files due to loss of uniqueness.
➧ \isakeyword{export_classpath}~‹patterns› specifies export artifacts that
should be included into the local Java/Scala classpath of this session
context. This is only relevant for tools that allow dynamic loading of
service classes (\secref{sec:scala-build}), while most other Isabelle/Scala
tools require global configuration during system startup. An empty list of
‹patterns› defaults to ▩‹"*:classpath/*.jar"›, which fits to the naming
convention of JAR modules produced by the Isabelle/Isar command
⬚‹scala_build_generated_files› \<^cite>‹"isabelle-isar-ref"›.
›
subsubsection ‹Examples›
text ‹
See 🗏‹~~/src/HOL/ROOT› for a diversity of practically relevant situations,
although it uses relatively complex quasi-hierarchic naming conventions like
▩‹HOL-SPARK›, ▩‹HOL-SPARK-Examples›. An alternative is to use unqualified
names that are relatively long and descriptive, as in the Archive of Formal
Proofs (🌐‹https://isa-afp.org›), for example.
›
section ‹System build options \label{sec:system-options}›
text ‹
See 🗏‹~~/etc/options› for the main defaults provided by the Isabelle
distribution. Isabelle/jEdit \<^cite>‹"isabelle-jedit"› includes a simple
editing mode ▩‹isabelle-options› for this file-format.
The following options are particularly relevant to build Isabelle sessions,
in particular with document preparation (\chref{ch:present}).
▪ @{system_option_def "browser_info"} controls output of HTML browser
info, see also \secref{sec:info}.
▪ @{system_option_def "document"} controls document output for a
particular session or theory; ▩‹document=pdf› or ▩‹document=true› means
enabled, ▩‹document=""› or ▩‹document=false› means disabled (especially
for particular theories).
▪ @{system_option_def "document_output"} specifies an alternative
directory for generated output of the document preparation system; the
default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
default configuration with output readily available to the author of the
document.
▪ @{system_option_def "document_echo"} informs about document file names
during session presentation.
▪ @{system_option_def "document_variants"} specifies document variants as
a colon-separated list of ‹name=tags› entries. The default name is
▩‹document›, without additional tags.
Tags are specified as a comma separated list of modifier/name pairs and
tell {\LaTeX} how to interpret certain Isabelle command regions:
``▩‹+›‹foo›'' (or just ``‹foo›'') means to keep, ``▩‹-›‹foo›'' to drop,
and ``▩‹/›‹foo›'' to fold text tagged as ‹foo›. The builtin default is
equivalent to the tag specification
``▩‹+document,+theory,+proof,+ML,+visible,-invisible,+important,+unimportant›'';
see also the {\LaTeX} macros ▩‹\isakeeptag›, ▩‹\isadroptag›, and
▩‹\isafoldtag›, in 🗏‹~~/lib/texinputs/isabelle.sty›.
In contrast, ▩‹document_variants=document:outline=/proof,/ML› indicates
two documents: the one called ▩‹document› with default tags, and the other
called ▩‹outline› where proofs and ML sections are folded.
Document variant names are just a matter of conventions. It is also
possible to use different document variant names (without tags) for
different document root entries, see also \secref{sec:tool-document}.
▪ @{system_option_def "document_tags"} specifies alternative command tags
as a comma-separated list of items: either ``‹command›▩‹%›‹tag›'' for a
specific command, or ``▩‹%›‹tag›'' as default for all other commands. This
is occasionally useful to control the global visibility of commands via
session options (e.g.\ in ▩‹ROOT›).
▪ @{system_option_def "document_comment_latex"} enables regular {\LaTeX}
▩‹comment.sty›, instead of the historic version for plain {\TeX}
(default). The latter is much faster, but in conflict with {\LaTeX}
classes like Dagstuhl
LIPIcs⁋‹🌐‹https://github.com/dagstuhl-publishing/styles››.
▪ @{system_option_def "document_bibliography"} explicitly enables the use
of ▩‹bibtex›; the default is to check the presence of ▩‹root.bib›, but it
could have a different name.
▪ @{system_option_def "document_heading_prefix"} specifies a prefix for
the {\LaTeX} macro names generated from Isar commands like ⬚‹chapter›,
⬚‹section› etc. The default is ▩‹isamarkup›, e.g. ⬚‹section› becomes
▩‹\isamarkupsection›.
▪ @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default ‹0› means that a
sensible maximum value is determined by the underlying hardware. For
machines with many cores or with hyperthreading, this sometimes requires
manual adjustment (on the command-line or within personal settings or
preferences, not within a session ▩‹ROOT›).
▪ @{system_option_def "condition"} specifies a comma-separated list of
process environment variables (or Isabelle settings) that are required for
the subsequent theories to be processed. Conditions are considered
``true'' if the corresponding environment value is defined and non-empty.
▪ @{system_option_def "timeout"} and @{system_option_def "timeout_scale"}
specify a real wall-clock timeout for the session as a whole: the two
values are multiplied and taken as the number of seconds. Typically,
@{system_option "timeout"} is given for individual sessions, and
@{system_option "timeout_scale"} as global adjustment to overall hardware
performance.
The timer is controlled outside the ML process by the JVM that runs
Isabelle/Scala. Thus it is relatively reliable in canceling processes that
get out of control, even if there is a deadlock without CPU time usage.
▪ @{system_option_def "profiling"} specifies a mode for global ML
profiling. Possible values are the empty string (disabled), ▩‹time› for
\<^ML>‹profile_time› and ▩‹allocations› for \<^ML>‹profile_allocations›.
Results appear near the bottom of the session log file.
▪ @{system_option_def system_log} specifies an optional log file for
low-level messages produced by \<^ML>‹Output.system_message› in
Isabelle/ML; the standard value ``▩‹-›'' refers to console progress of the
build job.
▪ @{system_option_def "system_heaps"} determines the directories for
session heap images: \<^path>‹$ISABELLE_HEAPS› is the user directory and
\<^path>‹$ISABELLE_HEAPS_SYSTEM› the system directory (usually within the
Isabelle application). For ▩‹system_heaps=false›, heaps are stored in the
user directory and may be loaded from both directories. For
▩‹system_heaps=true›, store and load happens only in the system directory.
The @{tool_def options} tool prints Isabelle system options. Its
command-line usage is:
@{verbatim [display]
‹Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
Options are:
-b include $ISABELLE_BUILD_OPTIONS
-g OPTION get value of OPTION
-l list options
-t TAGS restrict list to given tags (comma-separated)
-x FILE export options to FILE in YXML format
Report Isabelle system options, augmented by MORE_OPTIONS given as
arguments NAME=VAL or NAME.›}
The command line arguments provide additional system options of the form
‹name›▩‹=›‹value› or ‹name› for Boolean options.
Option ▩‹-b› augments the implicit environment of system options by the ones
of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
Option ▩‹-g› prints the value of the given option. Option ▩‹-l› lists all
options with their declaration and current value. Option ▩‹-t› restricts the
listing to given tags (as comma-separated list), e.g. ▩‹-t build,document›.
Option ▩‹-x› specifies a file to export the result in YXML format, instead
of printing it in human-readable form.
›
section ‹Invoking the build process \label{sec:tool-build}›
text ‹
The @{tool_def build} tool invokes the build process for Isabelle sessions.
It manages dependencies between sessions, related sources of theories and
auxiliary files, and target heap images. Accordingly, it runs instances of
the prover process with optional document preparation. Its command-line
usage is:⁋‹Isabelle/Scala provides the same functionality via
\<^scala_method>‹isabelle.Build.build›.›
@{verbatim [display]
‹Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
-A ROOT include AFP with given root directory (":" for $AFP_BASE)
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-H HOSTS additional build cluster host specifications, of the form
"NAMES:PARAMETERS" (separated by commas)
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
-P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b build heap images
-c clean build
-d DIR include session directory
-e export files from session specification into file-system
-f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-k KEYWORD check theory sources for conflicts with proposed keywords
-l list session source files
-n no build -- take existing session build databases
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
-x NAME exclude session NAME and all descendants
Build and manage Isabelle sessions: ML heaps, session databases, documents.
Parameters for host specifications (option -H), apart from system options:
...
Notable system options: see "isabelle options -l -t build"
Notable system settings:
ISABELLE_TOOL_JAVA_OPTIONS="..."
ISABELLE_BUILD_OPTIONS="..."
ML_PLATFORM="..."
ML_HOME="..."
ML_SYSTEM="..."
ML_OPTIONS="..."›}
┉
Isabelle sessions are defined via session ROOT files as described in
(\secref{sec:session-root}). The totality of sessions is determined by
collecting such specifications from all Isabelle component directories
(\secref{sec:components}), augmented by more directories given via options
▩‹-d›~‹DIR› on the command line. Each such directory may contain a session
▩‹ROOT› file with several session specifications.
Any session root directory may refer recursively to further directories of
the same kind, by listing them in a catalog file ▩‹ROOTS› line-by-line. This
helps to organize large collections of session specifications, or to make
▩‹-d› command line options persistent (e.g.\ in
▩‹$ISABELLE_HOME_USER/ROOTS›).
┉
The subset of sessions to be managed is determined via individual ‹SESSIONS›
given as command-line arguments, or session groups that are given via one or
more options ▩‹-g›~‹NAME›. Option ▩‹-a› selects all sessions. The build tool
takes session dependencies into account: the set of selected sessions is
completed by including all ancestors.
┉
One or more options ▩‹-B›~‹NAME› specify base sessions to be included (all
descendants wrt.\ the session parent or import graph).
┉
One or more options ▩‹-x›~‹NAME› specify sessions to be excluded (all
descendants wrt.\ the session parent or import graph). Option ▩‹-X› is
analogous to this, but excluded sessions are specified by session group
membership.
┉
Option ▩‹-R› reverses the selection in the sense that it refers to its
requirements: all ancestor sessions excluding the original selection. This
allows to prepare the stage for some build process with different options,
before running the main build itself (without option ▩‹-R›).
┉
Option ▩‹-D› is similar to ▩‹-d›, but selects all sessions that are defined
in the given directories.
┉
Option ▩‹-S› indicates a ``soft build'': the selection is restricted to
those sessions that have changed sources (according to actually imported
theories). The status of heap images is ignored.
┉
The build process depends on additional options
(\secref{sec:system-options}) that are passed to the prover eventually. The
settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
additional defaults, e.g.\ ▩‹ISABELLE_BUILD_OPTIONS="document=pdf
threads=4"›. Moreover, the environment of system build options may be
augmented on the command line via ▩‹-o›~‹name›▩‹=›‹value› or ▩‹-o›~‹name›,
which abbreviates ▩‹-o›~‹name›▩‹=true› for Boolean or string options.
Multiple occurrences of ▩‹-o› on the command-line are applied in the given
order.
┉
Option ▩‹-P› enables PDF/HTML presentation in the given directory, where
``▩‹-P:›'' refers to the default @{setting_ref ISABELLE_BROWSER_INFO} (or
@{setting_ref ISABELLE_BROWSER_INFO_SYSTEM}). This applies only to
explicitly selected sessions; note that option ▩‹-R› allows to select all
requirements separately.
┉
Option ▩‹-b› ensures that heap images are produced for all selected
sessions. By default, images are only saved for inner nodes of the hierarchy
of sessions, as required for other sessions to continue later on.
┉
Option ▩‹-c› cleans the selected sessions (all descendants wrt.\ the session
parent or import graph) before performing the specified build operation.
┉
Option ▩‹-e› executes the \isakeyword{export_files} directives from the ROOT
specification of all explicitly selected sessions: the status of the session
build database needs to be OK, but the session could have been built
earlier. Using \isakeyword{export_files}, a session may serve as abstract
interface for add-on build artefacts, but these are only materialized on
explicit request: without option ▩‹-e› there is no effect on the physical
file-system yet.
┉
Option ▩‹-f› forces a fresh build of all selected sessions and their
requirements.
┉ Option ▩‹-n› omits the actual build process after the preparatory stage
(including optional cleanup). The overall return code always the status of
the set of selected sessions. Add-on builds (like presentation) are run for
successful sessions, i.e.\ already finished ones.
┉
Option ▩‹-j› specifies the maximum number of parallel build jobs (prover
processes). Each prover process is subject to a separate limit of parallel
worker threads, cf.\ system option @{system_option_ref threads}.
┉
Option ▩‹-N› enables cyclic shuffling of NUMA CPU nodes. This may help
performance tuning on Linux servers with separate CPU/memory modules.
┉
Option ▩‹-v› increases the general level of verbosity.
┉
Option ▩‹-l› lists the source files that contribute to a session.
┉
Option ▩‹-k› specifies a newly proposed keyword for outer syntax. It is
possible to use option ▩‹-k› repeatedly to check multiple keywords. The
theory sources are checked for conflicts wrt.\ this hypothetical change of
syntax, e.g.\ to reveal occurrences of identifiers that need to be quoted.
┉
Option ▩‹-H› augments the cluster hosts to be used in this build process.
Each ▩‹-H› option accepts multiple host names (separated by commas), which
all share the same (optional) parameters. Multiple ▩‹-H› options may be
given to specify further hosts (with different parameters). For example:
▩‹-H host1,host2:jobs=2,threads=4 -H host3:jobs=4,threads=6›.
The syntax for host parameters follows Isabelle outer syntax, notably with
double-quoted string literals. On the command-line, this may require extra
single quotes or escapes. For example: ▩‹-H 'host4:dirs="..."'›.
The presence of at least one ▩‹-H› option changes the mode of operation of
▩‹isabelle build› substantially. It uses a shared PostgreSQL database
server, which needs to be accessible from each node via local system options
such as @{system_option "build_database_server"}, @{system_option
"build_database_host"}, or @{system_option "build_database_ssh_host"}.
Remote host connections are managed via regular SSH configuration, see also
▩‹$HOME/.ssh/config› on each node.
›
subsubsection ‹Examples›
text ‹
Build a specific logic image:
@{verbatim [display] ‹ isabelle build -b HOLCF›}
┈
Build the main group of logic images:
@{verbatim [display] ‹ isabelle build -b -g main›}
┈
Build all descendants (and requirements) of ▩‹FOL› and ▩‹ZF›:
@{verbatim [display] ‹ isabelle build -B FOL -B ZF›}
┈
Build all sessions where sources have changed (ignoring heaps):
@{verbatim [display] ‹ isabelle build -a -S›}
┈
Provide a general overview of the status of all Isabelle sessions, without
building anything:
@{verbatim [display] ‹ isabelle build -a -n -v›}
┈
Build all sessions with HTML browser info and PDF document preparation:
@{verbatim [display] ‹ isabelle build -a -o browser_info -o document›}
┈
Build all sessions with a maximum of 8 parallel prover processes and 4
worker threads each (on a machine with many cores):
@{verbatim [display] ‹ isabelle build -a -j8 -o threads=4›}
┈
Build some session images with cleanup of their descendants, while retaining
their ancestry:
@{verbatim [display] ‹ isabelle build -b -c HOL-Library HOL-Algebra›}
┈
HTML/PDF presentation for sessions that happen to be properly built already,
without rebuilding anything except the missing browser info:
@{verbatim [display] ‹ isabelle build -a -n -o browser_info›}
┈
Clean all sessions without building anything:
@{verbatim [display] ‹ isabelle build -a -n -c›}
┈
Build all sessions from some other directory hierarchy, according to the
settings variable ▩‹AFP› that happens to be defined inside the Isabelle
environment:
@{verbatim [display] ‹ isabelle build -D '$AFP'›}
┈
Inform about the status of all sessions required for AFP, without building
anything yet:
@{verbatim [display] ‹ isabelle build -D '$AFP' -R -v -n›}
┈
Run a distributed build on 3 cluster hosts (local, ▩‹host1›, ▩‹host2›):
@{verbatim [display] ‹ isabelle build -a -j2 -o threads=8 \
-H host1:jobs=2,threads=8
-H host2:jobs=4:threads=4,numa,shared›}
›
section ‹Print messages from session build database \label{sec:tool-log}›
text ‹
The @{tool_def "build_log"} tool prints prover messages from the build
database of the given session. Its command-line usage is:
@{verbatim [display]
‹Usage: isabelle build_log [OPTIONS] [SESSIONS ...]
Options are:
-H REGEX filter messages by matching against head
-M REGEX filter messages by matching against body
-T NAME restrict to given theories (multiple options possible)
-U output Unicode symbols
-m MARGIN margin for pretty printing (default: 76.0)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v print all messages, including information etc.
Print messages from the session build database of the given sessions,
without any checks against current sources nor session structure: results
from old sessions or failed builds can be printed as well.
Multiple options -H and -M are conjunctive: all given patterns need to
match. Patterns match any substring, but ^ or $ may be used to match the
start or end explicitly.›}
The specified session databases are taken as is, with formal checking
against current sources: There is ∗‹no› implicit build process involved, so
it is possible to retrieve error messages from a failed session as well. The
order of messages follows the source positions of source files; thus the
result is mostly deterministic, independent of the somewhat erratic
evaluation of parallel processing.
┉ Option ▩‹-o› allows to change system options, as in @{tool build}
(\secref{sec:tool-build}). This may affect the storage space for the build
database, notably via @{system_option system_heaps}, or @{system_option
build_database_server} and its relatives.
┉ Option ▩‹-T› restricts output to given theories: multiple entries are
possible by repeating this option on the command-line. The default is to
refer to ∗‹all› theories used in the original session build process.
┉ Options ▩‹-m› and ▩‹-U› modify pretty printing and output of Isabelle
symbols. The default is for an old-fashioned ASCII terminal at 80 characters
per line (76 + 4 characters to prefix warnings or errors).
┉ Option ▩‹-v› prints all messages from the session database that are
normally inlined into the source text, including information messages etc.
┉ Options ▩‹-H› and ▩‹-M› filter messages according to their header or body
content, respectively. The header follows a very basic format that makes it
easy to match message kinds (e.g. ▩‹Warning› or ▩‹Error›) and file names
(e.g. ▩‹src/HOL/Nat.thy›). The body is usually pretty-printed, but for
matching it is treated like one long line: blocks are ignored and breaks are
turned into plain spaces (according to their formal width).
The syntax for patters follows regular expressions of the Java
platform.⁋‹🌐‹https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/regex/Pattern.html››
›
subsubsection ‹Examples›
text ‹
Print messages from theory ▩‹HOL.Nat› of session ▩‹HOL›, using Unicode
rendering of Isabelle symbols and a margin of 100 characters:
@{verbatim [display] ‹ isabelle build_log -T HOL.Nat -U -m 100 HOL›}
Print warnings about ambiguous input (inner syntax) of session
▩‹HOL-Library›, which is built beforehand:
@{verbatim [display] ‹ isabelle build HOL-Library
isabelle build_log -H "Warning" -M "Ambiguous input" HOL-Library›}
Print all errors from all sessions, e.g. from a partial build of
Isabelle/AFP:
@{verbatim [display] ‹ isabelle build_log -H "Error" $(isabelle sessions -a -d AFP/thys)›}
›
section ‹Retrieve theory exports \label{sec:tool-export}›
text ‹
The @{tool_def "export"} tool retrieves theory exports from the session
database. Its command-line usage is: @{verbatim [display]
‹Usage: isabelle export [OPTIONS] SESSION
Options are:
-O DIR output directory for exported files (default: "export")
-d DIR include session directory
-l list exports
-n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NUM prune path of exported files by NUM elements
-x PATTERN extract files matching pattern (e.g. "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
isabelle build. Option -l or -x is required; option -x may be repeated.
The PATTERN language resembles glob patterns in the shell, with ? and *
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
and variants {pattern1,pattern2,pattern3}.›}
┉
The specified session is updated via @{tool build}
(\secref{sec:tool-build}), with the same options ▩‹-d›, ▩‹-o›. The option
▩‹-n› suppresses the implicit build process: it means that a potentially
outdated session database is used!
┉
Option ▩‹-l› lists all stored exports, with compound names
‹theory›▩‹:›‹name›.
┉
Option ▩‹-x› extracts stored exports whose compound name matches the given
pattern. Note that wild cards ``▩‹?›'' and ``▩‹*›'' do not match the
separators ``▩‹:›'' and ``▩‹/›''; the wild card ▩‹**› matches over directory
name hierarchies separated by ``▩‹/›''. Thus the pattern ``▩‹*:**›'' matches
∗‹all› theory exports. Multiple options ▩‹-x› refer to the union of all
specified patterns.
Option ▩‹-O› specifies an alternative output directory for option ▩‹-x›: the
default is ▩‹export› within the current directory. Each theory creates its
own sub-directory hierarchy, using the session-qualified theory name.
Option ▩‹-p› specifies the number of elements that should be pruned from
each name: it allows to reduce the resulting directory hierarchy at the
danger of overwriting files due to loss of uniqueness.
›
section ‹Dump PIDE session database \label{sec:tool-dump}›
text ‹
The @{tool_def "dump"} tool dumps information from the cumulative PIDE
session database (which is processed on the spot). Its command-line usage
is: @{verbatim [display]
‹Usage: isabelle dump [OPTIONS] [SESSIONS ...]
Options are:
-A NAMES dump named aspects (default: ...)
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-O DIR output directory for dumped files (default: "dump")
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b NAME base logic image (default "Pure")
-d DIR include session directory
-g NAME select session group NAME
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
-x NAME exclude session NAME and all descendants
Dump cumulative PIDE session database, with the following aspects:
...›}
┉ Options ▩‹-B›, ▩‹-D›, ▩‹-R›, ▩‹-X›, ▩‹-a›, ▩‹-d›, ▩‹-g›, ▩‹-x› and the
remaining command-line arguments specify sessions as in @{tool build}
(\secref{sec:tool-build}): the cumulative PIDE database of all their loaded
theories is dumped to the output directory of option ▩‹-O› (default: ▩‹dump›
in the current directory).
┉ Option ▩‹-b› specifies an optional base logic image, for improved
scalability of the PIDE session. Its theories are only processed if it is
included in the overall session selection.
┉ Option ▩‹-o› overrides Isabelle system options as for @{tool build}
(\secref{sec:tool-build}).
┉ Option ▩‹-v› increases the general level of verbosity.
┉ Option ▩‹-A› specifies named aspects of the dump, as a comma-separated
list. The default is to dump all known aspects, as given in the command-line
usage of the tool. The underlying Isabelle/Scala operation
\<^scala_method>‹isabelle.Dump.dump› takes aspects as user-defined
operations on the final PIDE state and document version. This allows to
imitate Prover IDE rendering under program control.
›
subsubsection ‹Examples›
text ‹
Dump all Isabelle/ZF sessions (which are rather small):
@{verbatim [display] ‹ isabelle dump -v -B ZF›}
┈
Dump the quite substantial ▩‹HOL-Analysis› session, with full bootstrap
from Isabelle/Pure:
@{verbatim [display] ‹ isabelle dump -v HOL-Analysis›}
┈
Dump all sessions connected to HOL-Analysis, using main Isabelle/HOL as
basis:
@{verbatim [display] ‹ isabelle dump -v -b HOL -B HOL-Analysis›}
This results in uniform PIDE markup for everything, except for the
Isabelle/Pure bootstrap process itself. Producing that on the spot requires
several GB of heap space, both for the Isabelle/Scala and Isabelle/ML
process (in 64bit mode). Here are some relevant settings (\secref{sec:boot})
for such ambitious applications:
@{verbatim [display]
‹ ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
ML_OPTIONS="--minheap 4G --maxheap 32G"
›}
›
section ‹Update theory sources based on PIDE markup \label{sec:tool-update}›
text ‹
The @{tool_def "update"} tool updates theory sources based on markup that is
produced by the regular @{tool build} process \secref{sec:tool-build}). Its
command-line usage is: @{verbatim [display]
‹Usage: isabelle update [OPTIONS] [SESSIONS ...]
Options are:
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b build heap images
-c clean build
-d DIR include session directory
-f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-l NAME additional base logic
-n no build -- take existing session build databases
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u OPT override "update" option for selected sessions
-v verbose
-x NAME exclude session NAME and all descendants
Update theory sources based on PIDE markup produced by "isabelle build".›}
┉ Most options are the same as for @{tool build} (\secref{sec:tool-build}).
┉ Option ▩‹-l› specifies one or more base logics: these sessions and their
ancestors are ∗‹excluded› from the update.
┉ Option ▩‹-u› refers to specific ▩‹update› options, by relying on naming
convention: ``▩‹-u›~‹OPT›'' is a shortcut for ``▩‹-o›~▩‹update_›‹OPT›''.
┉ The following ▩‹update› options are supported:
▪ @{system_option_ref update_inner_syntax_cartouches} to update inner
syntax (types, terms, etc.)~to use cartouches, instead of double-quoted
strings or atomic identifiers. For example, ``⬚‹lemma \<doublequote>x =
x\<doublequote>›'' is replaced by ``⬚‹lemma ‹x = x››'', and ``⬚‹assume
A›'' is replaced by ``⬚‹assume ‹A››''.
▪ @{system_option update_mixfix_cartouches} to update mixfix templates to
use cartouches instead of double-quoted strings. For example, ``⬚‹(infixl
\<doublequote>+\<doublequote> 65)›'' is replaced by ``⬚‹(infixl ‹+›
65)›''.
▪ @{system_option_ref update_control_cartouches} to update antiquotations
to use the compact form with control symbol and cartouche argument. For
example, ``‹@{term \<doublequote>x + y\<doublequote>}›'' is replaced by
``‹\<^term>‹x + y››'' (the control symbol is literally ▩‹\<^term>›.)
▪ @{system_option_ref update_path_cartouches} to update file-system paths
to use cartouches: this depends on language markup provided by semantic
processing of parsed input.
▪ @{system_option_ref update_cite} to update {\LaTeX} ▩‹\cite› commands
and old-style ▩‹@{cite "name"}› document antiquotations.
It is also possible to produce custom updates in Isabelle/ML, by reporting
\<^ML>‹Markup.update› with the precise source position and a replacement
text. This operation should be made conditional on specific system options,
similar to the ones above. Searching the above option names in ML sources of
🗀‹$ISABELLE_HOME/src/Pure› provides some examples.
Updates can be in conflict by producing nested or overlapping edits: this
may require to run @{tool update} multiple times.
›
subsubsection ‹Examples›
text ‹
Update some cartouche notation in all theory sources required for session
▩‹HOL-Analysis› (and ancestors):
@{verbatim [display] ‹ isabelle update -u mixfix_cartouches HOL-Analysis›}
┈ Update the same for all application sessions based on ▩‹HOL-Analysis›, but
do not change the underlying ▩‹HOL› (and ▩‹Pure›) session:
@{verbatim [display] ‹ isabelle update -u mixfix_cartouches -l HOL -B HOL-Analysis›}
┈ Update all sessions that happen to be properly built beforehand:
@{verbatim [display] ‹ isabelle update -u mixfix_cartouches -n -a›}
›
section ‹Explore sessions structure›
text ‹
The @{tool_def "sessions"} tool explores the sessions structure. Its
command-line usage is:
@{verbatim [display]
‹Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
Options are:
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
-b follow session build dependencies (default: source imports)
-d DIR include session directory
-g NAME select session group NAME
-x NAME exclude session NAME and all descendants
Explore the structure of Isabelle sessions and print result names in
topological order (on stdout).›}
Arguments and options for session selection resemble @{tool build}
(\secref{sec:tool-build}).
›
subsubsection ‹Examples›
text ‹
All sessions of the Isabelle distribution:
@{verbatim [display] ‹ isabelle sessions -a›}
┉
Sessions that are imported by ▩‹ZF›:
@{verbatim [display] ‹ isabelle sessions ZF›}
┉
Sessions that are required to build ▩‹ZF›:
@{verbatim [display] ‹ isabelle sessions -b ZF›}
┉
Sessions that are based on ▩‹ZF› (and imported by it):
@{verbatim [display] ‹ isabelle sessions -B ZF›}
┉
All sessions of Isabelle/AFP (based in directory \<^path>‹AFP›):
@{verbatim [display] ‹ isabelle sessions -D AFP/thys›}
┉
Sessions required by Isabelle/AFP (based in directory \<^path>‹AFP›):
@{verbatim [display] ‹ isabelle sessions -R -D AFP/thys›}
›
section ‹Synchronize source repositories and session images for Isabelle and AFP›
text ‹
The @{tool_def sync} tool synchronizes a local Isabelle and AFP source
repository, possibly with prebuilt ▩‹.jar› files and session images. Its
command-line usage is: @{verbatim [display]
‹Usage: isabelle sync [OPTIONS] TARGET
Options are:
-A ROOT include AFP with given root directory (":" for $AFP_BASE)
-H purge heaps directory on target
-I NAME include session heap image and build database
(based on accidental local state)
-J preserve *.jar files
-T thorough treatment of file content and directory times
-a REV explicit AFP revision (default: state of working directory)
-s HOST SSH host name for remote target (default: local)
-u USER explicit SSH user name
-n no changes: dry-run
-p PORT explicit SSH port
-r REV explicit revision (default: state of working directory)
-v verbose
Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".›}
The approach is to apply @{tool hg_sync} (see \secref{sec:tool-hg-sync}) on
the underlying Isabelle repository, and an optional AFP repository.
Consequently, the Isabelle installation needs to be a Mercurial repository
clone: a regular download of the Isabelle distribution is not sufficient!
On the target side, AFP is placed into @{setting ISABELLE_HOME} as immediate
sub-directory with the literal name ▩‹AFP›; thus it can be easily included
elsewhere, e.g. @{tool build}~▩‹-d›~▩‹'~~/AFP'› on the remote side.
┉ Options ▩‹-T›, ▩‹-n›, ▩‹-p›, ▩‹-s›, ▩‹-u›, ▩‹-v› are the same as
the underlying @{tool hg_sync}.
┉ Options ▩‹-r› and ▩‹-a› are the same as option ▩‹-r› for @{tool hg_sync},
but for the Isabelle and AFP repositories, respectively. The AFP version is
only used if a corresponding repository is given via option ▩‹-A›, either
with explicit root directory, or as ▩‹-A:› to refer to ▩‹$AFP_BASE› (this
assumes AFP as component of the local Isabelle installation). If no AFP
repository is given, an existing ▩‹AFP› directory on the target remains
unchanged.
┉ Option ▩‹-J› uploads existing ▩‹.jar› files from the working directory,
which are usually Isabelle/Scala/Java modules under control of @{tool
scala_build} via ▩‹etc/build.props› (see also \secref{sec:scala-build}).
Thus the dependency management is accurate: bad uploads will be rebuilt
eventually (or ignored). This might fail for very old Isabelle versions,
when going into the past via option ▩‹-r›: here it is better to omit option
▩‹-J› and thus purge ▩‹.jar› files on the target (because they do not belong
to the repository).
┉ Option ▩‹-I› uploads a collection of session images. The set of ▩‹-I›
options specifies the end-points in the session build graph, including all
required ancestors. The result collection is uploaded using the underlying
▩‹rsync› policies, so unchanged images are not sent again. Session images
are assembled within the target ▩‹heaps› directory: this scheme fits
together with @{tool build}~▩‹-o system_heaps›. Images are taken as-is from
the local Isabelle installation, regardless of option ▩‹-r›. Upload of bad
images could waste time and space, but running e.g. @{tool build} on the
target will check dependencies accurately and rebuild outdated images on
demand.
┉ Option ▩‹-H› tells the underlying ▩‹rsync› process to purge the ▩‹heaps›
directory on the target, before uploading new images via option ▩‹-I›. The
default is to work monotonically: old material that is not overwritten
remains unchanged. Over time, this may lead to unused garbage, due to
changes in session names or the Poly/ML version. Option ▩‹-H› helps to avoid
wasting file-system space.
›
subsubsection ‹Examples›
text ‹
For quick testing of Isabelle + AFP on a remote machine, upload changed
sources, jars, and local sessions images for ▩‹HOL›:
@{verbatim [display] ‹ isabelle sync -A: -I HOL -J -s testmachine test/isabelle_afp›}
Assuming that the local ▩‹HOL› hierarchy has been up-to-date, and the local
and remote ML platforms coincide, a remote @{tool build} will proceed
without building ▩‹HOL› again.
┉ Here is a variation for extra-clean testing of Isabelle + AFP: no option
▩‹-J›, but option ▩‹-T› to disable the default ``quick check'' of ▩‹rsync›
(which only inspects file sizes and date stamps); existing heaps are
deleted:
@{verbatim [display] ‹ isabelle sync -A: -T -H -s testmachine test/isabelle_afp›}
›
end