# HG changeset patch # User wenzelm # Date 1700394401 -3600 # Node ID ae2f5fd0bb5d6c925039e91a32dc367a1a030cce # Parent f728be354ffbc3e680259d6f80dd0d42391f54b0 clarified signature and modules: more explicit Build_Log.History; diff -r f728be354ffb -r ae2f5fd0bb5d src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Sat Nov 18 21:14:34 2023 +0100 +++ b/src/Pure/Admin/build_log.scala Sun Nov 19 12:46:41 2023 +0100 @@ -1190,6 +1190,88 @@ } + + /** build history **/ + + object History { + sealed case class Entry( + known: Boolean, + isabelle_version: String, + afp_version: Option[String], + pull_date: Date + ) { + def unknown: Boolean = !known + def versions: (String, Option[String]) = (isabelle_version, afp_version) + + def known_versions(rev: String, afp_rev: Option[String]): Boolean = + known && rev.nonEmpty && isabelle_version == rev && + (afp_rev.isEmpty || afp_rev.get.nonEmpty && afp_version == afp_rev) + } + + object Run { + val empty: Run = Run() + def longest(runs: List[Run]): Run = runs.foldLeft(empty)(_ max _) + } + + sealed case class Run(entries: List[Entry] = Nil) { + def is_empty: Boolean = entries.isEmpty + val length: Int = entries.length + def max(other: Run): Run = if (length >= other.length) this else other + def median: Option[Entry] = if (is_empty) None else Some(entries(length / 2)) + + override def toString: String = { + val s = if (is_empty) "" else "length = " + length + ", median = " + median.get.pull_date + "Build_Log.History.Run(" + s + ")" + } + } + + def retrieve( + db: SQL.Database, + days: Int, + rev: String, + afp_rev: Option[String], + sql: PostgreSQL.Source + ): History = { + val afp = afp_rev.isDefined + + val entries = + db.execute_query_statement( + private_data.select_recent_versions( + days = days, rev = rev, afp_rev = afp_rev, sql = SQL.where(sql)), + List.from[Entry], + { res => + val known = res.bool(private_data.known) + val isabelle_version = res.string(Prop.isabelle_version) + val afp_version = if (afp) proper_string(res.string(Prop.afp_version)) else None + val pull_date = res.date(private_data.pull_date(afp)) + Entry(known, isabelle_version, afp_version, pull_date) + }) + + new History(entries) + } + } + + final class History private(val entries: List[History.Entry]) { + override def toString: String = "Build_Log.History(" + entries.length + ")" + + def unknown_runs( + pre: History.Entry => Boolean = _ => true, + post: History.Run => Boolean = _ => true + ): List[History.Run] = { + var rest = entries.filter(pre) + val result = new mutable.ListBuffer[History.Run] + while (rest.nonEmpty) { + val (a, b) = Library.take_prefix[History.Entry](_.unknown, rest.dropWhile(_.known)) + val run = History.Run(a) + if (!run.is_empty && post(run)) result += run + rest = b + } + result.toList + } + } + + + /** maintain build_log database **/ def build_log_database(options: Options, logs: List[Path], diff -r f728be354ffb -r ae2f5fd0bb5d src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sat Nov 18 21:14:34 2023 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Nov 19 12:46:41 2023 +0100 @@ -118,53 +118,6 @@ /* remote build_history */ - sealed case class Item( - known: Boolean, - isabelle_version: String, - afp_version: Option[String], - pull_date: Date - ) { - def unknown: Boolean = !known - def versions: (String, Option[String]) = (isabelle_version, afp_version) - - def known_versions(rev: String, afp_rev: Option[String]): Boolean = - known && rev.nonEmpty && isabelle_version == rev && - (afp_rev.isEmpty || afp_rev.get.nonEmpty && afp_version == afp_rev) - } - - def recent_items( - db: SQL.Database, - days: Int, - rev: String, - afp_rev: Option[String], - sql: PostgreSQL.Source - ): List[Item] = { - val afp = afp_rev.isDefined - - db.execute_query_statement( - Build_Log.private_data.select_recent_versions( - days = days, rev = rev, afp_rev = afp_rev, sql = SQL.where(sql)), - List.from[Item], - { res => - val known = res.bool(Build_Log.private_data.known) - val isabelle_version = res.string(Build_Log.Prop.isabelle_version) - val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None - val pull_date = res.date(Build_Log.private_data.pull_date(afp)) - Item(known, isabelle_version, afp_version, pull_date) - }) - } - - def unknown_runs(items: List[Item]): List[List[Item]] = { - var rest = items - val result = new mutable.ListBuffer[List[Item]] - while (rest.nonEmpty) { - val (run, r) = Library.take_prefix[Item](_.unknown, rest.dropWhile(_.known)) - if (run.nonEmpty) result += run - rest = r - } - result.toList - } - sealed case class Remote_Build( description: String, host: String, @@ -195,29 +148,26 @@ def profile: Build_Status.Profile = Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql) - def pick(options: Options, filter: Item => Boolean): Option[(String, Option[String])] = { + def pick( + options: Options, + filter: Build_Log.History.Entry => Boolean + ): Option[(String, Option[String])] = { val rev = get_rev() val afp_rev = if (afp) Some(get_afp_rev()) else None val store = Build_Log.store(options) using(store.open_database()) { db => - def pick_recent(days: Int, gap: Int): Option[(String, Option[String])] = { - val items = recent_items(db, days, rev, afp_rev, sql).filter(filter) - val runs = unknown_runs(items).filter(run => run.length >= gap) - val (longest_run, longest_length) = - runs.foldLeft((List.empty[Item], 0)) { - case (res@(item1, len1), item2) => - val len2 = item2.length - if (len1 >= len2) res else (item2, len2) - } - if (longest_run.isEmpty) None - else Some(longest_run(longest_length / 2).versions) + def get(days: Int, gap: Int): Option[(String, Option[String])] = { + val runs = + Build_Log.History.retrieve(db, days, rev, afp_rev, sql) + .unknown_runs(pre = filter, post = run => run.length >= gap) + Build_Log.History.Run.longest(runs).median.map(_.versions) } - pick_recent(options.int("build_log_history") max history, 2) orElse - pick_recent(300, 8) orElse - pick_recent(3000, 32) orElse - pick_recent(0, 1) + get(options.int("build_log_history") max history, 2) orElse + get(300, 8) orElse + get(3000, 32) orElse + get(0, 1) } } @@ -615,10 +565,10 @@ val hg = Mercurial.repository(isabelle_repos) val hg_graph = hg.graph() - def history_base_filter(r: Remote_Build): Item => Boolean = { + def history_base_filter(r: Remote_Build): Build_Log.History.Entry => Boolean = { val base_rev = hg.id(r.history_base) val nodes = hg_graph.all_succs(List(base_rev)).toSet - (item: Item) => nodes(item.isabelle_version) + (entry: Build_Log.History.Entry) => nodes(entry.isabelle_version) }