1.1 --- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 11:03:44 2012 +0200
1.2 +++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 12:03:48 2012 +0200
1.3 @@ -167,6 +167,7 @@
1.4 Options are:
1.5 -a select all sessions
1.6 -b build heap images
1.7 + -c clean build
1.8 -d DIR include session directory with ROOT file
1.9 -g NAME select session group NAME
1.10 -j INT maximum number of parallel jobs (default 1)
1.11 @@ -221,6 +222,14 @@
1.12 saved for inner nodes of the hierarchy of sessions, as required for
1.13 other sessions to continue later on.
1.14
1.15 + \medskip Option @{verbatim "-c"} cleans all descendants of the
1.16 + selected sessions before performing the specified build operation.
1.17 +
1.18 + \medskip Option @{verbatim "-n"} omits the actual build process
1.19 + after the preparatory stage (including optional cleanup). Note that
1.20 + the return code always indicates the status of the set of selected
1.21 + sessions.
1.22 +
1.23 \medskip Option @{verbatim "-j"} specifies the maximum number of
1.24 parallel build jobs (prover processes). Note that each process is
1.25 subject to a separate limit of parallel threads, cf.\ system option
1.26 @@ -232,10 +241,6 @@
1.27 @{setting ISABELLE_OUTPUT} (which is normally in @{setting
1.28 ISABELLE_HOME_USER}, i.e.\ the user's home directory).
1.29
1.30 - \medskip Option @{verbatim "-n"} omits the actual build process
1.31 - after performing all dependency checks. The return code indicates
1.32 - the status of the set of selected sessions.
1.33 -
1.34 \medskip Option @{verbatim "-v"} enables verbose mode.
1.35 *}
1.36
1.37 @@ -247,30 +252,40 @@
1.38 isabelle build -b HOLCF
1.39 \end{ttbox}
1.40
1.41 - Build the main group of logic images (as determined by the session
1.42 - ROOT specifications of the Isabelle distribution):
1.43 + \smallskip Build the main group of logic images (as determined by
1.44 + the session ROOT specifications of the Isabelle distribution):
1.45 \begin{ttbox}
1.46 isabelle build -b -g main
1.47 \end{ttbox}
1.48
1.49 - Provide a general overview of the status of all Isabelle sessions,
1.50 - without building anything:
1.51 + \smallskip Provide a general overview of the status of all Isabelle
1.52 + sessions, without building anything:
1.53 \begin{ttbox}
1.54 isabelle build -a -n -v
1.55 \end{ttbox}
1.56
1.57 - Build all sessions with HTML browser info and PDF document
1.58 - preparation:
1.59 + \smallskip Build all sessions with HTML browser info and PDF
1.60 + document preparation:
1.61 \begin{ttbox}
1.62 isabelle build -a -o browser_info -o document=pdf
1.63 \end{ttbox}
1.64
1.65 - Build all sessions with a maximum of 8 prover processes and 4
1.66 - threads each (on a machine with many cores):
1.67 -
1.68 + \smallskip Build all sessions with a maximum of 8 prover processes
1.69 + and 4 threads each (on a machine with many cores):
1.70 \begin{ttbox}
1.71 isabelle build -a -j8 -o threads=4
1.72 \end{ttbox}
1.73 +
1.74 + \smallskip Build some session images with cleanup of their
1.75 + descendants, while retaining their ancestry:
1.76 +\begin{ttbox}
1.77 +isabelle build -b -c HOL-Boogie HOL-SPARK
1.78 +\end{ttbox}
1.79 +
1.80 + \smallskip Clean all sessions without building anything:
1.81 +\begin{ttbox}
1.82 +isabelle build -a -n -c
1.83 +\end{ttbox}
1.84 *}
1.85
1.86 end
2.1 --- a/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 11:03:44 2012 +0200
2.2 +++ b/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 12:03:48 2012 +0200
2.3 @@ -277,6 +277,7 @@
2.4 Options are:
2.5 -a select all sessions
2.6 -b build heap images
2.7 + -c clean build
2.8 -d DIR include session directory with ROOT file
2.9 -g NAME select session group NAME
2.10 -j INT maximum number of parallel jobs (default 1)
2.11 @@ -327,6 +328,14 @@
2.12 saved for inner nodes of the hierarchy of sessions, as required for
2.13 other sessions to continue later on.
2.14
2.15 + \medskip Option \verb|-c| cleans all descendants of the
2.16 + selected sessions before performing the specified build operation.
2.17 +
2.18 + \medskip Option \verb|-n| omits the actual build process
2.19 + after the preparatory stage (including optional cleanup). Note that
2.20 + the return code always indicates the status of the set of selected
2.21 + sessions.
2.22 +
2.23 \medskip Option \verb|-j| specifies the maximum number of
2.24 parallel build jobs (prover processes). Note that each process is
2.25 subject to a separate limit of parallel threads, cf.\ system option
2.26 @@ -337,10 +346,6 @@
2.27 \verb|$ISABELLE_HOME/heaps| instead of the default location
2.28 \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).
2.29
2.30 - \medskip Option \verb|-n| omits the actual build process
2.31 - after performing all dependency checks. The return code indicates
2.32 - the status of the set of selected sessions.
2.33 -
2.34 \medskip Option \verb|-v| enables verbose mode.%
2.35 \end{isamarkuptext}%
2.36 \isamarkuptrue%
2.37 @@ -355,29 +360,39 @@
2.38 isabelle build -b HOLCF
2.39 \end{ttbox}
2.40
2.41 - Build the main group of logic images (as determined by the session
2.42 - ROOT specifications of the Isabelle distribution):
2.43 + \smallskip Build the main group of logic images (as determined by
2.44 + the session ROOT specifications of the Isabelle distribution):
2.45 \begin{ttbox}
2.46 isabelle build -b -g main
2.47 \end{ttbox}
2.48
2.49 - Provide a general overview of the status of all Isabelle sessions,
2.50 - without building anything:
2.51 + \smallskip Provide a general overview of the status of all Isabelle
2.52 + sessions, without building anything:
2.53 \begin{ttbox}
2.54 isabelle build -a -n -v
2.55 \end{ttbox}
2.56
2.57 - Build all sessions with HTML browser info and PDF document
2.58 - preparation:
2.59 + \smallskip Build all sessions with HTML browser info and PDF
2.60 + document preparation:
2.61 \begin{ttbox}
2.62 isabelle build -a -o browser_info -o document=pdf
2.63 \end{ttbox}
2.64
2.65 - Build all sessions with a maximum of 8 prover processes and 4
2.66 - threads each (on a machine with many cores):
2.67 -
2.68 + \smallskip Build all sessions with a maximum of 8 prover processes
2.69 + and 4 threads each (on a machine with many cores):
2.70 \begin{ttbox}
2.71 isabelle build -a -j8 -o threads=4
2.72 +\end{ttbox}
2.73 +
2.74 + \smallskip Build some session images with cleanup of their
2.75 + descendants, while retaining their ancestry:
2.76 +\begin{ttbox}
2.77 +isabelle build -b -c HOL-Boogie HOL-SPARK
2.78 +\end{ttbox}
2.79 +
2.80 + \smallskip Clean all sessions without building anything:
2.81 +\begin{ttbox}
2.82 +isabelle build -a -n -c
2.83 \end{ttbox}%
2.84 \end{isamarkuptext}%
2.85 \isamarkuptrue%
3.1 --- a/lib/Tools/build Mon Jul 30 11:03:44 2012 +0200
3.2 +++ b/lib/Tools/build Mon Jul 30 12:03:48 2012 +0200
3.3 @@ -28,6 +28,7 @@
3.4 echo " Options are:"
3.5 echo " -a select all sessions"
3.6 echo " -b build heap images"
3.7 + echo " -c clean build"
3.8 echo " -d DIR include session directory with ROOT file"
3.9 echo " -g NAME select session group NAME"
3.10 echo " -j INT maximum number of parallel jobs (default 1)"
3.11 @@ -58,6 +59,7 @@
3.12
3.13 ALL_SESSIONS=false
3.14 BUILD_HEAP=false
3.15 +CLEAN_BUILD=false
3.16 declare -a MORE_DIRS=()
3.17 declare -a SESSION_GROUPS=()
3.18 MAX_JOBS=1
3.19 @@ -66,7 +68,7 @@
3.20 SYSTEM_MODE=false
3.21 VERBOSE=false
3.22
3.23 -while getopts "abd:g:j:no:sv" OPT
3.24 +while getopts "abcd:g:j:no:sv" OPT
3.25 do
3.26 case "$OPT" in
3.27 a)
3.28 @@ -75,6 +77,9 @@
3.29 b)
3.30 BUILD_HEAP="true"
3.31 ;;
3.32 + c)
3.33 + CLEAN_BUILD="true"
3.34 + ;;
3.35 d)
3.36 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
3.37 ;;
3.38 @@ -121,7 +126,8 @@
3.39 fi
3.40
3.41 "$ISABELLE_TOOL" java isabelle.Build \
3.42 - "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
3.43 + "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
3.44 + "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
3.45 "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
3.46 RC="$?"
3.47
4.1 --- a/src/Pure/System/build.scala Mon Jul 30 11:03:44 2012 +0200
4.2 +++ b/src/Pure/System/build.scala Mon Jul 30 12:03:48 2012 +0200
4.3 @@ -64,14 +64,27 @@
4.4
4.5 def - (name: String): Queue = new Queue(graph.del_node(name))
4.6
4.7 - def required(groups: List[String], names: List[String]): Queue =
4.8 + def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
4.9 + : (List[String], Queue) =
4.10 {
4.11 - val selected_group = groups.toSet
4.12 - val selected_name = names.toSet
4.13 + sessions.filterNot(isDefinedAt(_)) match {
4.14 + case Nil =>
4.15 + case bad => error("Undefined session(s): " + commas_quote(bad))
4.16 + }
4.17 +
4.18 val selected =
4.19 - graph.keys.filter(name =>
4.20 - selected_name(name) || apply(name).groups.exists(selected_group)).toList
4.21 - new Queue(graph.restrict(graph.all_preds(selected).toSet))
4.22 + {
4.23 + if (all_sessions) graph.keys.toList
4.24 + else {
4.25 + val sel_group = session_groups.toSet
4.26 + val sel = sessions.toSet
4.27 + graph.keys.toList.filter(name =>
4.28 + sel(name) || apply(name).groups.exists(sel_group)).toList
4.29 + }
4.30 + }
4.31 + val descendants = graph.all_succs(selected)
4.32 + val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet))
4.33 + (descendants, queue1)
4.34 }
4.35
4.36 def dequeue(skip: String => Boolean): Option[(String, Info)] =
4.37 @@ -83,7 +96,7 @@
4.38 }
4.39
4.40 def topological_order: List[(String, Info)] =
4.41 - graph.topological_order.map(name => (name, graph.get_node(name)))
4.42 + graph.topological_order.map(name => (name, apply(name)))
4.43 }
4.44 }
4.45
4.46 @@ -232,8 +245,7 @@
4.47 })
4.48 }
4.49
4.50 - def find_sessions(options: Options, more_dirs: List[Path],
4.51 - all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
4.52 + def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue =
4.53 {
4.54 var queue = Session.Queue.empty
4.55
4.56 @@ -246,12 +258,7 @@
4.57
4.58 for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
4.59
4.60 - sessions.filter(name => !queue.isDefinedAt(name)) match {
4.61 - case Nil =>
4.62 - case bad => error("Undefined session(s): " + commas_quote(bad))
4.63 - }
4.64 -
4.65 - if (all_sessions) queue else queue.required(session_groups, sessions)
4.66 + queue
4.67 }
4.68
4.69
4.70 @@ -439,6 +446,7 @@
4.71 def build(
4.72 all_sessions: Boolean = false,
4.73 build_heap: Boolean = false,
4.74 + clean_build: Boolean = false,
4.75 more_dirs: List[Path] = Nil,
4.76 session_groups: List[String] = Nil,
4.77 max_jobs: Int = 1,
4.78 @@ -449,7 +457,8 @@
4.79 sessions: List[String] = Nil): Int =
4.80 {
4.81 val options = (Options.init() /: build_options)(_.define_simple(_))
4.82 - val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
4.83 + val (descendants, queue) =
4.84 + find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
4.85 val deps = dependencies(verbose, queue)
4.86
4.87 def make_stamp(name: String): String =
4.88 @@ -469,6 +478,16 @@
4.89 // prepare log dir
4.90 (output_dir + LOG).file.mkdirs()
4.91
4.92 + // optional cleanup
4.93 + if (clean_build) {
4.94 + for (name <- descendants) {
4.95 + val files =
4.96 + List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
4.97 + if (!files.isEmpty) echo("Cleaning " + name + " ...")
4.98 + if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
4.99 + }
4.100 + }
4.101 +
4.102 // scheduler loop
4.103 @tailrec def loop(
4.104 pending: Session.Queue,
4.105 @@ -571,13 +590,14 @@
4.106 case
4.107 Properties.Value.Boolean(all_sessions) ::
4.108 Properties.Value.Boolean(build_heap) ::
4.109 + Properties.Value.Boolean(clean_build) ::
4.110 Properties.Value.Int(max_jobs) ::
4.111 Properties.Value.Boolean(no_build) ::
4.112 Properties.Value.Boolean(system_mode) ::
4.113 Properties.Value.Boolean(verbose) ::
4.114 Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
4.115 - build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
4.116 - max_jobs, no_build, build_options, system_mode, verbose, sessions)
4.117 + build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
4.118 + session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
4.119 case _ => error("Bad arguments:\n" + cat_lines(args))
4.120 }
4.121 }