# HG changeset patch
# User wenzelm
# Date 1698923010 -3600
# Node ID 45d570945fe4674afb47640f0625cc3b02a20223
# Parent  4222955f3b6967657728aa6148096b1c50d5b486
more detailed progress for build_log_database, to see better what happens when;

diff -r 4222955f3b69 -r 45d570945fe4 src/Pure/Admin/build_log.scala
--- 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)
           }
         }
       }
diff -r 4222955f3b69 -r 45d570945fe4 src/Pure/Admin/isabelle_cronjob.scala
--- 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(