# HG changeset patch # User wenzelm # Date 1676980402 -3600 # Node ID 1ab68d4370ecffc17ecfc8fea0535cd4bc6cc59a # Parent e9beaaf955bfa44b7dd5762f12bdb83ad5aa3c85 tuned signature; diff -r e9beaaf955bf -r 1ab68d4370ec src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Tue Feb 21 12:50:03 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Tue Feb 21 12:53:22 2023 +0100 @@ -172,6 +172,9 @@ running: Map[String, Build_Job] = Map.empty, results: Map[String, Build_Process.Result] = Map.empty ) { + def get_numa: (Int, Set[Int]) = (numa_index, numa_running) + def put_numa(i: Int): State = copy(numa_index = i) + def finished: Boolean = pending.isEmpty def remove_pending(name: String): State = @@ -263,13 +266,12 @@ val available = build_context.numa_nodes.zipWithIndex if (available.isEmpty) None else { - val used = _state.numa_running - val index = _state.numa_index + val (index, used) = _state.get_numa val candidates = available.drop(index) ::: available.take(index) val (n, i) = candidates.find({ case (n, i) => i == index && !used(n) }) orElse candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head - _state = _state.copy(numa_index = (i + 1) % available.length) + _state = _state.put_numa((i + 1) % available.length) Some(n) } }