clarified database content: store actual value instead of index;

--- a/src/Pure/System/host.scala	Sun Mar 05 18:38:52 2023 +0100
+++ b/src/Pure/System/host.scala	Sun Mar 05 19:21:07 2023 +0100
@@ -98,25 +98,25 @@
 
     object Node_Info {
       val hostname = SQL.Column.string("hostname").make_primary_key
-      val numa_index = SQL.Column.int("numa_index")
+      val numa_next = SQL.Column.int("numa_next")
 
-      val table = make_table("node_info", List(hostname, numa_index))
+      val table = make_table("node_info", List(hostname, numa_next))
     }
 
-    def read_numa_index(db: SQL.Database, hostname: String): Int =
+    def read_numa_next(db: SQL.Database, hostname: String): Int =
       db.using_statement(
-        Node_Info.table.select(List(Node_Info.numa_index),
+        Node_Info.table.select(List(Node_Info.numa_next),
           sql = Node_Info.hostname.where_equal(hostname))
-      )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_index)).nextOption.getOrElse(0))
+      )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_next)).nextOption.getOrElse(0))
 
-    def update_numa_index(db: SQL.Database, hostname: String, numa_index: Int): Boolean =
-      if (read_numa_index(db, hostname) != numa_index) {
+    def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
+      if (read_numa_next(db, hostname) != numa_next) {
         db.using_statement(
           Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname))
         )(_.execute())
         db.using_statement(Node_Info.table.insert()) { stmt =>
           stmt.string(1) = hostname
-          stmt.int(2) = numa_index
+          stmt.int(2) = numa_next
           stmt.execute()
         }
         true

--- a/src/Pure/Tools/build_process.scala	Sun Mar 05 18:38:52 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Mar 05 19:21:07 2023 +0100
@@ -166,7 +166,7 @@
   sealed case class State(
     serial: Long = 0,
     progress_seen: Long = 0,
-    numa_index: Int = 0,
+    numa_next: Int = 0,
     sessions: State.Sessions = Map.empty,   // static build targets
     pending: State.Pending = Nil,           // dynamic build "queue"
     running: State.Running = Map.empty,     // presently running jobs
@@ -183,17 +183,20 @@
       if (message_serial > progress_seen) copy(progress_seen = message_serial)
       else error("Bad serial " + message_serial + " for progress output (already seen)")
 
-    def numa_next(numa_nodes: List[Int]): (Option[Int], State) =
+    def numa_next_node(numa_nodes: List[Int]): (Option[Int], State) =
       if (numa_nodes.isEmpty) (None, this)
       else {
         val available = numa_nodes.zipWithIndex
         val used =
           Set.from(for (job <- running.valuesIterator; i <- job.node_info.numa_node) yield i)
+
+        val numa_index = available.collectFirst({ case (n, i) if n == numa_next => i }).getOrElse(0)
         val candidates = available.drop(numa_index) ::: available.take(numa_index)
         val (n, i) =
           candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse
           candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
-        (Some(n), copy(numa_index = (i + 1) % available.length))
+
+        (Some(n), copy(numa_next = numa_nodes((i + 1) % numa_nodes.length)))
       }
 
     def finished: Boolean = pending.isEmpty
@@ -576,7 +579,7 @@
           update_pending(db, state.pending),
           update_running(db, state.running),
           update_results(db, state.results),
-          Host.Data.update_numa_index(db, hostname, state.numa_index))
+          Host.Data.update_numa_next(db, hostname, state.numa_next))
 
       val serial0 = get_serial(db)
       val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0
@@ -742,7 +745,7 @@
 
       store.init_output(session_name)
 
-      val (numa_node, state1) = state.numa_next(build_context.numa_nodes)
+      val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes)
       val node_info = Host.Node_Info(build_context.hostname, numa_node)
       val job =
         Build_Job.start_session(build_context, progress, log,