1.1 --- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 10:59:33 2012 +0200
1.2 +++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 12:04:37 2012 +0200
1.3 @@ -167,8 +167,8 @@
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 - -f fresh build
1.10 -g NAME select session group NAME
1.11 -j INT maximum number of parallel jobs (default 1)
1.12 -n no build -- test dependencies only
1.13 @@ -222,8 +222,13 @@
1.14 saved for inner nodes of the hierarchy of sessions, as required for
1.15 other sessions to continue later on.
1.16
1.17 - \medskip Option @{verbatim "-f"} ensures a fresh build, even if all
1.18 - results are up-to-date wrt.\ the current set of sources.
1.19 + \medskip Option @{verbatim "-c"} cleans all descendants of the
1.20 + selected sessions before performing the specified build operation.
1.21 +
1.22 + \medskip Option @{verbatim "-n"} omits the actual build process
1.23 + after the preparatory stage (including optional cleanup). Note that
1.24 + the return code always indicates the status of the set of selected
1.25 + sessions.
1.26
1.27 \medskip Option @{verbatim "-j"} specifies the maximum number of
1.28 parallel build jobs (prover processes). Note that each process is
1.29 @@ -236,10 +241,6 @@
1.30 @{setting ISABELLE_OUTPUT} (which is normally in @{setting
1.31 ISABELLE_HOME_USER}, i.e.\ the user's home directory).
1.32
1.33 - \medskip Option @{verbatim "-n"} omits the actual build process
1.34 - after performing all dependency checks. The return code indicates
1.35 - the status of the set of selected sessions.
1.36 -
1.37 \medskip Option @{verbatim "-v"} enables verbose mode.
1.38 *}
1.39
1.40 @@ -251,30 +252,40 @@
1.41 isabelle build -b HOLCF
1.42 \end{ttbox}
1.43
1.44 - Build the main group of logic images (as determined by the session
1.45 - ROOT specifications of the Isabelle distribution):
1.46 + \smallskip Build the main group of logic images (as determined by
1.47 + the session ROOT specifications of the Isabelle distribution):
1.48 \begin{ttbox}
1.49 isabelle build -b -g main
1.50 \end{ttbox}
1.51
1.52 - Provide a general overview of the status of all Isabelle sessions,
1.53 - without building anything:
1.54 + \smallskip Provide a general overview of the status of all Isabelle
1.55 + sessions, without building anything:
1.56 \begin{ttbox}
1.57 isabelle build -a -n -v
1.58 \end{ttbox}
1.59
1.60 - Build all sessions with HTML browser info and PDF document
1.61 - preparation:
1.62 + \smallskip Build all sessions with HTML browser info and PDF
1.63 + document preparation:
1.64 \begin{ttbox}
1.65 isabelle build -a -o browser_info -o document=pdf
1.66 \end{ttbox}
1.67
1.68 - Build all sessions with a maximum of 8 prover processes and 4
1.69 - threads each (on a machine with many cores):
1.70 -
1.71 + \smallskip Build all sessions with a maximum of 8 prover processes
1.72 + and 4 threads each (on a machine with many cores):
1.73 \begin{ttbox}
1.74 isabelle build -a -j8 -o threads=4
1.75 \end{ttbox}
1.76 +
1.77 + \smallskip Build some session images with cleanup of their
1.78 + descendants, while retaining their ancestry:
1.79 +\begin{ttbox}
1.80 +isabelle build -b -c HOL-Boogie HOL-SPARK
1.81 +\end{ttbox}
1.82 +
1.83 + \smallskip Clean all sessions without building anything:
1.84 +\begin{ttbox}
1.85 +isabelle build -a -n -c
1.86 +\end{ttbox}
1.87 *}
1.88
1.89 end
2.1 --- a/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 10:59:33 2012 +0200
2.2 +++ b/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 12:04:37 2012 +0200
2.3 @@ -277,8 +277,8 @@
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 - -f fresh build
2.10 -g NAME select session group NAME
2.11 -j INT maximum number of parallel jobs (default 1)
2.12 -n no build -- test dependencies only
2.13 @@ -328,8 +328,13 @@
2.14 saved for inner nodes of the hierarchy of sessions, as required for
2.15 other sessions to continue later on.
2.16
2.17 - \medskip Option \verb|-f| ensures a fresh build, even if all
2.18 - results are up-to-date wrt.\ the current set of sources.
2.19 + \medskip Option \verb|-c| cleans all descendants of the
2.20 + selected sessions before performing the specified build operation.
2.21 +
2.22 + \medskip Option \verb|-n| omits the actual build process
2.23 + after the preparatory stage (including optional cleanup). Note that
2.24 + the return code always indicates the status of the set of selected
2.25 + sessions.
2.26
2.27 \medskip Option \verb|-j| specifies the maximum number of
2.28 parallel build jobs (prover processes). Note that each process is
2.29 @@ -341,10 +346,6 @@
2.30 \verb|$ISABELLE_HOME/heaps| instead of the default location
2.31 \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.32
2.33 - \medskip Option \verb|-n| omits the actual build process
2.34 - after performing all dependency checks. The return code indicates
2.35 - the status of the set of selected sessions.
2.36 -
2.37 \medskip Option \verb|-v| enables verbose mode.%
2.38 \end{isamarkuptext}%
2.39 \isamarkuptrue%
2.40 @@ -359,29 +360,39 @@
2.41 isabelle build -b HOLCF
2.42 \end{ttbox}
2.43
2.44 - Build the main group of logic images (as determined by the session
2.45 - ROOT specifications of the Isabelle distribution):
2.46 + \smallskip Build the main group of logic images (as determined by
2.47 + the session ROOT specifications of the Isabelle distribution):
2.48 \begin{ttbox}
2.49 isabelle build -b -g main
2.50 \end{ttbox}
2.51
2.52 - Provide a general overview of the status of all Isabelle sessions,
2.53 - without building anything:
2.54 + \smallskip Provide a general overview of the status of all Isabelle
2.55 + sessions, without building anything:
2.56 \begin{ttbox}
2.57 isabelle build -a -n -v
2.58 \end{ttbox}
2.59
2.60 - Build all sessions with HTML browser info and PDF document
2.61 - preparation:
2.62 + \smallskip Build all sessions with HTML browser info and PDF
2.63 + document preparation:
2.64 \begin{ttbox}
2.65 isabelle build -a -o browser_info -o document=pdf
2.66 \end{ttbox}
2.67
2.68 - Build all sessions with a maximum of 8 prover processes and 4
2.69 - threads each (on a machine with many cores):
2.70 -
2.71 + \smallskip Build all sessions with a maximum of 8 prover processes
2.72 + and 4 threads each (on a machine with many cores):
2.73 \begin{ttbox}
2.74 isabelle build -a -j8 -o threads=4
2.75 +\end{ttbox}
2.76 +
2.77 + \smallskip Build some session images with cleanup of their
2.78 + descendants, while retaining their ancestry:
2.79 +\begin{ttbox}
2.80 +isabelle build -b -c HOL-Boogie HOL-SPARK
2.81 +\end{ttbox}
2.82 +
2.83 + \smallskip Clean all sessions without building anything:
2.84 +\begin{ttbox}
2.85 +isabelle build -a -n -c
2.86 \end{ttbox}%
2.87 \end{isamarkuptext}%
2.88 \isamarkuptrue%
3.1 --- a/lib/Tools/build Mon Jul 30 10:59:33 2012 +0200
3.2 +++ b/lib/Tools/build Mon Jul 30 12:04:37 2012 +0200
3.3 @@ -28,8 +28,8 @@
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 " -f fresh build"
3.10 echo " -g NAME select session group NAME"
3.11 echo " -j INT maximum number of parallel jobs (default 1)"
3.12 echo " -n no build -- test dependencies only"
3.13 @@ -59,8 +59,8 @@
3.14
3.15 ALL_SESSIONS=false
3.16 BUILD_HEAP=false
3.17 +CLEAN_BUILD=false
3.18 declare -a MORE_DIRS=()
3.19 -FRESH_BUILD=false
3.20 declare -a SESSION_GROUPS=()
3.21 MAX_JOBS=1
3.22 NO_BUILD=false
3.23 @@ -68,7 +68,7 @@
3.24 SYSTEM_MODE=false
3.25 VERBOSE=false
3.26
3.27 -while getopts "abd:fg:j:no:sv" OPT
3.28 +while getopts "abcd:g:j:no:sv" OPT
3.29 do
3.30 case "$OPT" in
3.31 a)
3.32 @@ -77,12 +77,12 @@
3.33 b)
3.34 BUILD_HEAP="true"
3.35 ;;
3.36 + c)
3.37 + CLEAN_BUILD="true"
3.38 + ;;
3.39 d)
3.40 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
3.41 ;;
3.42 - f)
3.43 - FRESH_BUILD="true"
3.44 - ;;
3.45 g)
3.46 SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
3.47 ;;
3.48 @@ -126,7 +126,8 @@
3.49 fi
3.50
3.51 "$ISABELLE_TOOL" java isabelle.Build \
3.52 - "$ALL_SESSIONS" "$BUILD_HEAP" "$FRESH_BUILD" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
3.53 + "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
3.54 + "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
3.55 "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
3.56 RC="$?"
3.57
4.1 --- a/src/Pure/System/build.scala Mon Jul 30 10:59:33 2012 +0200
4.2 +++ b/src/Pure/System/build.scala Mon Jul 30 12:04:37 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,8 +446,8 @@
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 - fresh_build: Boolean,
4.77 session_groups: List[String] = Nil,
4.78 max_jobs: Int = 1,
4.79 no_build: Boolean = false,
4.80 @@ -450,7 +457,8 @@
4.81 sessions: List[String] = Nil): Int =
4.82 {
4.83 val options = (Options.init() /: build_options)(_.define_simple(_))
4.84 - val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
4.85 + val (descendants, queue) =
4.86 + find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
4.87 val deps = dependencies(verbose, queue)
4.88
4.89 def make_stamp(name: String): String =
4.90 @@ -470,6 +478,16 @@
4.91 // prepare log dir
4.92 (output_dir + LOG).file.mkdirs()
4.93
4.94 + // optional cleanup
4.95 + if (clean_build) {
4.96 + for (name <- descendants) {
4.97 + val files =
4.98 + List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
4.99 + if (!files.isEmpty) echo("Cleaning " + name + " ...")
4.100 + if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
4.101 + }
4.102 + }
4.103 +
4.104 // scheduler loop
4.105 @tailrec def loop(
4.106 pending: Session.Queue,
4.107 @@ -524,7 +542,7 @@
4.108 case None => false
4.109 }
4.110 }
4.111 - val all_current = current && parent_current && !fresh_build
4.112 + val all_current = current && parent_current
4.113
4.114 if (all_current)
4.115 loop(pending - name, running, results + (name -> (true, 0)))
4.116 @@ -572,13 +590,13 @@
4.117 case
4.118 Properties.Value.Boolean(all_sessions) ::
4.119 Properties.Value.Boolean(build_heap) ::
4.120 - Properties.Value.Boolean(fresh_build) ::
4.121 + Properties.Value.Boolean(clean_build) ::
4.122 Properties.Value.Int(max_jobs) ::
4.123 Properties.Value.Boolean(no_build) ::
4.124 Properties.Value.Boolean(system_mode) ::
4.125 Properties.Value.Boolean(verbose) ::
4.126 Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
4.127 - build(all_sessions, build_heap, more_dirs.map(Path.explode), fresh_build,
4.128 + build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
4.129 session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
4.130 case _ => error("Bad arguments:\n" + cat_lines(args))
4.131 }