merged

--- a/etc/options	Fri Jan 17 20:24:02 2025 +0000
+++ b/etc/options	Fri Jan 17 20:24:09 2025 +0000
@@ -234,6 +234,9 @@
 option build_schedule_inactive_delay : real = 300.0
   -- "delay removing inactive hosts"
 
+option build_schedule_history : int = 150
+  -- "length of history relevant for scheduling (in days)"
+
 
 section "Build Manager"
 

--- a/src/Pure/Build/build_schedule.scala	Fri Jan 17 20:24:02 2025 +0000
+++ b/src/Pure/Build/build_schedule.scala	Fri Jan 17 20:24:09 2025 +0000
@@ -69,14 +69,16 @@
     }
 
     def load(
+      build_options: Options,
       host_infos: Host_Infos,
       log_database: SQL.Database,
       sessions_structure: Sessions.Structure
     ): Timing_Data = {
+      val days = build_options.int("build_schedule_history")
       val build_history =
         for {
           log_name <- log_database.execute_query_statement(
-            Build_Log.private_data.meta_info_table.select(List(Build_Log.Column.log_name)),
+            Build_Log.private_data.select_recent_log_names(days),
             List.from[String], res => res.string(Build_Log.Column.log_name))
           meta_info <- Build_Log.private_data.read_meta_info(log_database, log_name)
           build_info = Build_Log.private_data.read_build_info(log_database, log_name)
@@ -1065,9 +1067,8 @@
       Host_Infos.load(build_options, build_hosts, _host_database)
     }
 
-    private val timing_data: Timing_Data = {
-      Timing_Data.load(_host_infos, _log_database, build_context.sessions_structure)
-    }
+    private val timing_data: Timing_Data =
+      Timing_Data.load(build_options, _host_infos, _log_database, build_context.sessions_structure)
 
     private var _scheduler = init_scheduler(timing_data)
 
@@ -1108,6 +1109,7 @@
       val props =
         List(
           Build_Log.Prop.build_id.name -> build_context.build_uuid,
+          Build_Log.Prop.isabelle_version.name -> Isabelle_System.isabelle_id(),
           Build_Log.Prop.build_engine.name -> build_context.engine.name,
           Build_Log.Prop.build_host.name -> hostname,
           Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start))
@@ -1261,7 +1263,7 @@
 
     def read_serial(db: SQL.Database, build_uuid: String = ""): Long =
       db.execute_query_statementO[Long](
-        Schedules.table.select(List(Schedules.serial.max), sql = 
+        Schedules.table.select(List(Schedules.serial.max), sql =
           SQL.where(if_proper(build_uuid, Schedules.build_uuid.equal(build_uuid)))),
           _.long(Schedules.serial)).getOrElse(0L)
 
@@ -1373,7 +1375,7 @@
         schedule.generator != old_schedule.generator ||
         schedule.start != old_schedule.start ||
         schedule.graph != old_schedule.graph
-      
+
       val schedule1 =
         if (changed) schedule.copy(serial = old_schedule.next_serial) else schedule
       if (schedule1.serial != schedule.serial) write_schedule(db, schedule1)
@@ -1525,7 +1527,7 @@
       }
 
       val host_infos = Host_Infos.load(build_options, cluster_hosts, host_database)
-      val timing_data = Timing_Data.load(host_infos, log_database, full_sessions)
+      val timing_data = Timing_Data.load(build_options, host_infos, log_database, full_sessions)
 
       val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
 

--- a/src/Pure/General/mercurial.scala	Fri Jan 17 20:24:02 2025 +0000
+++ b/src/Pure/General/mercurial.scala	Fri Jan 17 20:24:09 2025 +0000
@@ -117,6 +117,9 @@
 
   /* hg_sync meta data */
 
+  def sync_id(root: Path, ssh: SSH.System = SSH.Local): Option[String] =
+    if (Hg_Sync.ok(root, ssh)) Some(Hg_Sync.directory(root, ssh).id) else None
+
   object Hg_Sync {
     val NAME = ".hg_sync"
     val _NAME: String = " " + NAME

--- a/src/Pure/System/isabelle_system.scala	Fri Jan 17 20:24:02 2025 +0000
+++ b/src/Pure/System/isabelle_system.scala	Fri Jan 17 20:24:09 2025 +0000
@@ -100,7 +100,8 @@
   def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_ID", root = root) orElse
     Mercurial.archive_id(root) orElse
-    Mercurial.id_repository(root, rev = "") getOrElse
+    Mercurial.id_repository(root, rev = "") orElse
+    Mercurial.sync_id(root) getOrElse
     error("Failed to identify Isabelle distribution " + root.expand)
 
   object Isabelle_Id extends Scala.Fun_String("isabelle_id") {