# HG changeset patch
# User wenzelm
# Date 1709921058 -3600
# Node ID 2da08d9ce629af1ed93b40b15428b4ff68a58e84
# Parent  5f033e4cbeb72cd6acfb90f984ea4e35461bca89
prefer explicit option "build_log_verbose";

diff -r 5f033e4cbeb7 -r 2da08d9ce629 etc/options
--- a/etc/options	Fri Mar 08 18:58:49 2024 +0100
+++ b/etc/options	Fri Mar 08 19:04:18 2024 +0100
@@ -424,6 +424,9 @@
 option build_log_history : int = 30
   -- "length of relevant history (in days)"
 
+option build_log_verbose : bool = false for build_sync
+  -- "extra verbosity for build log database"
+
 
 section "Isabelle/Scala/ML system channel"
 
diff -r 5f033e4cbeb7 -r 2da08d9ce629 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri Mar 08 18:58:49 2024 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Mar 08 19:04:18 2024 +0100
@@ -201,7 +201,8 @@
         augment_settings(
           other_isabelle, threads, arch_64, arch_apple, heap, max_heap, more_settings)
 
-      File.write(other_isabelle.etc_preferences, cat_lines(more_preferences))
+      File.write(other_isabelle.etc_preferences,
+        cat_lines("build_log_verbose = true" :: more_preferences))
 
       val isabelle_output =
         other_isabelle.expand_path(
diff -r 5f033e4cbeb7 -r 2da08d9ce629 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Mar 08 18:58:49 2024 +0100
+++ b/src/Pure/Build/build.scala	Fri Mar 08 19:04:18 2024 +0100
@@ -119,7 +119,7 @@
 
     def build_options(options: Options, build_cluster: Boolean = false): Options = {
       val options1 = options + "completion_limit=0" + "editor_tracing_messages=0"
-      if (build_cluster) options1 + "build_database" else options1
+      if (build_cluster) options1 + "build_database" + "build_log_verbose" else options1
     }
 
     final def build_store(options: Options,
diff -r 5f033e4cbeb7 -r 2da08d9ce629 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Fri Mar 08 18:58:49 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Fri Mar 08 19:04:18 2024 +0100
@@ -1052,14 +1052,15 @@
       else state
     }
     else {
+      val build_log_verbose = build_options.bool("build_log_verbose")
+
       val start = progress.now()
       val start_time = start.time - build_start.time
-      val start_time_msg = _build_database.isDefined
+      val start_time_msg = build_log_verbose
 
       val node_info = next_node_info(state, session_name)
       val node_info_msg =
-        node_info.numa_node.isDefined || node_info.rel_cpus.nonEmpty  ||
-        _build_database.isDefined && _build_database.get.is_postgresql
+        node_info.numa_node.isDefined || node_info.rel_cpus.nonEmpty  || build_log_verbose
 
       progress.echo(
         (if (store_heap) "Building " else "Running ") + session_name +