# HG changeset patch
# User wenzelm
# Date 1710325402 -3600
# Node ID 6fa259b24deb759f293623a16079964ff1a5de58
# Parent  6f9ae0f052bc6398140a280320b522669148b57b
proper system option, instead of hardwired default;

diff -r 6f9ae0f052bc -r 6fa259b24deb etc/options
--- 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"
 
diff -r 6f9ae0f052bc -r 6fa259b24deb src/Pure/Build/build_process.scala
--- 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 }