--- 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"
--- 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(
--- 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,
--- 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 +