src/Pure/Tools/build_process.scala

--- a/src/Pure/Tools/build_process.scala	Sat Jul 22 12:11:50 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sat Jul 22 13:31:55 2023 +0200
@@ -881,22 +881,16 @@
 
   protected val log: Logger = Logger.make_system_log(progress, build_options)
 
-  protected def init_build_cluster(remote_hosts: List[Build_Cluster.Host]): Build_Cluster =
-    new Build_Cluster(build_context, remote_hosts, progress = build_progress)
-
-  protected def exit_build_cluster(build_cluster: Build_Cluster): Boolean = {
-    val results = build_cluster.join
-    build_cluster.close()
-    results.forall({ case Exn.Res(res) => res.ok case _ => false })
+  protected def open_build_cluster(): Build_Cluster = {
+    val build_cluster = Build_Cluster.make(build_context, progress = build_progress)
+    build_cluster.open()
+    build_cluster
   }
 
   private val _build_cluster =
     try {
-      val remote_hosts = build_context.build_hosts.filterNot(_.is_local)
-      if (build_context.master && _build_database.isDefined && remote_hosts.nonEmpty) {
-        Some(init_build_cluster(remote_hosts))
-      }
-      else None
+      if (build_context.master && _build_database.isDefined) open_build_cluster()
+      else Build_Cluster.none
     }
     catch { case exn: Throwable => close(); throw exn }
 
@@ -904,7 +898,7 @@
     Option(_database_server).flatten.foreach(_.close())
     Option(_build_database).flatten.foreach(_.close())
     Option(_host_database).flatten.foreach(_.close())
-    Option(_build_cluster).flatten.foreach(_.close())
+    Option(_build_cluster).foreach(_.close())
     progress match {
       case db_progress: Database_Progress =>
         db_progress.exit(close = true)
@@ -1076,6 +1070,7 @@
 
   def run(): Map[String, Process_Result] = {
     if (build_context.master) {
+      _build_cluster.init()
       synchronized_database("Build_Process.init") { _state = init_state(_state) }
     }
 
@@ -1102,9 +1097,9 @@
     else {
       if (build_context.master) start_build()
       start_worker()
-      _build_cluster.foreach(_.start())
+      _build_cluster.start()
 
-      if (build_context.master && !build_context.worker_active && _build_cluster.isDefined) {
+      if (build_context.master && !build_context.worker_active && _build_cluster.active()) {
         build_progress.echo("Waiting for external workers ...")
       }
 
@@ -1127,7 +1122,7 @@
         }
       }
       finally {
-        _build_cluster.foreach(exit_build_cluster)
+        _build_cluster.stop()
         stop_worker()
         if (build_context.master) stop_build()
       }