--- a/src/Pure/Admin/build_log.scala Thu Nov 02 11:57:40 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Thu Nov 02 12:03:30 2023 +0100
@@ -1071,10 +1071,22 @@
val consumer =
Consumer_Thread.fork[Log_File]("build_log_database")(
consume = { log_file =>
+ val t0 = progress.start.time
+ val t1 = progress.now().time
+
private_data.transaction_lock(db, label = "build_log_database") {
try { status.foreach(_.update(log_file)) }
catch { case exn: Throwable => add_error(log_file.name, exn) }
}
+
+ val t2 = progress.now().time
+
+ progress.echo(verbose = true,
+ msg =
+ "Log " + quote(log_file.name) + " (" +
+ (t1 - t0).message + " start time, " +
+ (t2 - t1).message + " elapsed time)")
+
true
},
limit = 1
@@ -1082,11 +1094,9 @@
try {
for (file <- files.iterator if status.exists(_.required(file))) {
- val log_name = Log_File.plain_name(file)
- progress.echo("Log " + quote(log_name), verbose = true)
Exn.result { Log_File.read(file, cache = cache.compress) } match {
case Exn.Res(log_file) => consumer.send(log_file)
- case Exn.Exn(exn) => add_error(log_name, exn)
+ case Exn.Exn(exn) => add_error(Log_File.plain_name(file), exn)
}
}
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Nov 02 11:57:40 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Nov 02 12:03:30 2023 +0100
@@ -19,6 +19,7 @@
val main_dir: Path = Path.explode("~/cronjob")
val main_state_file: Path = main_dir + Path.explode("run/main.state")
val build_release_log: Path = main_dir + Path.explode("run/build_release.log")
+ val build_log_database_log: Path = main_dir + Path.explode("run/build_log_database.log")
val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service
val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service
@@ -626,6 +627,8 @@
val main_start_date = Date.now()
File.write(main_state_file, main_start_date.toString + " " + log_service.hostname)
+ val build_log_database_progress = new File_Progress(build_log_database_log, verbose = true)
+
run(main_start_date,
Logger_Task("isabelle_cronjob", logger =>
run_now(
@@ -638,6 +641,7 @@
Logger_Task("build_log_database",
logger =>
Build_Log.build_log_database(logger.options, build_log_dirs,
+ progress = build_log_database_progress,
vacuum = true, ml_statistics = true,
snapshot = Some(isabelle_devel + Path.explode("build_log.db")))))),
PAR(