# HG changeset patch # User wenzelm # Date 1676283901 -3600 # Node ID e9f1fcb9b358b7be1fea7d9401fbd179b2475c2f # Parent d060545f01a29e8ed95dc07b8120e4f213cb7fab tuned signature: explicit marker for mutable global state; diff -r d060545f01a2 -r e9f1fcb9b358 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Mon Feb 13 10:49:33 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Mon Feb 13 11:25:01 2023 +0100 @@ -168,24 +168,24 @@ } // global state - private val numa_nodes = new NUMA.Nodes(numa_shuffling) - private var build_graph = build_context.sessions_structure.build_graph - private var build_order = SortedSet.from(build_graph.keys)(build_context.ordering) - private var running = Map.empty[String, Build_Job] - private var results = Map.empty[String, Build_Process.Result] + private val _numa_nodes = new NUMA.Nodes(numa_shuffling) + private var _build_graph = build_context.sessions_structure.build_graph + private var _build_order = SortedSet.from(_build_graph.keys)(build_context.ordering) + private var _running = Map.empty[String, Build_Job] + private var _results = Map.empty[String, Build_Process.Result] private def remove_pending(name: String): Unit = { - build_graph = build_graph.del_node(name) - build_order = build_order - name + _build_graph = _build_graph.del_node(name) + _build_order = _build_order - name } private def next_pending(): Option[String] = - build_order.iterator - .dropWhile(name => running.isDefinedAt(name) || !build_graph.is_minimal(name)) + _build_order.iterator + .dropWhile(name => _running.isDefinedAt(name) || !_build_graph.is_minimal(name)) .nextOption() private def used_node(i: Int): Boolean = - running.valuesIterator.exists(job => job.numa_node.isDefined && job.numa_node.get == i) + _running.valuesIterator.exists(job => job.numa_node.isDefined && job.numa_node.get == i) private def session_finished(session_name: String, process_result: Process_Result): String = "Finished " + session_name + " (" + process_result.timing.message_resources + ")" @@ -251,14 +251,14 @@ } remove_pending(session_name) - running -= session_name - results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail)) + _running -= session_name + _results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail)) } private def start_job(session_name: String): Unit = { val ancestor_results = build_deps.sessions_structure.build_requirements(List(session_name)). - filterNot(_ == session_name).map(results(_)) + filterNot(_ == session_name).map(_results(_)) val input_heaps = if (ancestor_results.isEmpty) { SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) @@ -289,12 +289,12 @@ if (all_current) { remove_pending(session_name) - results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok)) + _results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok)) } else if (no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") remove_pending(session_name) - results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error)) + _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error)) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") @@ -308,16 +308,16 @@ new Resources(session_background, log = log, command_timings = build_context(session_name).old_command_timings) - val numa_node = numa_nodes.next(used_node) + val numa_node = _numa_nodes.next(used_node) val job = new Build_Job(progress, session_background, store, do_store, resources, session_setup, input_heaps, numa_node) - running += (session_name -> job) + _running += (session_name -> job) } else { progress.echo(session_name + " CANCELLED") remove_pending(session_name) - results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined)) + _results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined)) } } @@ -327,12 +327,12 @@ } def run(): Map[String, Build_Process.Result] = { - while (!build_graph.is_empty) { - if (progress.stopped) running.valuesIterator.foreach(_.terminate()) + while (!_build_graph.is_empty) { + if (progress.stopped) _running.valuesIterator.foreach(_.terminate()) - running.find({ case (_, job) => job.is_finished }) match { + _running.find({ case (_, job) => job.is_finished }) match { case Some((session_name, job)) => finish_job(session_name, job) - case None if running.size < (max_jobs max 1) => + case None if _running.size < (max_jobs max 1) => next_pending() match { case Some(session_name) => start_job(session_name) case None => sleep() @@ -341,6 +341,6 @@ } } - results + _results } }