# HG changeset patch
# User wenzelm
# Date 1689847372 -7200
# Node ID 6f3066a9b609db5a48a8977cc9c5ab2326160f51
# Parent  eda362f85cbf486f1ccb6bb3d2a4ba58fe071deb
more pro-forma support for Build_Cluster;

diff -r eda362f85cbf -r 6f3066a9b609 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Thu Jul 20 11:10:28 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Thu Jul 20 12:02:52 2023 +0200
@@ -9,6 +9,8 @@
 
 
 object Build_Cluster {
+  /* host specifications */
+
   object Host {
     private val rfc822_specials = """()<>@,;:\"[]"""
 
@@ -75,6 +77,8 @@
     numa: Boolean,
     options: List[Options.Spec]
   ) {
+    def is_remote: Boolean = host.nonEmpty
+
     override def toString: String = print
 
     def print: String = {
@@ -95,4 +99,29 @@
     def open_ssh_session(options: Options): SSH.Session =
       SSH.open_session(options, host, port = port, user = user)
   }
+
+
+  /* remote sessions */
+
+  class Session(host: Host) extends AutoCloseable {
+    override def close(): Unit = ()
+  }
 }
+
+// class extensible via Build.Engine.build_process() and Build_Process.init_cluster()
+class Build_Cluster(
+  build_context: Build_Process.Context,
+  remote_hosts: List[Build_Cluster.Host],
+  progress: Progress = new Progress
+) extends AutoCloseable {
+  require(remote_hosts.nonEmpty && remote_hosts.forall(_.is_remote), "remote hosts required")
+
+  override def toString: String = remote_hosts.mkString("Build_Cluster(", ", ", ")")
+
+  progress.echo("Remote hosts:\n" + cat_lines(remote_hosts.map("  " + _)))
+
+  def start(): Unit = ()
+  def stop(): Unit = ()
+
+  override def close(): Unit = ()
+}
diff -r eda362f85cbf -r 6f3066a9b609 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Jul 20 11:10:28 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Jul 20 12:02:52 2023 +0200
@@ -853,7 +853,7 @@
   protected final val build_uuid: String = build_context.build_uuid
 
 
-  /* progress backed by database */
+  /* global resources with common close() operation */
 
   private val _database_server: Option[SQL.Database] =
     try { store.maybe_open_database_server(server = server) }
@@ -911,10 +911,24 @@
 
   protected val log: Logger = Logger.make_system_log(progress, build_options)
 
+  protected def init_cluster(remote_hosts: List[Build_Cluster.Host]): Build_Cluster =
+    new Build_Cluster(build_context, remote_hosts, progress = build_progress)
+
+  private val _build_cluster =
+    try {
+      val remote_hosts = build_context.build_hosts.filter(_.is_remote)
+      if (build_context.master && _build_database.isDefined && remote_hosts.nonEmpty) {
+        Some(init_cluster(remote_hosts))
+      }
+      else None
+    }
+    catch { case exn: Throwable => close(); throw exn }
+
   def close(): Unit = synchronized {
     Option(_database_server).flatten.foreach(_.close())
     Option(_build_database).flatten.foreach(_.close())
     Option(_host_database).flatten.foreach(_.close())
+    Option(_build_cluster).flatten.foreach(_.close())
     progress match {
       case db_progress: Database_Progress =>
         db_progress.exit(close = true)
@@ -922,6 +936,7 @@
     }
   }
 
+
   /* global state: internal var vs. external database */
 
   private var _state: Build_Process.State = Build_Process.State()
@@ -1111,13 +1126,9 @@
     else {
       if (build_context.master) start_build()
       start_worker()
+      _build_cluster.foreach(_.start())
 
-      if (build_context.master && build_context.build_hosts.nonEmpty) {
-        build_progress.echo("Remote build hosts:\n" +
-          cat_lines(build_context.build_hosts.map("  " + _)))
-      }
-
-      if (build_context.master && !build_context.worker_active) {
+      if (build_context.master && !build_context.worker_active && _build_cluster.isDefined) {
         build_progress.echo("Waiting for external workers ...")
       }
 
@@ -1140,6 +1151,7 @@
         }
       }
       finally {
+        _build_cluster.foreach(_.stop())
         stop_worker()
         if (build_context.master) stop_build()
       }