# HG changeset patch # User wenzelm # Date 1680092521 -7200 # Node ID 1398add8c41453663956c27937c19202fab5f0a7 # Parent 33bee7a96f721c12867703307150daf7bd49dc93 clarified modules; diff -r 33bee7a96f72 -r 1398add8c414 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Wed Mar 29 12:25:24 2023 +0200 +++ b/src/Pure/Admin/build_log.scala Wed Mar 29 14:22:01 2023 +0200 @@ -1114,4 +1114,19 @@ Build_Info(sessions) } } + + + /* maintain build_log database */ + + def build_log_database(options: Options, log_dirs: List[Path], + snapshot: Option[Path] = None + ): Unit = { + val store = Build_Log.store(options) + using(store.open_database()) { db => + db.vacuum() + store.update_database(db, log_dirs) + store.update_database(db, log_dirs, ml_statistics = true) + snapshot.foreach(store.snapshot_database(db, _)) + } + } } diff -r 33bee7a96f72 -r 1398add8c414 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Wed Mar 29 12:25:24 2023 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Mar 29 14:22:01 2023 +0200 @@ -596,7 +596,9 @@ (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) } yield remote_build_history(rev, afp_rev, i, r)))), Logger_Task("build_log_database", - logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)), + logger => + Build_Log.build_log_database(logger.options, build_log_dirs, + snapshot = Some(Isabelle_Devel.build_log_snapshot))), Logger_Task("build_status", logger => Isabelle_Devel.build_status(logger.options)))))), exit))))) diff -r 33bee7a96f72 -r 1398add8c414 src/Pure/Admin/isabelle_devel.scala --- a/src/Pure/Admin/isabelle_devel.scala Wed Mar 29 12:25:24 2023 +0200 +++ b/src/Pure/Admin/isabelle_devel.scala Wed Mar 29 14:22:01 2023 +0200 @@ -15,6 +15,7 @@ val root: Path = Path.explode("~/html-data/devel") val cronjob_log: Path = root + Path.basic(CRONJOB_LOG) + val build_log_snapshot: Path = root + Path.explode(BUILD_LOG_DB) /* index */ @@ -49,19 +50,6 @@ } - /* maintain build_log database */ - - def build_log_database(options: Options, log_dirs: List[Path]): Unit = { - val store = Build_Log.store(options) - using(store.open_database()) { db => - db.vacuum() - store.update_database(db, log_dirs) - store.update_database(db, log_dirs, ml_statistics = true) - store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB)) - } - } - - /* present build status */ def build_status(options: Options): Unit = {