--- 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.\<close>
@@ -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.
\<close>
@@ -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):
--- 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.
\<close>
@@ -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.
\<close>
@@ -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!\<close>
@@ -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.\<close>
@@ -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}
--- 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.\<close>
+
section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
text \<open>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.\<close>
@@ -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
--- 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.\<close>
@@ -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