src/Pure/Tools/build_process.scala

   object Context {
     def apply(
       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,
       max_jobs: Int = 1,
       fresh_build: Boolean = false,

               case ord => ord
             }
         }
 
       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)
     }
   }
 
   final class Context private(
     val store: Sessions.Store,
     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,
     val max_jobs: Int,
     val fresh_build: Boolean,

         val db = SQLite.open_database(Build_Process.Data.database)
         try { Isabelle_System.chmod("600", Build_Process.Data.database) }
         catch { case exn: Throwable => db.close(); throw exn }
         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))
   }

           if_proper(worker_uuid, Generic.worker_uuid.equal(worker_uuid)),
           if_proper(name, Generic.name.equal(name)),
           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 table = make_table("", List(build_uuid, ml_platform, options))
+      val start = SQL.Column.date("start")
+
+      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()
+      }
     }
 
 
     /* sessions */
 

         Pending.table,
         Running.table,
         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,
       build_uuid: String,
       hostname: String,

 
   private val _database: Option[SQL.Database] = build_context.open_database()
 
   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 {
         case None => body
         case Some(db) => db.transaction { body }

 
   /* run */
 
   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()
       }

     if (finished()) {
       progress.echo_warning("Nothing to build")
       Map.empty[String, Process_Result]
     }
     else {
-      setup_database()
+      init()
       while (!finished()) {
         if (progress.stopped) synchronized_database { _state.stop_running() }
 
         for (job <- synchronized_database { _state.finished_running() }) {
           val job_name = job.job_name