# HG changeset patch
# User wenzelm
# Date 1494274896 -7200
# Node ID d3d5cb2d6866cd7fd4425fc0d76dd3ff03c75a5d
# Parent  4935bac8a85039fbb17cf92bd5275f4a9194eaf2
pick isabelle_version based on build_log database;

diff -r 4935bac8a850 -r d3d5cb2d6866 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 08 21:58:15 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 08 22:21:36 2017 +0200
@@ -658,6 +658,7 @@
     val heap_size = SQL.Column.long("heap_size")
     val status = SQL.Column.string("status")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
+    val known = SQL.Column.bool("known")
 
     val meta_info_table =
       build_log_table("meta_info", log_name :: Prop.all_props ::: Settings.all_settings)
@@ -689,11 +690,13 @@
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
-    def recent_pull_date_table(days: Int): SQL.Table =
+    def recent_pull_date_table(days: Int, rev: String = ""): SQL.Table =
     {
       val table = pull_date_table
       SQL.Table("recent_pull_date", table.columns,
-        table.select(table.columns, "WHERE " + pull_date(table) + " > " + recent_time(days)))
+        table.select(table.columns,
+          "WHERE " + pull_date(table) + " > " + recent_time(days) +
+          (if (rev == "") "" else " OR " + Prop.isabelle_version(table) + " = " + SQL.string(rev))))
     }
 
     def select_recent_log_names(days: Int): SQL.Source =
@@ -704,6 +707,22 @@
         " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
     }
 
+    def select_recent_isabelle_versions(days: Int, rev: String = "", sql: SQL.Source = "")
+      : SQL.Source =
+    {
+      val table1 = recent_pull_date_table(days, rev = rev)
+      val table2 = meta_info_table
+      val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql))
+
+      val columns =
+        List(Prop.isabelle_version(table1), pull_date(table1),
+          known.copy(expr = log_name(aux_table) + " IS NOT NULL"))
+      SQL.select(columns, distinct = true) +
+        table1.query_named + SQL.join_outer + aux_table.query_named +
+        " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(aux_table) +
+        " ORDER BY " + pull_date(table1) + " DESC"
+    }
+
 
     /* universal view on main data */
 
diff -r 4935bac8a850 -r d3d5cb2d6866 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon May 08 21:58:15 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon May 08 22:21:36 2017 +0200
@@ -73,6 +73,11 @@
 
   /* remote build_history */
 
+  sealed case class Item(known: Boolean, isabelle_version: String, pull_date: Date)
+  {
+    def unknown: Boolean = !known
+  }
+
   sealed case class Remote_Build(
     description: String,
     host: String,
@@ -83,13 +88,47 @@
     args: String = "",
     detect: SQL.Source = "")
   {
+    def sql: SQL.Source =
+      Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
+      Build_Log.Prop.build_host + " = " + SQL.string(host) +
+      (if (detect == "") "" else " AND " + SQL.enclose(detect))
+
     def profile: Build_Status.Profile =
+      Build_Status.Profile(description, sql)
+
+    def pick(options: Options, rev: String = ""): Option[String] =
     {
-      val sql =
-        Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
-        Build_Log.Prop.build_host + " = " + SQL.string(host) +
-        (if (detect == "") "" else " AND " + SQL.enclose(detect))
-      Build_Status.Profile(description, sql)
+      val store = Build_Log.store(options)
+      using(store.open_database())(db =>
+      {
+        val select =
+          Build_Log.Data.select_recent_isabelle_versions(
+            days = options.int("build_log_history"), rev = rev, sql = "WHERE " + sql)
+
+        val recent_items =
+          db.using_statement(select)(stmt =>
+            stmt.execute_query().iterator(res =>
+            {
+              val known = res.bool(Build_Log.Data.known)
+              val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
+              val pull_date = res.date(Build_Log.Data.pull_date)
+              Item(known, isabelle_version, pull_date)
+            }).toList)
+
+        def unknown_runs(items: List[Item]): List[List[Item]] =
+        {
+          val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
+          if (run.nonEmpty) run :: unknown_runs(rest) else Nil
+        }
+
+        if (rev == "" || recent_items.exists(item => item.known && item.isabelle_version == rev)) {
+          unknown_runs(recent_items).sortBy(_.length).reverse match {
+            case longest_run :: _ => Some(longest_run(longest_run.length / 2).isabelle_version)
+            case _ => None
+          }
+        }
+        else Some(rev)
+      })
     }
   }
 
@@ -306,10 +345,11 @@
     val rev = Mercurial.repository(isabelle_repos).id()
 
     run(main_start_date,
-      Logger_Task("isabelle_cronjob", _ =>
+      Logger_Task("isabelle_cronjob", logger =>
         run_now(
           SEQ(List(build_release, build_history_base,
-            PAR(remote_builds.map(seq => SEQ(seq.map(remote_build_history(rev, _))))),
+            PAR(remote_builds.map(seq =>
+              SEQ(seq.flatMap(r => r.pick(logger.options, rev).map(remote_build_history(_, r)))))),
             Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
             Logger_Task("build_log_database",
               logger => Isabelle_Devel.build_log_database(logger.options)),