# HG changeset patch
# User wenzelm
# Date 1698604966 -3600
# Node ID 4838a27794ac3edee714ecd5a8d3b3dd1514af3e
# Parent  aeb511a520f405b04da02a24f0e091e483552678
performance tuning: parallel and incremental update of build_log_database;

diff -r aeb511a520f4 -r 4838a27794ac src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Oct 29 18:49:42 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Oct 29 19:42:46 2023 +0100
@@ -429,12 +429,18 @@
               options =
                 " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
                 " -f " + r.build_history_options,
+
               args = "-o timeout=10800 " + r.args)
 
-          for ((log_name, bytes) <- results) {
-            logger.log(Date.now(), log_name)
-            Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
-          }
+          val log_files =
+            for ((log_name, bytes) <- results) yield {
+              val log_file = logger.log_dir + Path.explode(log_name)
+              logger.log(Date.now(), log_name)
+              Bytes.write(log_file, bytes)
+              log_file
+            }
+
+          Build_Log.build_log_database(logger.options, log_files, ml_statistics = true)
         }
       })
   }
@@ -597,7 +603,15 @@
         run_now(
           SEQ(List(
             init,
-            PAR(List(mailman_archives, build_release)),
+            PAR(
+              List(
+                mailman_archives,
+                build_release,
+                Logger_Task("build_log_database",
+                  logger =>
+                    Build_Log.build_log_database(logger.options, build_log_dirs,
+                      vacuum = true, ml_statistics = true,
+                      snapshot = Some(Isabelle_Devel.build_log_snapshot))))),
             PAR(
               List(remote_builds1, remote_builds2).map(remote_builds =>
               SEQ(List(
@@ -607,11 +621,6 @@
                       (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
                       (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 =>
-                    Build_Log.build_log_database(logger.options, build_log_dirs,
-                      vacuum = true, ml_statistics = true,
-                      snapshot = Some(Isabelle_Devel.build_log_snapshot))),
                 Logger_Task("build_status",
                   logger => Isabelle_Devel.build_status(logger.options)))))),
             exit)))))