# HG changeset patch # User wenzelm # Date 1678287029 -3600 # Node ID 8036d5f129971aa9664275daa068ad6b326a82e5 # Parent 80021d645a01699ef141b763bacb9a28326cf0da more database content, e.g. for monitoring; diff -r 80021d645a01 -r 8036d5f12997 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Wed Mar 08 15:25:55 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Wed Mar 08 15:50:29 2023 +0100 @@ -12,11 +12,12 @@ trait Build_Job { def job_name: String + def worker_uuid: String def node_info: Host.Node_Info def cancel(): Unit = () def is_finished: Boolean = false def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) - def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info) + def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, worker_uuid, node_info) } object Build_Job { @@ -26,6 +27,7 @@ sealed case class Abstract( override val job_name: String, + override val worker_uuid: String, override val node_info: Host.Node_Info ) extends Build_Job { override def make_abstract: Abstract = this @@ -38,13 +40,15 @@ def start_session( build_context: Build_Process.Context, + worker_uuid: String, progress: Progress, log: Logger, session_background: Sessions.Background, input_shasum: SHA1.Shasum, node_info: Host.Node_Info ): Session_Job = { - new Session_Job(build_context, progress, log, session_background, input_shasum, node_info) + new Session_Job( + build_context, worker_uuid, progress, log, session_background, input_shasum, node_info) } object Session_Context { @@ -106,6 +110,7 @@ class Session_Job private[Build_Job]( build_context: Build_Process.Context, + override val worker_uuid: String, progress: Progress, log: Logger, session_background: Sessions.Background, diff -r 80021d645a01 -r 8036d5f12997 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Mar 08 15:25:55 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Wed Mar 08 15:50:29 2023 +0100 @@ -600,10 +600,11 @@ object Running { val name = Generic.name.make_primary_key + val worker_uuid = Generic.worker_uuid val hostname = SQL.Column.string("hostname") val numa_node = SQL.Column.int("numa_node") - val table = make_table("running", List(name, hostname, numa_node)) + val table = make_table("running", List(name, worker_uuid, hostname, numa_node)) } def read_running(db: SQL.Database): List[Build_Job.Abstract] = @@ -612,9 +613,10 @@ List.from[Build_Job.Abstract], { res => val name = res.string(Running.name) + val worker_uuid = res.string(Running.worker_uuid) val hostname = res.string(Running.hostname) val numa_node = res.get_int(Running.numa_node) - Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node)) + Build_Job.Abstract(name, worker_uuid, Host.Node_Info(hostname, numa_node)) } ) @@ -633,8 +635,9 @@ db.execute_statement(Running.table.insert(), body = { stmt => stmt.string(1) = job.job_name - stmt.string(2) = job.node_info.hostname - stmt.int(3) = job.node_info.numa_node + stmt.string(2) = job.worker_uuid + stmt.string(3) = job.node_info.hostname + stmt.int(4) = job.node_info.numa_node }) } @@ -908,7 +911,7 @@ store.init_output(session_name) val job = - Build_Job.start_session(build_context, progress, log, + Build_Job.start_session(build_context, worker_uuid, progress, log, build_deps.background(session_name), input_shasum, node_info) state1.add_running(session_name, job) }