more database content;
authorwenzelm
Mon, 13 Mar 2023 19:04:16 +0100
changeset 77634 50fc9143ccfa
parent 77633 a65b39fdf8b6
child 77635 dcd2c3bb4b68
more database content;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 13 18:53:14 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 13 19:04:16 2023 +0100
@@ -168,6 +168,7 @@
   case class Job(
     name: String,
     worker_uuid: String,
+    build_uuid: String,
     node_info: Host.Node_Info,
     build: Option[Build_Job]
   ) {
@@ -609,10 +610,11 @@
     object Running {
       val name = Generic.name.make_primary_key
       val worker_uuid = Generic.worker_uuid
+      val build_uuid = Generic.build_uuid
       val hostname = SQL.Column.string("hostname")
       val numa_node = SQL.Column.int("numa_node")
 
-      val table = make_table("running", List(name, worker_uuid, hostname, numa_node))
+      val table = make_table("running", List(name, worker_uuid, build_uuid, hostname, numa_node))
     }
 
     def read_running(db: SQL.Database): List[Job] =
@@ -622,9 +624,10 @@
         { res =>
           val name = res.string(Running.name)
           val worker_uuid = res.string(Running.worker_uuid)
+          val build_uuid = res.string(Running.build_uuid)
           val hostname = res.string(Running.hostname)
           val numa_node = res.get_int(Running.numa_node)
-          Job(name, worker_uuid, Host.Node_Info(hostname, numa_node), None)
+          Job(name, worker_uuid, build_uuid, Host.Node_Info(hostname, numa_node), None)
         }
       )
 
@@ -644,8 +647,9 @@
           { stmt =>
             stmt.string(1) = job.name
             stmt.string(2) = job.worker_uuid
-            stmt.string(3) = job.node_info.hostname
-            stmt.int(4) = job.node_info.numa_node
+            stmt.string(3) = job.build_uuid
+            stmt.string(4) = job.node_info.hostname
+            stmt.int(5) = job.node_info.numa_node
           })
       }
 
@@ -922,7 +926,9 @@
         Build_Job.start_session(build_context, progress, log,
           build_deps.background(session_name), input_shasum, node_info)
 
-      state1.add_running(Build_Process.Job(session_name, worker_uuid, node_info, Some(build)))
+      val job = Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, Some(build))
+
+      state1.add_running(job)
     }
   }