# HG changeset patch # User wenzelm # Date 1678730656 -3600 # Node ID 50fc9143ccfa33e179c7c8904f63e3e12ba84b7d # Parent a65b39fdf8b64eb45be1eaa1c4c936ac3b3720af more database content; diff -r a65b39fdf8b6 -r 50fc9143ccfa 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) } }