--- a/src/Pure/Tools/build_cluster.scala Tue Jul 18 20:14:57 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Tue Jul 18 21:06:11 2023 +0200
@@ -9,4 +9,44 @@
object Build_Cluster {
+ object Host {
+ val PORT = "port"
+ val JOBS = "jobs"
+ val NUMA = "numa"
+
+ def apply(
+ host: String,
+ user: String = "",
+ port: Int = 0,
+ jobs: Int = 1,
+ numa: Boolean = false,
+ options: List[Options.Spec] = Nil
+ ): Host = new Host(host, user, port, jobs, numa, options)
+ }
+
+ final class Host private(
+ host: String,
+ user: String,
+ port: Int,
+ jobs: Int,
+ numa: Boolean,
+ options: List[Options.Spec]
+ ) {
+ require(host.nonEmpty, "Undefined host name")
+
+ override def toString: String = print
+ def print: String = {
+ val props =
+ List(
+ if (port == 0) "" else Properties.Eq(Host.PORT, port.toString),
+ if (jobs == 1) "" else Properties.Eq(Host.JOBS, jobs.toString),
+ if_proper(numa, Host.NUMA)
+ ).filter(_.nonEmpty)
+ val rest = (props ::: options).mkString(",")
+ if_proper(user, user + "@") + host + if_proper(rest, ":" + rest)
+ }
+
+ def open_ssh_session(options: Options): SSH.Session =
+ SSH.open_session(options, host, port = port, user = user)
+ }
}