# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1706113849 -3600
# Node ID 6e5397fcc41b0e34b92b8da6949b0aa7065ae8ac
# Parent  9bc62f636fc47c8ebe528482fa4ee847659f16d7
add build_sync tag to sync certain options (e.g., build_engine) across build processes;

diff -r 9bc62f636fc4 -r 6e5397fcc41b etc/options
--- a/etc/options	Tue Jan 23 23:15:51 2024 +0100
+++ b/etc/options	Wed Jan 24 17:30:49 2024 +0100
@@ -177,7 +177,7 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
-public option ML_system_64 : bool = false for build
+public option ML_system_64 : bool = false for build build_sync
   -- "prefer native 64bit platform (change requires restart)"
 
 public option ML_system_apple : bool = true for build
@@ -192,10 +192,10 @@
 option build_hostname : string = ""
   -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)"
 
-option build_engine : string = ""
+option build_engine : string = "" for build_sync
   -- "alternative session build engine"
 
-option build_database : bool = false
+option build_database : bool = false for build_sync
   -- "expose state of build process via central database"
 
 option build_database_slice : real = 300
@@ -399,7 +399,7 @@
 
 section "Build Database"
 
-option build_database_server : bool = false for connection
+option build_database_server : bool = false for connection build_sync
 option build_database_user : string = "" for connection
 option build_database_password : string = "" for connection
 option build_database_name : string = "" for connection
diff -r 9bc62f636fc4 -r 6e5397fcc41b src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Tue Jan 23 23:15:51 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Wed Jan 24 17:30:49 2024 +0100
@@ -194,10 +194,12 @@
         error("Bad ML_PLATFORM: found " + remote_ml_platform +
           ", but expected " + build_context.ml_platform)
       }
+      val build_options = 
+        for { option <- options.iterator if option.for_build_sync } yield options.spec(option.name)
       val script =
         Build.build_worker_command(host,
           ssh = ssh,
-          build_options = List(options.spec("build_database_server")),
+          build_options = build_options.toList,
           build_id = build_context.build_uuid,
           isabelle_home = remote_isabelle_home,
           afp_root = remote_afp_root,
diff -r 9bc62f636fc4 -r 6e5397fcc41b src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Jan 23 23:15:51 2024 +0100
+++ b/src/Pure/System/options.scala	Wed Jan 24 17:30:49 2024 +0100
@@ -104,7 +104,8 @@
 
   val TAG_CONTENT = "content"    // formal theory content
   val TAG_DOCUMENT = "document"  // document preparation
-  val TAG_BUILD = "build"        // relavant for "isabelle build"
+  val TAG_BUILD = "build"        // relevant for "isabelle build"
+  val TAG_BUILD_SYNC = "build_sync" // relevant for distributed "isabelle build"
   val TAG_UPDATE = "update"      // relevant for "isabelle update"
   val TAG_CONNECTION = "connection"  // private information about connections (password etc.)
   val TAG_COLOR_DIALOG = "color_dialog"  // special color selection dialog
@@ -154,6 +155,7 @@
     def for_content: Boolean = for_tag(TAG_CONTENT)
     def for_document: Boolean = for_tag(TAG_DOCUMENT)
     def for_color_dialog: Boolean = for_tag(TAG_COLOR_DIALOG)
+    def for_build_sync: Boolean = for_tag(TAG_BUILD_SYNC)
 
     def session_content: Boolean = for_content || for_document
   }