# 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) } }