# HG changeset patch
# User wenzelm
# Date 1709903645 -3600
# Node ID d9fc2cc376940adac63626f826667f992f223db2
# Parent  4b23abde5d0b1d3082557d9b71dc9d02235fdca8
more robust build_start for master and workers (via database);

diff -r 4b23abde5d0b -r d9fc2cc37694 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Mar 08 13:05:01 2024 +0100
+++ b/src/Pure/Build/build.scala	Fri Mar 08 14:14:05 2024 +0100
@@ -40,6 +40,7 @@
     no_build: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => (),
     build_uuid: String = UUID.random_string(),
+    build_start: Option[Date] = None,
     jobs: Int = 0,
     master: Boolean = false
   ) {
@@ -632,7 +633,8 @@
         val build_context =
           Context(store, build_deps, engine = engine, afp_root = afp_root,
             hostname = hostname(build_options), numa_shuffling = numa_shuffling,
-            build_uuid = build_master.build_uuid, jobs = max_jobs.getOrElse(1))
+            build_uuid = build_master.build_uuid, build_start = Some(build_master.start),
+            jobs = max_jobs.getOrElse(1))
 
         engine.run_build_process(build_context, progress, server)
       }
diff -r 4b23abde5d0b -r d9fc2cc37694 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Fri Mar 08 13:05:01 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Fri Mar 08 14:14:05 2024 +0100
@@ -354,14 +354,15 @@
       db: SQL.Database,
       build_uuid: String,
       ml_platform: String,
-      options: String
+      options: String,
+      start: Date
     ): Unit = {
       db.execute_statement(Base.table.insert(), body =
         { stmt =>
           stmt.string(1) = build_uuid
           stmt.string(2) = ml_platform
           stmt.string(3) = options
-          stmt.date(4) = db.now()
+          stmt.date(4) = start
           stmt.date(5) = None
         })
     }
@@ -914,6 +915,8 @@
     }
   }
 
+  protected val build_start: Date = build_context.build_start getOrElse progress.now()
+
   protected val log: Logger = Logger.make_system_log(progress, build_options)
 
   protected def open_build_cluster(): Build_Cluster =
@@ -1082,7 +1085,7 @@
   protected final def start_build(): Unit = synchronized_database("Build_Process.start_build") {
     for (db <- _build_database) {
       Build_Process.private_data.start_build(db, build_uuid, build_context.ml_platform,
-        build_context.sessions_structure.session_prefs)
+        build_context.sessions_structure.session_prefs, build_start)
     }
   }