author | wenzelm |
Thu, 06 Jun 2024 12:53:02 +0200 | |
changeset 80268 | 979f3893aa37 |
parent 80200 | 5f053991315c |
permissions | -rw-r--r-- |
79502 | 1 |
/* Title: Pure/Build/build_cluster.scala |
78398 | 2 |
Author: Makarius |
3 |
||
4 |
Management of build cluster: independent ssh hosts with access to shared |
|
5 |
PostgreSQL server. |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
6 |
|
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
7 |
NB: extensible classes allow quite different implementations in user-space, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
8 |
via the service class Build.Engine and overridable methods |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
9 |
Build.Engine.open_build_process(), Build_Process.open_build_cluster(). |
78398 | 10 |
*/ |
11 |
||
12 |
package isabelle |
|
13 |
||
14 |
||
15 |
object Build_Cluster { |
|
78413 | 16 |
/* host specifications */ |
17 |
||
78399 | 18 |
object Host { |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
19 |
private val rfc822_specials = """()<>@,;:\"[]""" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
20 |
|
78925 | 21 |
private val HOSTNAME = "hostname" |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
22 |
private val USER = "user" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
23 |
private val PORT = "port" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
24 |
private val JOBS = "jobs" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
25 |
private val NUMA = "numa" |
78580 | 26 |
private val DIRS = "dirs" |
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
27 |
private val HOME = "home" |
78567 | 28 |
private val SHARED = "shared" |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
29 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
30 |
val parameters: Options = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
31 |
Options.inline(""" |
78925 | 32 |
option hostname : string = "" -- "explicit SSH hostname" |
33 |
option user : string = "" -- "explicit SSH user" |
|
34 |
option port : int = 0 -- "explicit SSH port" |
|
35 |
option jobs : int = 1 -- "maximum number of parallel jobs" |
|
36 |
option numa : bool = false -- "cyclic shuffling of NUMA CPU nodes" |
|
37 |
option dirs : string = "" -- "additional session directories (separated by colon)" |
|
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
38 |
option home : string = "" -- "alternative user home (via $USER_HOME)" |
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
39 |
option shared : bool = false -- "shared home directory: omit sync + init" |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
40 |
""") |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
41 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
42 |
def is_parameter(spec: Options.Spec): Boolean = parameters.defined(spec.name) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
43 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
44 |
lazy val test_options: Options = Options.init0() |
78399 | 45 |
|
46 |
def apply( |
|
78416 | 47 |
name: String = "", |
78925 | 48 |
hostname: String = parameters.string(HOSTNAME), |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
49 |
user: String = parameters.string(USER), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
50 |
port: Int = parameters.int(PORT), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
51 |
jobs: Int = parameters.int(JOBS), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
52 |
numa: Boolean = parameters.bool(NUMA), |
78580 | 53 |
dirs: String = parameters.string(DIRS), |
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
54 |
home: String = parameters.string(HOME), |
78567 | 55 |
shared: Boolean = parameters.bool(SHARED), |
78399 | 56 |
options: List[Options.Spec] = Nil |
78580 | 57 |
): Host = { |
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
58 |
new Host(name, hostname, user, port, jobs, numa, dirs, home, shared, options) |
78580 | 59 |
} |
78401 | 60 |
|
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
61 |
def parse(registry: Registry, str: String): List[Host] = { |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
62 |
def err(msg: String): Nothing = |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
63 |
cat_error(msg, "The error(s) above occurred in host specification " + quote(str)) |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
64 |
|
78578 | 65 |
val names = str.takeWhile(c => !rfc822_specials.contains(c) || c == ',') |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
66 |
val more_specs = |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
67 |
try { |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
68 |
val n = str.length |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
69 |
val m = names.length |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
70 |
val l = |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
71 |
if (m == n) n |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
72 |
else if (str(m) == ':') m + 1 |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
73 |
else error("Missing \":\" after host name") |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
74 |
Options.Spec.parse(str.substring(l)) |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
75 |
} |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
76 |
catch { case ERROR(msg) => err(msg) } |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
77 |
|
78965 | 78 |
def get_registry(a: String): Registry.Cluster.Value = |
78964
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
79 |
Registry.Cluster.try_unqualify(a) match { |
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
80 |
case Some(b) => Registry.Cluster.get(registry, b) |
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
81 |
case None => List(a -> Registry.Host.get(registry, a)) |
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
82 |
} |
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
83 |
|
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
84 |
for (name <- space_explode(',', names); (host, host_specs) <- get_registry(name)) |
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
85 |
yield { |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
86 |
val (params, options) = |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
87 |
try { |
78964
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
88 |
val (specs1, specs2) = (host_specs ::: more_specs).partition(is_parameter) |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
89 |
(parameters ++ specs1, { test_options ++ specs2; specs2 }) |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
90 |
} |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
91 |
catch { case ERROR(msg) => err(msg) } |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
92 |
|
78964
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
93 |
apply(name = host, |
78925 | 94 |
hostname = params.string(HOSTNAME), |
78578 | 95 |
user = params.string(USER), |
96 |
port = params.int(PORT), |
|
97 |
jobs = params.int(JOBS), |
|
98 |
numa = params.bool(NUMA), |
|
78580 | 99 |
dirs = params.string(DIRS), |
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
100 |
home = params.string(HOME), |
78578 | 101 |
shared = params.bool(SHARED), |
102 |
options = options) |
|
103 |
} |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
104 |
} |
78943 | 105 |
|
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
106 |
def parse_single(registry: Registry, str: String): Host = |
79626 | 107 |
Library.the_single(parse(registry, str), message = "Single host expected: " + quote(str)) |
78399 | 108 |
} |
109 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
110 |
class Host( |
78427 | 111 |
val name: String, |
78925 | 112 |
val hostname: String, |
78427 | 113 |
val user: String, |
114 |
val port: Int, |
|
115 |
val jobs: Int, |
|
116 |
val numa: Boolean, |
|
78580 | 117 |
val dirs: String, |
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
118 |
val home: String, |
78567 | 119 |
val shared: Boolean, |
78427 | 120 |
val options: List[Options.Spec] |
78399 | 121 |
) { |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
122 |
host => |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
123 |
|
79636 | 124 |
Path.split(host.dirs) // check |
125 |
||
79637 | 126 |
def ssh_host: String = proper_string(host.hostname) getOrElse host.name |
78925 | 127 |
def is_local: Boolean = SSH.is_local(ssh_host) |
79619 | 128 |
def is_remote: Boolean = !is_local |
78413 | 129 |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
130 |
override def toString: String = print |
78399 | 131 |
|
132 |
def print: String = { |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
133 |
val params = |
78399 | 134 |
List( |
78925 | 135 |
if (host.hostname.isEmpty) "" else Options.Spec.print(Host.HOSTNAME, host.hostname), |
78560 | 136 |
if (host.user.isEmpty) "" else Options.Spec.print(Host.USER, host.user), |
137 |
if (host.port == 0) "" else Options.Spec.print(Host.PORT, host.port.toString), |
|
138 |
if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString), |
|
78567 | 139 |
if_proper(host.numa, Host.NUMA), |
79632 | 140 |
if_proper(host.dirs, Options.Spec.print(Host.DIRS, host.dirs)), |
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
141 |
if_proper(host.home, Options.Spec.print(Host.HOME, host.home)), |
78567 | 142 |
if_proper(host.shared, Host.SHARED) |
78399 | 143 |
).filter(_.nonEmpty) |
78560 | 144 |
val rest = (params ::: host.options.map(_.print)).mkString(",") |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
145 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
146 |
SSH.print_local(host.name) + if_proper(rest, ":" + rest) |
78399 | 147 |
} |
148 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
149 |
def message(msg: String): String = "Host " + quote(host.name) + if_proper(msg, ": " + msg) |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
150 |
|
78926 | 151 |
def open_ssh(options: Options): SSH.System = |
79634
432217a1e990
support for alternative user home, e.g. to avoid slow NFS shares;
wenzelm
parents:
79632
diff
changeset
|
152 |
SSH.open_system(options ++ host.options, ssh_host, port = host.port, |
79637 | 153 |
user = host.user, user_home = host.home) |
78926 | 154 |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
155 |
def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = { |
78926 | 156 |
val ssh_options = build_context.build_options ++ host.options |
157 |
val ssh = open_ssh(build_context.build_options) |
|
158 |
new Session(build_context, host, ssh_options, ssh, progress) |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
159 |
} |
78399 | 160 |
} |
78413 | 161 |
|
162 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
163 |
/* SSH sessions */ |
78413 | 164 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
165 |
class Session( |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
166 |
val build_context: Build.Context, |
78433 | 167 |
val host: Host, |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
168 |
val options: Options, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
169 |
val ssh: SSH.System, |
78433 | 170 |
val progress: Progress |
171 |
) extends AutoCloseable { |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
172 |
override def toString: String = ssh.toString |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
173 |
|
79704 | 174 |
val build_cluster_identifier: String = options.string("build_cluster_identifier") |
80200 | 175 |
val build_cluster_isabelle_home: Path = |
176 |
Path.explode(options.string("build_cluster_root")) + Path.explode("isabelle") |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
177 |
|
79704 | 178 |
lazy val build_cluster_isabelle: Other_Isabelle = |
80199 | 179 |
Other_Isabelle(build_cluster_isabelle_home, |
79704 | 180 |
isabelle_identifier = build_cluster_identifier, ssh = ssh) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
181 |
|
78443 | 182 |
def sync(): Other_Isabelle = { |
80198
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
183 |
val context = Rsync.Context(ssh = ssh) |
80199 | 184 |
val target = build_cluster_isabelle_home |
80198
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
185 |
if (Mercurial.Hg_Sync.ok(Path.ISABELLE_HOME)) { |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
186 |
val source = File.standard_path(Path.ISABELLE_HOME) |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
187 |
Rsync.exec(context, clean = true, |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
188 |
args = List("--", Url.direct_path(source), context.target(target))).check |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
189 |
} |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
190 |
else { |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
191 |
Sync.sync(options, context, target, |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
192 |
purge_heaps = true, |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
193 |
preserve_jars = true, |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
194 |
dirs = Sync.afp_dirs(build_context.afp_root)) |
7883f221d6d3
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
wenzelm
parents:
80196
diff
changeset
|
195 |
} |
79704 | 196 |
build_cluster_isabelle |
78443 | 197 |
} |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
198 |
|
79681
df1059ea8846
propagate property "isabelle.debug", notably for Java/Scala exception trace;
wenzelm
parents:
79637
diff
changeset
|
199 |
def init(): Unit = |
79704 | 200 |
build_cluster_isabelle.init(other_settings = |
201 |
build_cluster_isabelle.init_components() ::: build_cluster_isabelle.debug_settings()) |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
202 |
|
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
203 |
def benchmark(): Unit = { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
204 |
val script = |
79948
8fe1ed4b5705
option for benchmark session;
Fabian Huch <huch@in.tum.de>
parents:
79704
diff
changeset
|
205 |
Build_Benchmark.benchmark_command(options, host, ssh = ssh, |
80199 | 206 |
isabelle_home = build_cluster_isabelle_home) |
79704 | 207 |
build_cluster_isabelle.bash(script).check |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
208 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
209 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
210 |
def start(): Process_Result = { |
79704 | 211 |
val build_cluster_ml_platform = build_cluster_isabelle.getenv("ML_PLATFORM") |
212 |
if (build_cluster_ml_platform != build_context.ml_platform) { |
|
213 |
error("Bad ML_PLATFORM: found " + build_cluster_ml_platform + |
|
78572 | 214 |
", but expected " + build_context.ml_platform) |
215 |
} |
|
79704 | 216 |
val build_options = |
79526
6e5397fcc41b
add build_sync tag to sync certain options (e.g., build_engine) across build processes;
Fabian Huch <huch@in.tum.de>
parents:
79502
diff
changeset
|
217 |
for { option <- options.iterator if option.for_build_sync } yield options.spec(option.name) |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
218 |
val script = |
78558 | 219 |
Build.build_worker_command(host, |
78556 | 220 |
ssh = ssh, |
79526
6e5397fcc41b
add build_sync tag to sync certain options (e.g., build_engine) across build processes;
Fabian Huch <huch@in.tum.de>
parents:
79502
diff
changeset
|
221 |
build_options = build_options.toList, |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
222 |
build_id = build_context.build_uuid, |
80199 | 223 |
isabelle_home = build_cluster_isabelle_home, |
79704 | 224 |
dirs = Path.split(host.dirs).map(build_cluster_isabelle.expand_path), |
78638
28a2c55648d5
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
wenzelm
parents:
78584
diff
changeset
|
225 |
quiet = true) |
79704 | 226 |
build_cluster_isabelle.bash(script).check |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
227 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
228 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
229 |
override def close(): Unit = ssh.close() |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
230 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
231 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
232 |
class Result(val host: Host, val process_result: Exn.Result[Process_Result]) { |
78443 | 233 |
def rc: Int = Process_Result.RC(process_result) |
234 |
def ok: Boolean = rc == Process_Result.RC.ok |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
235 |
} |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
236 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
237 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
238 |
/* build clusters */ |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
239 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
240 |
object none extends Build_Cluster { |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
241 |
override def toString: String = "Build_Cluster.none" |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
242 |
} |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
243 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
244 |
def make(build_context: Build.Context, progress: Progress = new Progress): Build_Cluster = { |
79619 | 245 |
val remote_hosts = build_context.build_hosts.filter(_.is_remote) |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
246 |
if (remote_hosts.isEmpty) none |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
247 |
else new Remote_Build_Cluster(build_context, remote_hosts, progress = progress) |
78413 | 248 |
} |
78398 | 249 |
} |
78413 | 250 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
251 |
// NB: extensible via Build.Engine.build_process() and Build_Process.init_cluster() |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
252 |
trait Build_Cluster extends AutoCloseable { |
78443 | 253 |
def rc: Int = Process_Result.RC.ok |
254 |
def ok: Boolean = rc == Process_Result.RC.ok |
|
255 |
def return_code(rc: Int): Unit = () |
|
256 |
def return_code(res: Process_Result): Unit = return_code(res.rc) |
|
257 |
def return_code(exn: Throwable): Unit = return_code(Process_Result.RC(exn)) |
|
79627 | 258 |
def open(): Build_Cluster = this |
259 |
def init(): Build_Cluster = this |
|
260 |
def benchmark(): Build_Cluster = this |
|
261 |
def start(): Build_Cluster = this |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
262 |
def active(): Boolean = false |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
263 |
def join: List[Build_Cluster.Result] = Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
264 |
def stop(): Unit = { join; close() } |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
265 |
override def close(): Unit = () |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
266 |
} |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
267 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
268 |
class Remote_Build_Cluster( |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
269 |
val build_context: Build.Context, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
270 |
val remote_hosts: List[Build_Cluster.Host], |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
271 |
val progress: Progress = new Progress |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
272 |
) extends Build_Cluster { |
79619 | 273 |
require(remote_hosts.nonEmpty && remote_hosts.forall(_.is_remote), "remote hosts required") |
78413 | 274 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
275 |
override def toString: String = |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
276 |
remote_hosts.iterator.map(_.name).mkString("Build_Cluster(", ", ", ")") |
78413 | 277 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
278 |
|
78443 | 279 |
/* cumulative return code */ |
280 |
||
78581 | 281 |
private val _rc = Synchronized(Process_Result.RC.ok) |
78443 | 282 |
|
78581 | 283 |
override def rc: Int = _rc.value |
78499
a7dab3b8ebfe
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;
wenzelm
parents:
78447
diff
changeset
|
284 |
|
a7dab3b8ebfe
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;
wenzelm
parents:
78447
diff
changeset
|
285 |
override def return_code(rc: Int): Unit = |
78581 | 286 |
_rc.change(rc0 => Process_Result.RC.merge(rc0, rc)) |
78443 | 287 |
|
288 |
def capture[A](host: Build_Cluster.Host, op: String)( |
|
289 |
e: => A, |
|
290 |
msg: String = host.message(op + " ..."), |
|
78506 | 291 |
err: Throwable => String = { exn => |
292 |
return_code(exn) |
|
293 |
host.message("failed to " + op + "\n" + Exn.print(exn)) |
|
294 |
} |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
295 |
): Exn.Result[A] = { |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
296 |
progress.capture(e, msg = msg, err = err) |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
297 |
} |
78443 | 298 |
|
299 |
||
300 |
/* open remote sessions */ |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
301 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
302 |
private var _sessions = List.empty[Build_Cluster.Session] |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
303 |
|
79627 | 304 |
override def open(): Build_Cluster = synchronized { |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
305 |
require(_sessions.isEmpty, "build cluster already open") |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
306 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
307 |
val attempts = |
78433 | 308 |
Par_List.map((host: Build_Cluster.Host) => |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
309 |
capture(host, "open") { host.open_session(build_context, progress = progress) }, |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
310 |
remote_hosts, thread = true) |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
311 |
|
78674 | 312 |
if (attempts.forall(Exn.is_res)) { |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
313 |
_sessions = attempts.map(Exn.the_res) |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
314 |
_sessions |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
315 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
316 |
else { |
78592 | 317 |
for (case Exn.Res(session) <- attempts) session.close() |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
318 |
error("Failed to connect build cluster") |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
319 |
} |
79627 | 320 |
|
321 |
this |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
322 |
} |
78413 | 323 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
324 |
|
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
325 |
/* init and benchmark remote Isabelle distributions */ |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
326 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
327 |
private var _init = List.empty[Future[Unit]] |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
328 |
|
79627 | 329 |
override def init(): Build_Cluster = synchronized { |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
330 |
require(_sessions.nonEmpty, "build cluster not yet open") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
331 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
332 |
if (_init.isEmpty) { |
78443 | 333 |
_init = |
78567 | 334 |
for (session <- _sessions if !session.host.shared) yield { |
78443 | 335 |
Future.thread(session.host.message("session")) { |
336 |
capture(session.host, "sync") { session.sync() } |
|
337 |
capture(session.host, "init") { session.init() } |
|
338 |
} |
|
339 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
340 |
} |
79627 | 341 |
|
342 |
this |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
343 |
} |
79704 | 344 |
|
79627 | 345 |
override def benchmark(): Build_Cluster = synchronized { |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
346 |
_init.foreach(_.join) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
347 |
_init = |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
348 |
for (session <- _sessions if !session.host.shared) yield { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
349 |
Future.thread(session.host.message("session")) { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
350 |
capture(session.host, "benchmark") { session.benchmark() } |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
351 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
352 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
353 |
_init.foreach(_.join) |
79627 | 354 |
|
355 |
this |
|
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
356 |
} |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
357 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
358 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
359 |
/* workers */ |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
360 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
361 |
private var _workers = List.empty[Future[Process_Result]] |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
362 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
363 |
override def active(): Boolean = synchronized { _workers.nonEmpty } |
78413 | 364 |
|
79627 | 365 |
override def start(): Build_Cluster = synchronized { |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
366 |
require(_sessions.nonEmpty, "build cluster not yet open") |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
367 |
require(_workers.isEmpty, "build cluster already active") |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
368 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
369 |
init() |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
370 |
_init.foreach(_.join) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
371 |
|
78443 | 372 |
_workers = |
373 |
for (session <- _sessions) yield { |
|
78582 | 374 |
Future.thread(session.host.message("work")) { |
375 |
Exn.release(capture(session.host, "work") { session.start() }) |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
376 |
} |
78443 | 377 |
} |
79627 | 378 |
|
379 |
this |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
380 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
381 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
382 |
override def join: List[Build_Cluster.Result] = synchronized { |
78443 | 383 |
_init.foreach(_.join) |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
384 |
if (_workers.isEmpty) Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
385 |
else { |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
386 |
assert(_sessions.length == _workers.length) |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
387 |
for ((session, worker) <- _sessions zip _workers) |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
388 |
yield Build_Cluster.Result(session.host, worker.join_result) |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
389 |
} |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
390 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
391 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
392 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
393 |
/* close */ |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
394 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
395 |
override def close(): Unit = synchronized { |
78441 | 396 |
_init.foreach(_.join) |
78639
ca56952b7322
proper stop of build_process shutdown, despite errors on workers;
wenzelm
parents:
78638
diff
changeset
|
397 |
_workers.foreach(_.join_result) |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
398 |
_sessions.foreach(_.close()) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
399 |
|
78443 | 400 |
_init = Nil |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
401 |
_workers = Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
402 |
_sessions = Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
403 |
} |
78413 | 404 |
} |