--- a/src/Pure/Admin/build_log.scala Wed Mar 29 21:16:14 2023 +0200
+++ b/src/Pure/Admin/build_log.scala Wed Mar 29 21:23:56 2023 +0200
@@ -1150,6 +1150,7 @@
def build_log_database(options: Options, log_dirs: List[Path],
progress: Progress = new Progress,
+ vacuum: Boolean = false,
ml_statistics: Boolean = false,
snapshot: Option[Path] = None
): Unit = {
@@ -1161,7 +1162,7 @@
).sortBy(Log_File.plain_name)
using(store.open_database()) { db =>
- db.vacuum()
+ if (vacuum) db.vacuum()
progress.echo("Updating database " + db + " ...")
val errors0 = store.write_info(db, log_files, progress = progress)
@@ -1198,6 +1199,7 @@
{ args =>
var ml_statistics: Boolean = false
var snapshot: Option[Path] = None
+ var vacuum = false
var dirs: List[Path] = Nil
var options = Options.init()
var verbose = false
@@ -1208,6 +1210,7 @@
Options are:
-M include ML statistics
-S FILE snapshot to SQLite db file
+ -V vacuum cleaning of database
-d DIR include directory with log files
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
@@ -1217,6 +1220,7 @@
""",
"M" -> (_ => ml_statistics = true),
"S:" -> (arg => snapshot = Some(Path.explode(arg))),
+ "V" -> (_ => vacuum = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true))
@@ -1226,7 +1230,7 @@
val progress = new Console_Progress(verbose = verbose)
- build_log_database(options, dirs, progress = progress,
+ build_log_database(options, dirs, progress = progress, vacuum = vacuum,
ml_statistics = ml_statistics, snapshot = snapshot)
})
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Mar 29 21:16:14 2023 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Mar 29 21:23:56 2023 +0200
@@ -598,7 +598,7 @@
Logger_Task("build_log_database",
logger =>
Build_Log.build_log_database(logger.options, build_log_dirs,
- ml_statistics = true,
+ vacuum = true, ml_statistics = true,
snapshot = Some(Isabelle_Devel.build_log_snapshot))),
Logger_Task("build_status",
logger => Isabelle_Devel.build_status(logger.options)))))),