more robust ancestor_results: avoid total existence failure after build_process has crashed elsewhere;
--- a/src/Pure/Tools/build_process.scala Thu Aug 10 11:29:11 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Thu Aug 10 12:15:40 2023 +0200
@@ -77,6 +77,7 @@
final class Sessions private(val graph: Sessions.Graph) {
override def toString: String = graph.toString
+ def defined(name: String): Boolean = graph.defined(name)
def apply(name: String): Build_Job.Session_Context = graph.get_node(name)
def iterator: Iterator[Build_Job.Session_Context] =
@@ -248,6 +249,13 @@
Result(name, worker_uuid, build_uuid, node_info, process_result, output_shasum, current)
copy(results = results + (name -> result))
}
+
+ def ancestor_results(name: String): Option[List[Result]] = {
+ val defined =
+ sessions.defined(name) &&
+ sessions(name).ancestors.forall(a => sessions.defined(a) && results.isDefinedAt(a))
+ if (defined) Some(sessions(name).ancestors.map(results)) else None
+ }
}
@@ -957,10 +965,11 @@
else Nil
}
- protected def start_session(state: Build_Process.State, session_name: String): Build_Process.State = {
- val ancestor_results =
- for (a <- state.sessions(session_name).ancestors) yield state.results(a)
-
+ protected def start_session(
+ state: Build_Process.State,
+ session_name: String,
+ ancestor_results: List[Build_Process.Result]
+ ): Build_Process.State = {
val sources_shasum = state.sessions(session_name).sources_shasum
val input_shasum =
@@ -1083,7 +1092,12 @@
val jobs = next_jobs(_state)
for (name <- jobs) {
if (is_session_name(name)) {
- _state = start_session(_state, name)
+ _state.ancestor_results(name) match {
+ case Some(results) => _state = start_session(_state, name, results)
+ case None =>
+ build_progress.echo_warning(
+ "Broken build job " + quote(name) + ": no ancestor results")
+ }
}
else build_progress.echo_warning("Unsupported build job " + quote(name))
}