# HG changeset patch
# User wenzelm
# Date 1678284906 -3600
# Node ID 42922317b6764f3137c1461f9e061fc2488ffa28
# Parent  9af2afc3f7b34b7e0f53efffa9e3f86e619c91f9
more database content, e.g. for monitoring;

diff -r 9af2afc3f7b3 -r 42922317b676 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 14:45:17 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 15:15:06 2023 +0100
@@ -162,6 +162,9 @@
   case class Worker(
     worker_uuid: String,
     build_uuid: String,
+    hostname: String,
+    java_pid: Long,
+    java_start: Option[Date],
     start: Date,
     stamp: Date,
     stop: Option[Date],
@@ -448,12 +451,16 @@
     object Workers {
       val worker_uuid = Generic.worker_uuid.make_primary_key
       val build_uuid = Generic.build_uuid
+      val hostname = SQL.Column.string("hostname")
+      val java_pid = SQL.Column.long("java_pid")
+      val java_start = SQL.Column.date("java_start")
       val start = SQL.Column.date("start")
       val stamp = SQL.Column.date("stamp")
       val stop = SQL.Column.date("stop")
       val serial = SQL.Column.long("serial")
 
-      val table = make_table("workers", List(worker_uuid, build_uuid, start, stamp, stop, serial))
+      val table = make_table("workers",
+        List(worker_uuid, build_uuid, hostname, java_pid, java_start, start, stamp, stop, serial))
 
       val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
     }
@@ -464,7 +471,14 @@
         res => res.long(Workers.serial)
       ).getOrElse(0L)
 
-    def start_worker(db: SQL.Database, worker_uuid: String, build_uuid: String): Long = {
+    def start_worker(
+      db: SQL.Database,
+      worker_uuid: String,
+      build_uuid: String,
+      hostname: String,
+      java_pid: Long,
+      java_start: Option[Date]
+    ): Long = {
       def err(msg: String): Nothing =
         error("Cannot start worker " + worker_uuid + if_proper(msg, "\n" + msg))
 
@@ -486,10 +500,13 @@
           val now = db.now()
           stmt.string(1) = worker_uuid
           stmt.string(2) = build_uuid
-          stmt.date(3) = now
-          stmt.date(4) = now
-          stmt.date(5) = None
-          stmt.long(6) = serial
+          stmt.string(3) = hostname
+          stmt.long(4) = java_pid
+          stmt.date(5) = java_start
+          stmt.date(6) = now
+          stmt.date(7) = now
+          stmt.date(8) = None
+          stmt.long(9) = serial
         })
       serial
     }
@@ -525,6 +542,9 @@
             Worker(
               worker_uuid = res.string(Workers.worker_uuid),
               build_uuid = res.string(Workers.build_uuid),
+              hostname = res.string(Workers.hostname),
+              java_pid = res.long(Workers.java_pid),
+              java_start = res.get_date(Workers.java_start),
               start = res.date(Workers.start),
               stamp = res.date(Workers.stamp),
               stop = res.get_date(Workers.stop),
@@ -912,7 +932,13 @@
 
   final def start_worker(): Unit = synchronized_database {
     for (db <- _database) {
-      val serial = Build_Process.Data.start_worker(db, worker_uuid, build_uuid)
+      val java = ProcessHandle.current()
+      val java_pid = java.pid
+      val java_start0 = java.info.startInstant
+      val java_start = if (java_start0.isPresent) Some(Date.instant(java_start0.get)) else None
+      val serial =
+        Build_Process.Data.start_worker(
+          db, worker_uuid, build_uuid, build_context.hostname, java_pid, java_start)
       _state = _state.set_serial(serial)
     }
   }