added start date to build jobs, e.g., for build time estimation;

--- a/src/Pure/Tools/build_process.scala	Wed Oct 18 19:49:08 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Oct 18 19:53:39 2023 +0200
@@ -56,6 +56,7 @@
     worker_uuid: String,
     build_uuid: String,
     node_info: Host.Node_Info,
+    start_date: Date,
     build: Option[Build_Job]
   ) extends Library.Named {
     def join_build: Option[Build_Job.Result] = build.flatMap(_.join)
@@ -615,10 +616,12 @@
       val hostname = SQL.Column.string("hostname")
       val numa_node = SQL.Column.int("numa_node")
       val rel_cpus = SQL.Column.string("rel_cpus")
+      val start_date = SQL.Column.date("start_date")
 
       val table =
         make_table(
-          List(name, worker_uuid, build_uuid, hostname, numa_node, rel_cpus), name = "running")
+          List(name, worker_uuid, build_uuid, hostname, numa_node, rel_cpus, start_date),
+          name = "running")
     }
 
     def read_running(db: SQL.Database): State.Running =
@@ -632,9 +635,10 @@
           val hostname = res.string(Running.hostname)
           val numa_node = res.get_int(Running.numa_node)
           val rel_cpus = res.string(Running.rel_cpus)
+          val start_date = res.date(Running.start_date)
 
           val node_info = Host.Node_Info(hostname, numa_node, Host.Range.from(rel_cpus))
-          name -> Job(name, worker_uuid, build_uuid, node_info, None)
+          name -> Job(name, worker_uuid, build_uuid, node_info, start_date, None)
         }
       )
 
@@ -661,6 +665,7 @@
             stmt.string(4) = job.node_info.hostname
             stmt.int(5) = job.node_info.numa_node
             stmt.string(6) = Host.Range(job.node_info.rel_cpus)
+            stmt.date(7) = job.start_date
           })
       }
 
@@ -1057,7 +1062,8 @@
         Build_Job.start_session(build_context, session, progress, log, server,
           build_deps.background(session_name), sources_shasum, input_shasum, node_info, store_heap)
 
-      val job = Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, Some(build))
+      val job =
+        Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, Date.now(), Some(build))
 
       state.add_running(job)
     }