diff -r 1cd5888ec05f -r 512d701d0df9 src/Pure/Build/build_cluster.scala --- a/src/Pure/Build/build_cluster.scala Thu Feb 22 17:21:13 2024 +0100 +++ b/src/Pure/Build/build_cluster.scala Thu Feb 22 17:24:43 2024 +0100 @@ -171,52 +171,53 @@ ) extends AutoCloseable { override def toString: String = ssh.toString - val remote_identifier: String = options.string("build_cluster_identifier") - val remote_root: Path = Path.explode(options.string("build_cluster_root")) - val remote_isabelle_home: Path = remote_root + Path.explode("isabelle") - val remote_afp_root: Option[Path] = + val build_cluster_identifier: String = options.string("build_cluster_identifier") + val build_cluster_root: Path = Path.explode(options.string("build_cluster_root")) + val built_cluster_isabelle_home: Path = build_cluster_root + Path.explode("isabelle") + val build_cluster_afp_root: Option[Path] = if (build_context.afp_root.isEmpty) None - else Some(remote_isabelle_home + Path.explode("AFP")) + else Some(built_cluster_isabelle_home + Path.explode("AFP")) - lazy val remote_isabelle: Other_Isabelle = - Other_Isabelle(remote_isabelle_home, isabelle_identifier = remote_identifier, ssh = ssh) + lazy val build_cluster_isabelle: Other_Isabelle = + Other_Isabelle(built_cluster_isabelle_home, + isabelle_identifier = build_cluster_identifier, ssh = ssh) def sync(): Other_Isabelle = { - Sync.sync(options, Rsync.Context(ssh = ssh), remote_isabelle_home, + Sync.sync(options, Rsync.Context(ssh = ssh), built_cluster_isabelle_home, afp_root = build_context.afp_root, purge_heaps = true, preserve_jars = true) - remote_isabelle + build_cluster_isabelle } def init(): Unit = - remote_isabelle.init(other_settings = - remote_isabelle.init_components() ::: remote_isabelle.debug_settings()) + build_cluster_isabelle.init(other_settings = + build_cluster_isabelle.init_components() ::: build_cluster_isabelle.debug_settings()) def benchmark(): Unit = { val script = - Build_Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home) - remote_isabelle.bash(script).check + Build_Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = built_cluster_isabelle_home) + build_cluster_isabelle.bash(script).check } def start(): Process_Result = { - val remote_ml_platform = remote_isabelle.getenv("ML_PLATFORM") - if (remote_ml_platform != build_context.ml_platform) { - error("Bad ML_PLATFORM: found " + remote_ml_platform + + val build_cluster_ml_platform = build_cluster_isabelle.getenv("ML_PLATFORM") + if (build_cluster_ml_platform != build_context.ml_platform) { + error("Bad ML_PLATFORM: found " + build_cluster_ml_platform + ", but expected " + build_context.ml_platform) } - val build_options = + 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 = build_options.toList, build_id = build_context.build_uuid, - isabelle_home = remote_isabelle_home, - afp_root = remote_afp_root, - dirs = Path.split(host.dirs).map(remote_isabelle.expand_path), + isabelle_home = built_cluster_isabelle_home, + afp_root = build_cluster_afp_root, + dirs = Path.split(host.dirs).map(build_cluster_isabelle.expand_path), quiet = true) - remote_isabelle.bash(script).check + build_cluster_isabelle.bash(script).check } override def close(): Unit = ssh.close() @@ -334,7 +335,7 @@ this } - + override def benchmark(): Build_Cluster = synchronized { _init.foreach(_.join) _init =