back to static numa_nodes (reverting part of c2c59de57df9);

--- a/src/Pure/Build/build.scala	Thu Apr 11 12:04:44 2024 +0200
+++ b/src/Pure/Build/build.scala	Thu Apr 11 12:05:01 2024 +0200
@@ -34,6 +34,7 @@
     ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
     hostname: String = Isabelle_System.hostname(),
     numa_shuffling: Boolean = false,
+    numa_nodes: List[Int] = Nil,
     clean_sessions: List[String] = Nil,
     build_heap: Boolean = false,
     fresh_build: Boolean = false,
@@ -249,12 +250,13 @@
       val clean_sessions =
         if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil
 
+      val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
       val build_context =
         Context(store, build_deps, engine = engine, afp_root = afp_root,
           build_hosts = build_hosts, hostname = hostname(build_options),
           clean_sessions = clean_sessions, build_heap = build_heap,
-          numa_shuffling = numa_shuffling, fresh_build = fresh_build,
-          no_build = no_build, session_setup = session_setup,
+          numa_shuffling = numa_shuffling, numa_nodes = numa_nodes,
+          fresh_build = fresh_build, no_build = no_build, session_setup = session_setup,
           jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true)
 
       val results = engine.run_build_process(build_context, progress, server)

--- a/src/Pure/Build/build_process.scala	Thu Apr 11 12:04:44 2024 +0200
+++ b/src/Pure/Build/build_process.scala	Thu Apr 11 12:05:01 2024 +0200
@@ -221,7 +221,6 @@
 
   sealed case class State(
     serial: Long = 0,
-    numa_nodes: List[Int] = Nil,
     sessions: Sessions = Sessions.empty,
     pending: State.Pending = Map.empty,
     running: State.Running = Map.empty,
@@ -1150,7 +1149,8 @@
   protected def next_node_info(state: Build_Process.State, session_name: String): Host.Node_Info = {
     def used_nodes: Set[Int] =
       Set.from(for (job <- state.running.valuesIterator; i <- job.node_info.numa_node) yield i)
-    val numa_node = Host.next_numa_node(_host_database, hostname, state.numa_nodes, used_nodes)
+    val numa_node =
+      Host.next_numa_node(_host_database, hostname, build_context.numa_nodes, used_nodes)
     Host.Node_Info(hostname, numa_node, Nil)
   }
 
@@ -1302,7 +1302,7 @@
       finished || sleep
     }
 
-  protected def init_unsynchronized(): Unit = {
+  protected def init_unsynchronized(): Unit =
     if (build_context.master) {
       val sessions1 =
         _state.sessions.init(build_context, _database_server, progress = build_progress)
@@ -1315,10 +1315,6 @@
       _state = _state.copy(sessions = sessions1, pending = pending1)
     }
 
-    val numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling)
-    _state = _state.copy(numa_nodes = numa_nodes)
-  }
-
   protected def main_unsynchronized(): Unit = {
     for (job <- _state.running.valuesIterator; build <- job.build if build.is_finished) {
       val result = build.join

--- a/src/Pure/Build/build_schedule.scala	Thu Apr 11 12:04:44 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala	Thu Apr 11 12:05:01 2024 +0200
@@ -471,8 +471,9 @@
 
       if (used.length >= host.max_jobs) false
       else {
-        if (host.numa_nodes.length <= 1)
+        if (host.numa_nodes.length <= 1) {
           used.map(host_infos.num_threads).sum + threads <= host.max_threads
+        }
         else {
           def node_threads(n: Int): Int =
             used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum