# 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() }