# HG changeset patch
# User wenzelm
# Date 1677098432 -3600
# Node ID c1c6f895d9ec501dd60ffbec4185a60d6087a5f9
# Parent  505958b16880944a6613636ecfcf910144f88d27# Parent  5a84de89170dafff68ce0aa3cdc160ab49ab6b94
merged

diff -r 505958b16880 -r c1c6f895d9ec src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/General/json.scala	Wed Feb 22 21:40:32 2023 +0100
@@ -33,6 +33,9 @@
           Some(m.asInstanceOf[Object.T])
         case _ => None
       }
+
+    def parse(s: S): Object.T =
+      unapply(JSON.parse(s)).getOrElse(error("Bad JSON object " + quote(s)))
   }
 
 
diff -r 505958b16880 -r c1c6f895d9ec src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/General/sql.scala	Wed Feb 22 21:40:32 2023 +0100
@@ -55,8 +55,12 @@
   val join_inner: Source = " INNER JOIN "
   def join(outer: Boolean): Source = if (outer) join_outer else join_inner
 
-  def member(x: Source, set: Iterable[String]): Source =
+  def member(x: Source, set: Iterable[String]): Source = {
+    require(set.nonEmpty)
     set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
+  }
+
+  def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set)
 
 
   /* types */
@@ -295,6 +299,8 @@
 
     def is_server: Boolean
 
+    def rebuild(): Unit = ()
+
 
     /* types */
 
@@ -407,6 +413,7 @@
   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
     override def toString: String = name
     override def is_server: Boolean = false
+    override def rebuild(): Unit = using_statement("VACUUM")(_.execute())
 
     def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
 
@@ -419,8 +426,6 @@
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd("INSERT OR IGNORE", sql = sql)
-
-    def rebuild(): Unit = using_statement("VACUUM")(_.execute())
   }
 }
 
diff -r 505958b16880 -r c1c6f895d9ec src/Pure/General/uuid.scala
--- a/src/Pure/General/uuid.scala	Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/General/uuid.scala	Wed Feb 22 21:40:32 2023 +0100
@@ -17,4 +17,7 @@
     catch { case _: IllegalArgumentException => None }
 
   def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
+
+  def make(s: String): T =
+    unapply(s).getOrElse(error("Bad UUID: " + quote(s)))
 }
diff -r 505958b16880 -r c1c6f895d9ec src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/Tools/build_job.scala	Wed Feb 22 21:40:32 2023 +0100
@@ -12,15 +12,23 @@
 
 
 trait Build_Job {
-  def session_name: String
+  def job_name: String
   def numa_node: Option[Int] = None
   def start(): Unit = ()
   def terminate(): Unit = ()
   def is_finished: Boolean = false
   def join: Process_Result = Process_Result.undefined
+  def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, numa_node)
 }
 
 object Build_Job {
+  case class Abstract(
+    override val job_name: String,
+    override val numa_node: Option[Int]
+  ) extends Build_Job {
+    override def make_abstract: Abstract = this
+  }
+
   class Build_Session(progress: Progress,
     session_background: Sessions.Background,
     store: Sessions.Store,
@@ -31,6 +39,8 @@
     override val numa_node: Option[Int]
   ) extends Build_Job {
     def session_name: String = session_background.session_name
+    def job_name: String = session_name
+
     val info: Sessions.Info = session_background.sessions_structure(session_name)
     val options: Options = NUMA.policy_options(info.options, numa_node)
 
diff -r 505958b16880 -r c1c6f895d9ec src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/Tools/build_process.scala	Wed Feb 22 21:40:32 2023 +0100
@@ -152,7 +152,7 @@
 
   /* dynamic state */
 
-  case class Entry(name: String, deps: List[String]) {
+  case class Entry(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) {
     def is_ready: Boolean = deps.isEmpty
     def resolve(dep: String): Entry =
       if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this
@@ -172,8 +172,17 @@
     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 numa_next(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.numa_node) yield i)
+        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))
+      }
 
     def finished: Boolean = pending.isEmpty
 
@@ -183,9 +192,6 @@
 
     def is_running(name: String): Boolean = running.isDefinedAt(name)
 
-    def numa_running: Set[Int] =
-      Set.from(for (job <- running.valuesIterator; i <- job.numa_node) yield i)
-
     def stop_running(): Unit = running.valuesIterator.foreach(_.terminate())
 
     def finished_running(): List[Build_Job.Build_Session] =
@@ -262,31 +268,12 @@
     else None
   }
 
-  protected def next_numa_node(): Option[Int] = synchronized {
-    val available = build_context.numa_nodes.zipWithIndex
-    if (available.isEmpty) None
-    else {
-      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.put_numa((i + 1) % available.length)
-      Some(n)
-    }
-  }
-
   protected def stop_running(): Unit = synchronized { _state.stop_running() }
 
   protected def finished_running(): List[Build_Job.Build_Session] = synchronized {
     _state.finished_running()
   }
 
-  protected def job_running(name: String, job: Build_Job): Build_Job = synchronized {
-    _state = _state.add_running(name, job)
-    job
-  }
-
   protected def finish_job(job: Build_Job.Build_Session): Unit = {
     val session_name = job.session_name
     val process_result = job.join
@@ -407,10 +394,12 @@
 
       val job =
         synchronized {
-          val numa_node = next_numa_node()
-          job_running(session_name,
+          val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
+          val job =
             new Build_Job.Build_Session(progress, session_background, store, do_store,
-              resources, build_context.session_setup, input_heaps, numa_node))
+              resources, build_context.session_setup, input_heaps, numa_node)
+          _state = state1.add_running(session_name, job)
+          job
         }
       job.start()
     }