add build_sync tag to sync certain options (e.g., build_engine) across build processes;
--- 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
--- 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,
--- 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
}