# HG changeset patch # User wenzelm # Date 1444662677 -7200 # Node ID eb2463fc4d7b35af060e30eb13b78c3ce1ffb9a1 # Parent d2ce32c5793a5e818acb7cc5264cc14f9a5e33cf more symbols; diff -r d2ce32c5793a -r eb2463fc4d7b src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Mon Oct 12 17:10:36 2015 +0200 +++ b/src/Doc/System/Basics.thy Mon Oct 12 17:11:17 2015 +0200 @@ -12,22 +12,23 @@ Manual} @{cite "isabelle-implementation"} for the main concepts of the underlying implementation in Isabelle/ML. - \medskip The Isabelle system environment provides the following + \<^medskip> + The Isabelle system environment provides the following basic infrastructure to integrate tools smoothly. \begin{enumerate} - \item The \emph{Isabelle settings} mechanism provides process + \<^enum> The \emph{Isabelle settings} mechanism provides process environment variables to all Isabelle executables (including tools and user interfaces). - \item The raw \emph{Isabelle process} (@{executable_ref + \<^enum> The raw \emph{Isabelle process} (@{executable_ref "isabelle_process"}) runs logic sessions either interactively or in batch mode. In particular, this view abstracts over the invocation of the actual ML system to be used. Regular users rarely need to care about the low-level process. - \item The main \emph{Isabelle tool wrapper} (@{executable_ref + \<^enum> The main \emph{Isabelle tool wrapper} (@{executable_ref isabelle}) provides a generic startup environment Isabelle related utilities, user interfaces etc. Such tools automatically benefit from the settings mechanism. @@ -73,7 +74,7 @@ \begin{enumerate} - \item The special variable @{setting_def ISABELLE_HOME} is + \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined automatically from the location of the binary that has been run. @@ -84,7 +85,7 @@ links are admissible, but a plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work! - \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a + \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a @{executable_ref bash} shell script with the auto-export option for variables enabled. @@ -95,7 +96,7 @@ of these may have to be adapted (probably @{setting ML_SYSTEM} etc.). - \item The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it + \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it exists) is run in the same way as the site default settings. Note that the variable @{setting ISABELLE_HOME_USER} has already been set before --- usually to something like @{verbatim @@ -116,23 +117,25 @@ particular, external environment references should be kept at a minimum. - \medskip A few variables are somewhat special: + \<^medskip> + A few variables are somewhat special: \begin{itemize} - \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set + \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set automatically to the absolute path names of the @{executable "isabelle_process"} and @{executable isabelle} executables, respectively. - \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of + \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically to its value. \end{itemize} - \medskip Note that the settings environment may be inspected with + \<^medskip> + Note that the settings environment may be inspected with the @{tool getenv} tool. This might help to figure out the effect of complex settings scripts.\ @@ -155,7 +158,7 @@ its HOME should point to the \texttt{/home} directory tree or the Windows user home.} - \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the + \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the top-level Isabelle distribution directory. This is automatically determined from the Isabelle executable that has been invoked. Do not attempt to set @{setting ISABELLE_HOME} yourself from the shell! @@ -287,7 +290,7 @@ \begin{itemize} - \item @{verbatim "etc/settings"} holds additional settings that are + \<^item> @{verbatim "etc/settings"} holds additional settings that are initialized when bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As usual, the content is interpreted as a @{verbatim bash} script. It may refer to the component's enclosing @@ -309,7 +312,7 @@ ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" \end{ttbox} - \item @{verbatim "etc/components"} holds a list of further + \<^item> @{verbatim "etc/components"} holds a list of further sub-components of the same structure. The directory specifications given here can be either absolute (with leading @{verbatim "/"}) or relative to the component's main directory. @@ -332,7 +335,8 @@ This is tolerant wrt.\ missing component directories, but might produce a warning. - \medskip More complex situations may be addressed by initializing + \<^medskip> + More complex situations may be addressed by initializing components listed in a given catalog file, relatively to some base directory: @@ -406,39 +410,46 @@ Users are responsible for themselves to dispose their heap files when they are no longer needed. - \medskip The @{verbatim "-w"} option makes the output heap file + \<^medskip> + The @{verbatim "-w"} option makes the output heap file read-only after terminating. Thus subsequent invocations cause the logic image to be read-only automatically. - \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be + \<^medskip> + Using the @{verbatim "-e"} option, arbitrary ML code may be passed to the Isabelle session from the command line. Multiple @{verbatim "-e"}'s are evaluated in the given order. Strange things may happen when erroneous ML code is provided. Also make sure that the ML commands are terminated properly by semicolon. - \medskip The @{verbatim "-m"} option adds identifiers of print modes + \<^medskip> + The @{verbatim "-m"} option adds identifiers of print modes to be made active for this session. Typically, this is used by some user interface, e.g.\ to enable output of proper mathematical symbols. - \medskip Isabelle normally enters an interactive top-level loop + \<^medskip> + Isabelle normally enters an interactive top-level loop (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"} option inhibits interaction, thus providing a pure batch mode facility. - \medskip Option @{verbatim "-o"} allows to override Isabelle system + \<^medskip> + Option @{verbatim "-o"} allows to override Isabelle system options for this process, see also \secref{sec:system-options}. Alternatively, option @{verbatim "-O"} specifies the full environment of system options as a file in YXML format (according to the Isabelle/Scala function @{verbatim isabelle.Options.encode}). - \medskip The @{verbatim "-P"} option starts the Isabelle process wrapper + \<^medskip> + The @{verbatim "-P"} option starts the Isabelle process wrapper for Isabelle/Scala, with a private protocol running over the specified TCP socket. Isabelle/ML and Isabelle/Scala provide various programming interfaces to invoke protocol functions over untyped strings and XML trees. - \medskip The @{verbatim "-S"} option makes the Isabelle process more + \<^medskip> + The @{verbatim "-S"} option makes the Isabelle process more secure by disabling some critical operations, notably runtime compilation and evaluation of ML source code. \ @@ -475,7 +486,8 @@ isabelle_process -r Test \end{ttbox} - \bigskip The next example demonstrates batch execution of Isabelle. + \<^bigskip> + The next example demonstrates batch execution of Isabelle. We retrieve the @{verbatim Main} theory value from the theory loader within ML (observe the delicate quoting rules for the Bash shell vs.\ ML): diff -r d2ce32c5793a -r eb2463fc4d7b src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Mon Oct 12 17:10:36 2015 +0200 +++ b/src/Doc/System/Misc.thy Mon Oct 12 17:11:17 2015 +0200 @@ -35,7 +35,8 @@ When no file name is specified, the browser automatically changes to the directory @{setting ISABELLE_BROWSER_INFO}. - \medskip The @{verbatim "-b"} option indicates that this is for + \<^medskip> + The @{verbatim "-b"} option indicates that this is for administrative build only, i.e.\ no browser popup if no files are given. @@ -46,7 +47,8 @@ output written to the indicated file; note that @{verbatim pdf} produces an @{verbatim eps} copy as well. - \medskip The applet version of the browser is part of the standard + \<^medskip> + The applet version of the browser is part of the standard WWW theory presentation, see the link ``theory dependencies'' within each session index. \ @@ -75,20 +77,20 @@ \begin{itemize} - \item A red arrow before a directory name indicates that the + \<^item> A red arrow before a directory name indicates that the directory is currently ``folded'', i.e.~the nodes in this directory are collapsed to one single node. In the right sub-window, the names of nodes corresponding to folded directories are enclosed in square brackets and displayed in red color. - \item A green downward arrow before a directory name indicates that + \<^item> A green downward arrow before a directory name indicates that the directory is currently ``unfolded''. It can be folded by clicking on the directory name. Clicking on the name for a second time unfolds the directory again. Alternatively, a directory can also be unfolded by clicking on the corresponding node in the right sub-window. - \item Blue arrows stand before ordinary node names. When clicking on + \<^item> Blue arrows stand before ordinary node names. When clicking on such a name (i.e.\ that of a theory), the graph display window focuses to the corresponding node. Double clicking invokes a text viewer window in which the contents of the theory file are @@ -281,7 +283,8 @@ Display DOCUMENT (in DVI or PDF format). \end{ttbox} - \medskip The settings @{setting DVI_VIEWER} and @{setting + \<^medskip> + The settings @{setting DVI_VIEWER} and @{setting PDF_VIEWER} determine the programs for viewing the corresponding file formats. Normally this opens the document via the desktop environment, potentially in an asynchronous manner with re-use of @@ -304,7 +307,8 @@ display the corresponding document (see also \secref{sec:tool-display}). - \medskip The @{setting ISABELLE_DOCS} setting specifies the list of + \<^medskip> + The @{setting ISABELLE_DOCS} setting specifies the list of directories (separated by colons) to be scanned for documentations. \ @@ -362,7 +366,8 @@ isabelle getenv ISABELLE_HOME_USER \end{ttbox} - \medskip Get the value only of the same settings variable, which is + \<^medskip> + Get the value only of the same settings variable, which is particularly useful in shell scripts: \begin{ttbox} isabelle getenv -b ISABELLE_OUTPUT @@ -396,7 +401,8 @@ should be placed, which is typically a directory in the shell's @{setting PATH}, such as @{verbatim "$HOME/bin"}. - \medskip It is also possible to make symbolic links of the main + \<^medskip> + It is also possible to make symbolic links of the main Isabelle executables manually, but making separate copies outside the Isabelle distribution directory will not work!\ @@ -421,7 +427,8 @@ Option @{verbatim "-q"} omits printing of the result file name. - \medskip Implementors of Isabelle tools and applications are + \<^medskip> + Implementors of Isabelle tools and applications are encouraged to make derived Isabelle logos for their own projects using this template.\ @@ -439,7 +446,8 @@ Display Isabelle version information. \end{ttbox} - \medskip The default is to output the full version string of the + \<^medskip> + The default is to output the full version string of the Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}. The @{verbatim "-i"} option produces a short identification derived @@ -456,13 +464,13 @@ \begin{enumerate} - \item The encoding is always UTF-8. + \<^enum> The encoding is always UTF-8. - \item Body text is represented verbatim (no escaping, no special + \<^enum> Body text is represented verbatim (no escaping, no special treatment of white space, no named entities, no CDATA chunks, no comments). - \item Markup elements are represented via ASCII control characters + \<^enum> Markup elements are represented via ASCII control characters @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows: \begin{tabular}{ll} diff -r d2ce32c5793a -r eb2463fc4d7b src/Doc/System/Presentation.thy --- a/src/Doc/System/Presentation.thy Mon Oct 12 17:10:36 2015 +0200 +++ b/src/Doc/System/Presentation.thy Mon Oct 12 17:11:17 2015 +0200 @@ -71,8 +71,7 @@ such as generating Postscript files, which are not available in the applet version. See \secref{sec:browse} for further information. - \medskip - + \<^medskip> The easiest way to let Isabelle generate theory browsing information for existing sessions is to invoke @{tool build} with suitable options: @@ -98,13 +97,15 @@ information as well, see \secref{sec:tool-document} for further details. - \bigskip The theory browsing information is stored in a + \<^bigskip> + The theory browsing information is stored in a sub-directory directory determined by the @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the session chapter and identifier. In order to present Isabelle applications on the web, the corresponding subdirectory from @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.\ + section \Preparing session root directories \label{sec:tool-mkroot}\ text \The @{tool_def mkroot} tool configures a given directory as @@ -126,7 +127,8 @@ files or directories. Earlier attempts to generate a session root need to be deleted manually. - \medskip Option @{verbatim "-d"} indicates that the session shall be + \<^medskip> + Option @{verbatim "-d"} indicates that the session shall be accompanied by a formal document, with @{text DIR}@{verbatim "/document/root.tex"} as its {\LaTeX} entry point (see also \chref{ch:present}). @@ -134,7 +136,8 @@ Option @{verbatim "-n"} allows to specify an alternative session name; otherwise the base name of the given directory is used. - \medskip The implicit Isabelle settings variable @{setting + \<^medskip> + The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled into the generated @{verbatim ROOT} file.\ @@ -148,7 +151,8 @@ isabelle mkroot -d Test && isabelle build -D Test \end{ttbox} - \medskip Upgrade the current directory into a session ROOT with + \<^medskip> + Upgrade the current directory into a session ROOT with document preparation, and build it: \begin{ttbox} isabelle mkroot -d && isabelle build -D . @@ -180,17 +184,20 @@ information document output as well, e.g.\ in case of errors encountered in the batch run. - \medskip The @{verbatim "-c"} option tells @{tool document} to + \<^medskip> + The @{verbatim "-c"} option tells @{tool document} to dispose the document sources after successful operation! This is the right thing to do for sources generated by an Isabelle process, but take care of your files in manual document preparation! - \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify + \<^medskip> + The @{verbatim "-n"} and @{verbatim "-o"} option specify the final output file name and format, the default is ``@{verbatim document.dvi}''. Note that the result will appear in the parent of the target @{verbatim DIR}. - \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret + \<^medskip> + The @{verbatim "-t"} option tells {\LaTeX} how to interpret tagged Isabelle command regions. Tags are specified as a comma separated list of modifier/name pairs: ``@{verbatim "+"}@{text foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim @@ -202,12 +209,14 @@ @{verbatim "\\isafoldtag"}, in @{file "~~/lib/texinputs/isabelle.sty"}. - \medskip Document preparation requires a @{verbatim document} + \<^medskip> + Document preparation requires a @{verbatim document} directory within the session sources. This directory is supposed to contain all the files needed to produce the final document --- apart from the actual theories which are generated by Isabelle. - \medskip For most practical purposes, @{tool document} is smart + \<^medskip> + For most practical purposes, @{tool document} is smart enough to create any of the specified output formats, taking @{verbatim root.tex} supplied by the user as a starting point. This even includes multiple runs of {\LaTeX} to accommodate references @@ -223,7 +232,8 @@ but it is also possible to harvest generated {\LaTeX} sources and copy them elsewhere. - \medskip When running the session, Isabelle copies the content of + \<^medskip> + When running the session, Isabelle copies the content of the original @{verbatim document} directory into its proper place within @{setting ISABELLE_BROWSER_INFO}, according to the session path and document variant. Then, for any processed theory @{text A} @@ -254,7 +264,8 @@ bookmarks), we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well. - \medskip As a final step of Isabelle document preparation, @{tool + \<^medskip> + As a final step of Isabelle document preparation, @{tool document}~@{verbatim "-c"} is run on the resulting copy of the @{verbatim document} directory. Thus the actual output document is built and installed in its proper place. The generated sources are diff -r d2ce32c5793a -r eb2463fc4d7b src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Mon Oct 12 17:10:36 2015 +0200 +++ b/src/Doc/System/Sessions.thy Mon Oct 12 17:11:17 2015 +0200 @@ -171,15 +171,15 @@ \begin{itemize} - \item @{system_option_def "browser_info"} controls output of HTML + \<^item> @{system_option_def "browser_info"} controls output of HTML browser info, see also \secref{sec:info}. - \item @{system_option_def "document"} specifies the document output + \<^item> @{system_option_def "document"} specifies the document output format, see @{tool document} option @{verbatim "-o"} in \secref{sec:tool-document}. In practice, the most relevant values are @{verbatim "document=false"} or @{verbatim "document=pdf"}. - \item @{system_option_def "document_output"} specifies an + \<^item> @{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 @@ -187,7 +187,7 @@ default configuration with output readily available to the author of the document. - \item @{system_option_def "document_variants"} specifies document + \<^item> @{system_option_def "document_variants"} specifies document variants as a colon-separated list of @{text "name=tags"} entries, corresponding to @{tool document} options @{verbatim "-n"} and @{verbatim "-t"}. @@ -203,7 +203,7 @@ different document root entries, see also \secref{sec:tool-document}. - \item @{system_option_def "threads"} determines the number of worker + \<^item> @{system_option_def "threads"} determines the number of worker threads for parallel checking of theories and proofs. The default @{text "0"} means that a sensible maximum value is determined by the underlying hardware. For machines with many cores or with @@ -211,7 +211,7 @@ command-line or within personal settings or preferences, not within a session @{verbatim ROOT}). - \item @{system_option_def "condition"} specifies a comma-separated + \<^item> @{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 @@ -222,7 +222,7 @@ explicitly via some shell prefix @{verbatim "env ISABELLE_FULL_TEST=true"} before invoking @{tool build}. - \item @{system_option_def "timeout"} specifies a real wall-clock + \<^item> @{system_option_def "timeout"} specifies a real wall-clock timeout (in seconds) for the session as a whole. The timer is controlled outside the ML process by the JVM that runs Isabelle/Scala. Thus it is relatively reliable in canceling @@ -302,7 +302,8 @@ ML_OPTIONS="..." \end{ttbox} - \medskip Isabelle sessions are defined via session ROOT files as + \<^medskip> + 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 @@ -317,29 +318,34 @@ command line options persistent (say within @{verbatim "$ISABELLE_HOME_USER/ROOTS"}). - \medskip The subset of sessions to be managed is determined via + \<^medskip> + The subset of sessions to be managed is determined via individual @{text "SESSIONS"} given as command-line arguments, or session groups that are given via one or more options @{verbatim "-g"}~@{text "NAME"}. Option @{verbatim "-a"} selects all sessions. The build tool takes session dependencies into account: the set of selected sessions is completed by including all ancestors. - \medskip One or more options @{verbatim "-x"}~@{text NAME} specify + \<^medskip> + One or more options @{verbatim "-x"}~@{text NAME} specify sessions to be excluded. All descendents of excluded sessions are removed from the selection as specified above. Option @{verbatim "-X"} is analogous to this, but excluded sessions are specified by session group membership. - \medskip Option @{verbatim "-R"} reverses the selection in the sense + \<^medskip> + Option @{verbatim "-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 @{verbatim "-R"}). - \medskip Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but + \<^medskip> + Option @{verbatim "-D"} is similar to @{verbatim "-d"}, but selects all sessions that are defined in the given directories. - \medskip The build process depends on additional options + \<^medskip> + 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.\ @@ -351,35 +357,42 @@ Boolean options. Multiple occurrences of @{verbatim "-o"} on the command-line are applied in the given order. - \medskip Option @{verbatim "-b"} ensures that heap images are + \<^medskip> + Option @{verbatim "-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. - \medskip Option @{verbatim "-c"} cleans all descendants of the + \<^medskip> + Option @{verbatim "-c"} cleans all descendants of the selected sessions before performing the specified build operation. - \medskip Option @{verbatim "-n"} omits the actual build process + \<^medskip> + Option @{verbatim "-n"} omits the actual build process after the preparatory stage (including optional cleanup). Note that the return code always indicates the status of the set of selected sessions. - \medskip Option @{verbatim "-j"} specifies the maximum number of + \<^medskip> + Option @{verbatim "-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}. - \medskip Option @{verbatim "-s"} enables \emph{system mode}, which + \<^medskip> + Option @{verbatim "-s"} enables \emph{system mode}, which means that resulting heap images and log files are stored in @{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting ISABELLE_HOME_USER}, i.e.\ the user's home directory). - \medskip Option @{verbatim "-v"} increases the general level of + \<^medskip> + Option @{verbatim "-v"} increases the general level of verbosity. Option @{verbatim "-l"} lists the source files that contribute to a session. - \medskip Option @{verbatim "-k"} specifies a newly proposed keyword for + \<^medskip> + Option @{verbatim "-k"} specifies a newly proposed keyword for outer syntax (multiple uses allowed). 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.\ @@ -393,48 +406,56 @@ isabelle build -b HOLCF \end{ttbox} - \smallskip Build the main group of logic images: + \<^smallskip> + Build the main group of logic images: \begin{ttbox} isabelle build -b -g main \end{ttbox} - \smallskip Provide a general overview of the status of all Isabelle + \<^smallskip> + Provide a general overview of the status of all Isabelle sessions, without building anything: \begin{ttbox} isabelle build -a -n -v \end{ttbox} - \smallskip Build all sessions with HTML browser info and PDF + \<^smallskip> + Build all sessions with HTML browser info and PDF document preparation: \begin{ttbox} isabelle build -a -o browser_info -o document=pdf \end{ttbox} - \smallskip Build all sessions with a maximum of 8 parallel prover + \<^smallskip> + Build all sessions with a maximum of 8 parallel prover processes and 4 worker threads each (on a machine with many cores): \begin{ttbox} isabelle build -a -j8 -o threads=4 \end{ttbox} - \smallskip Build some session images with cleanup of their + \<^smallskip> + Build some session images with cleanup of their descendants, while retaining their ancestry: \begin{ttbox} isabelle build -b -c HOL-Algebra HOL-Word \end{ttbox} - \smallskip Clean all sessions without building anything: + \<^smallskip> + Clean all sessions without building anything: \begin{ttbox} isabelle build -a -n -c \end{ttbox} - \smallskip Build all sessions from some other directory hierarchy, + \<^smallskip> + Build all sessions from some other directory hierarchy, according to the settings variable @{verbatim "AFP"} that happens to be defined inside the Isabelle environment: \begin{ttbox} isabelle build -D '$AFP' \end{ttbox} - \smallskip Inform about the status of all sessions required for AFP, + \<^smallskip> + Inform about the status of all sessions required for AFP, without building anything yet: \begin{ttbox} isabelle build -D '$AFP' -R -v -n