--- a/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 11:03:44 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 12:03:48 2012 +0200
@@ -277,6 +277,7 @@
Options are:
-a select all sessions
-b build heap images
+ -c clean build
-d DIR include session directory with ROOT file
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
@@ -327,6 +328,14 @@
saved for inner nodes of the hierarchy of sessions, as required for
other sessions to continue later on.
+ \medskip Option \verb|-c| cleans all descendants of the
+ selected sessions before performing the specified build operation.
+
+ \medskip Option \verb|-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 \verb|-j| specifies the maximum number of
parallel build jobs (prover processes). Note that each process is
subject to a separate limit of parallel threads, cf.\ system option
@@ -337,10 +346,6 @@
\verb|$ISABELLE_HOME/heaps| instead of the default location
\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} (which is normally in \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}, i.e.\ the user's home directory).
- \medskip Option \verb|-n| omits the actual build process
- after performing all dependency checks. The return code indicates
- the status of the set of selected sessions.
-
\medskip Option \verb|-v| enables verbose mode.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -355,29 +360,39 @@
isabelle build -b HOLCF
\end{ttbox}
- Build the main group of logic images (as determined by the session
- ROOT specifications of the Isabelle distribution):
+ \smallskip Build the main group of logic images (as determined by
+ the session ROOT specifications of the Isabelle distribution):
\begin{ttbox}
isabelle build -b -g main
\end{ttbox}
- Provide a general overview of the status of all Isabelle sessions,
- without building anything:
+ \smallskip Provide a general overview of the status of all Isabelle
+ sessions, without building anything:
\begin{ttbox}
isabelle build -a -n -v
\end{ttbox}
- Build all sessions with HTML browser info and PDF document
- preparation:
+ \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}
- Build all sessions with a maximum of 8 prover processes and 4
- threads each (on a machine with many cores):
-
+ \smallskip Build all sessions with a maximum of 8 prover processes
+ and 4 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
+ descendants, while retaining their ancestry:
+\begin{ttbox}
+isabelle build -b -c HOL-Boogie HOL-SPARK
+\end{ttbox}
+
+ \smallskip Clean all sessions without building anything:
+\begin{ttbox}
+isabelle build -a -n -c
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%