--- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 11:03:44 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 12:03:48 2012 +0200
@@ -167,6 +167,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)
@@ -221,6 +222,14 @@
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
+ selected sessions before performing the specified build operation.
+
+ \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
parallel build jobs (prover processes). Note that each process is
subject to a separate limit of parallel threads, cf.\ system option
@@ -232,10 +241,6 @@
@{setting ISABELLE_OUTPUT} (which is normally in @{setting
ISABELLE_HOME_USER}, i.e.\ the user's home directory).
- \medskip Option @{verbatim "-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 @{verbatim "-v"} enables verbose mode.
*}
@@ -247,30 +252,40 @@
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
--- 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%
--- a/lib/Tools/build Mon Jul 30 11:03:44 2012 +0200
+++ b/lib/Tools/build Mon Jul 30 12:03:48 2012 +0200
@@ -28,6 +28,7 @@
echo " Options are:"
echo " -a select all sessions"
echo " -b build heap images"
+ echo " -c clean build"
echo " -d DIR include session directory with ROOT file"
echo " -g NAME select session group NAME"
echo " -j INT maximum number of parallel jobs (default 1)"
@@ -58,6 +59,7 @@
ALL_SESSIONS=false
BUILD_HEAP=false
+CLEAN_BUILD=false
declare -a MORE_DIRS=()
declare -a SESSION_GROUPS=()
MAX_JOBS=1
@@ -66,7 +68,7 @@
SYSTEM_MODE=false
VERBOSE=false
-while getopts "abd:g:j:no:sv" OPT
+while getopts "abcd:g:j:no:sv" OPT
do
case "$OPT" in
a)
@@ -75,6 +77,9 @@
b)
BUILD_HEAP="true"
;;
+ c)
+ CLEAN_BUILD="true"
+ ;;
d)
MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
;;
@@ -121,7 +126,8 @@
fi
"$ISABELLE_TOOL" java isabelle.Build \
- "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
+ "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
+ "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
"${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
RC="$?"
--- a/src/Pure/System/build.scala Mon Jul 30 11:03:44 2012 +0200
+++ b/src/Pure/System/build.scala Mon Jul 30 12:03:48 2012 +0200
@@ -64,14 +64,27 @@
def - (name: String): Queue = new Queue(graph.del_node(name))
- def required(groups: List[String], names: List[String]): Queue =
+ def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
+ : (List[String], Queue) =
{
- val selected_group = groups.toSet
- val selected_name = names.toSet
+ sessions.filterNot(isDefinedAt(_)) match {
+ case Nil =>
+ case bad => error("Undefined session(s): " + commas_quote(bad))
+ }
+
val selected =
- graph.keys.filter(name =>
- selected_name(name) || apply(name).groups.exists(selected_group)).toList
- new Queue(graph.restrict(graph.all_preds(selected).toSet))
+ {
+ if (all_sessions) graph.keys.toList
+ else {
+ val sel_group = session_groups.toSet
+ val sel = sessions.toSet
+ graph.keys.toList.filter(name =>
+ sel(name) || apply(name).groups.exists(sel_group)).toList
+ }
+ }
+ val descendants = graph.all_succs(selected)
+ val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet))
+ (descendants, queue1)
}
def dequeue(skip: String => Boolean): Option[(String, Info)] =
@@ -83,7 +96,7 @@
}
def topological_order: List[(String, Info)] =
- graph.topological_order.map(name => (name, graph.get_node(name)))
+ graph.topological_order.map(name => (name, apply(name)))
}
}
@@ -232,8 +245,7 @@
})
}
- def find_sessions(options: Options, more_dirs: List[Path],
- all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
+ def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue =
{
var queue = Session.Queue.empty
@@ -246,12 +258,7 @@
for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
- sessions.filter(name => !queue.isDefinedAt(name)) match {
- case Nil =>
- case bad => error("Undefined session(s): " + commas_quote(bad))
- }
-
- if (all_sessions) queue else queue.required(session_groups, sessions)
+ queue
}
@@ -439,6 +446,7 @@
def build(
all_sessions: Boolean = false,
build_heap: Boolean = false,
+ clean_build: Boolean = false,
more_dirs: List[Path] = Nil,
session_groups: List[String] = Nil,
max_jobs: Int = 1,
@@ -449,7 +457,8 @@
sessions: List[String] = Nil): Int =
{
val options = (Options.init() /: build_options)(_.define_simple(_))
- val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
+ val (descendants, queue) =
+ find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
val deps = dependencies(verbose, queue)
def make_stamp(name: String): String =
@@ -469,6 +478,16 @@
// prepare log dir
(output_dir + LOG).file.mkdirs()
+ // optional cleanup
+ if (clean_build) {
+ for (name <- descendants) {
+ val files =
+ List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
+ if (!files.isEmpty) echo("Cleaning " + name + " ...")
+ if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
+ }
+ }
+
// scheduler loop
@tailrec def loop(
pending: Session.Queue,
@@ -571,13 +590,14 @@
case
Properties.Value.Boolean(all_sessions) ::
Properties.Value.Boolean(build_heap) ::
+ Properties.Value.Boolean(clean_build) ::
Properties.Value.Int(max_jobs) ::
Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
Properties.Value.Boolean(verbose) ::
Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
- build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
- max_jobs, no_build, build_options, system_mode, verbose, sessions)
+ build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
+ session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}