--- a/etc/options Wed Mar 13 11:04:06 2024 +0100
+++ b/etc/options Wed Mar 13 11:23:22 2024 +0100
@@ -207,6 +207,9 @@
option build_cluster_delay : real = 1.0
-- "delay build process main loop (cluster)"
+option build_cluster_expire : int = 50
+ -- "enforce database synchronization after given number of delay loops"
+
option build_cluster_root : string = "$USER_HOME/.isabelle/build_cluster"
-- "root directory for remote build cluster sessions"
--- a/src/Pure/Build/build_process.scala Wed Mar 13 11:04:06 2024 +0100
+++ b/src/Pure/Build/build_process.scala Wed Mar 13 11:23:22 2024 +0100
@@ -1025,6 +1025,8 @@
build_options.seconds(option)
}
+ protected val build_expire: Int = build_options.int("build_cluster_expire")
+
protected val _host_database: SQL.Database =
try { store.open_build_database(path = Host.private_data.database, server = server) }
catch { case exn: Throwable => close(); throw exn }
@@ -1041,7 +1043,8 @@
hostname = hostname,
context_uuid = build_uuid,
kind = "build_process",
- timeout = Some(build_delay))
+ timeout = Some(build_delay),
+ tick_expire = build_expire)
(progress, progress.agent_uuid)
}
catch { case exn: Throwable => close(); throw exn }