--- 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, _))
+ }
+ }
}
--- 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)))))
--- 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 = {