diff -r 334a286b2975 -r 7c7f1473e51a src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 06 10:58:36 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 06 11:39:40 2023 +0100
@@ -21,6 +21,7 @@
       store: Sessions.Store,
       build_deps: Sessions.Deps,
       progress: Progress = new Progress,
+      ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
       hostname: String = Isabelle_System.hostname(),
       numa_shuffling: Boolean = false,
       build_heap: Boolean = false,
@@ -80,7 +81,7 @@
         }
 
       val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
-      new Context(store, build_deps, sessions, ordering, hostname, numa_nodes,
+      new Context(store, build_deps, sessions, ordering, ml_platform, hostname, numa_nodes,
         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
         no_build = no_build, session_setup, build_uuid = build_uuid)
     }
@@ -91,6 +92,7 @@
     val build_deps: Sessions.Deps,
     val sessions: State.Sessions,
     val ordering: Ordering[String],
+    val ml_platform: String,
     val hostname: String,
     val numa_nodes: List[Int],
     val build_heap: Boolean,
@@ -123,6 +125,13 @@
         Some(db)
       }
 
+    def prepare_database(): Unit = {
+      using_option(open_database()) { db =>
+        db.transaction { for (table <- Data.all_tables) db.create_table(table) }
+        db.rebuild()
+      }
+    }
+
     def store_heap(name: String): Boolean =
       build_heap || Sessions.is_pure(name) ||
       sessions.valuesIterator.exists(_.ancestors.contains(name))
@@ -256,12 +265,31 @@
           if_proper(names, Generic.name.member(names)))
     }
 
+
+    /* base table */
+
     object Base {
       val build_uuid = Generic.build_uuid.make_primary_key
       val ml_platform = SQL.Column.string("ml_platform")
       val options = SQL.Column.string("options")
+      val start = SQL.Column.date("start")
 
-      val table = make_table("", List(build_uuid, ml_platform, options))
+      val table = make_table("", List(build_uuid, ml_platform, options, start))
+    }
+
+    def start_build(
+      db: SQL.Database,
+      build_uuid: String,
+      ml_platform: String,
+      options: String
+    ): Unit = {
+      db.using_statement(Base.table.insert()) { stmt =>
+        stmt.string(1) = build_uuid
+        stmt.string(2) = ml_platform
+        stmt.string(3) = options
+        stmt.date(4) = db.now()
+        stmt.execute()
+      }
     }
 
 
@@ -583,25 +611,6 @@
         Results.table,
         Host.Data.Node_Info.table)
 
-    def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
-      for (table <- all_tables) db.create_table(table)
-
-      val old_pending = Data.read_pending(db)
-      if (old_pending.nonEmpty) {
-        error("Cannot init build process, because of unfinished " +
-          commas_quote(old_pending.map(_.name)))
-      }
-
-      for (table <- all_tables) db.using_statement(table.delete())(_.execute())
-
-      db.using_statement(Base.table.insert()) { stmt =>
-        stmt.string(1) = build_context.build_uuid
-        stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM")
-        stmt.string(3) = build_context.store.options.make_prefs(Options.init(prefs = ""))
-        stmt.execute()
-      }
-    }
-
     def update_database(
       db: SQL.Database,
       worker_uuid: String,
@@ -652,14 +661,6 @@
 
   def close(): Unit = synchronized { _database.foreach(_.close()) }
 
-  private def setup_database(): Unit =
-    synchronized {
-      for (db <- _database) {
-        db.transaction { Build_Process.Data.init_database(db, build_context) }
-        db.rebuild()
-      }
-    }
-
   protected def synchronized_database[A](body: => A): A =
     synchronized {
       _database match {
@@ -798,6 +799,13 @@
   def run(): Map[String, Process_Result] = {
     def finished(): Boolean = synchronized_database { _state.finished }
 
+    def init(): Unit = synchronized_database {
+      for (db <- _database) {
+        Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
+          store.options.make_prefs(Options.init(prefs = "")))
+      }
+    }
+
     def sleep(): Unit =
       Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
         build_options.seconds("editor_input_delay").sleep()
@@ -820,7 +828,7 @@
       Map.empty[String, Process_Result]
     }
     else {
-      setup_database()
+      init()
       while (!finished()) {
         if (progress.stopped) synchronized_database { _state.stop_running() }