author | wenzelm |
Fri, 16 Feb 2024 11:12:42 +0100 | |
changeset 79627 | 0f01c575ff3e |
parent 79626 | 73b8ac4b0492 |
child 79632 | 463f94c504a4 |
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" |
78567 | 27 |
private val SHARED = "shared" |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
28 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
29 |
val parameters: Options = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
30 |
Options.inline(""" |
78925 | 31 |
option hostname : string = "" -- "explicit SSH hostname" |
32 |
option user : string = "" -- "explicit SSH user" |
|
33 |
option port : int = 0 -- "explicit SSH port" |
|
34 |
option jobs : int = 1 -- "maximum number of parallel jobs" |
|
35 |
option numa : bool = false -- "cyclic shuffling of NUMA CPU nodes" |
|
36 |
option dirs : string = "" -- "additional session directories (separated by colon)" |
|
37 |
option shared : bool = false -- "shared directory: omit sync + init" |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
38 |
""") |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
39 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
40 |
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
|
41 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
42 |
lazy val test_options: Options = Options.init0() |
78399 | 43 |
|
44 |
def apply( |
|
78416 | 45 |
name: String = "", |
78925 | 46 |
hostname: String = parameters.string(HOSTNAME), |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
47 |
user: String = parameters.string(USER), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
48 |
port: Int = parameters.int(PORT), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
49 |
jobs: Int = parameters.int(JOBS), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
50 |
numa: Boolean = parameters.bool(NUMA), |
78580 | 51 |
dirs: String = parameters.string(DIRS), |
78567 | 52 |
shared: Boolean = parameters.bool(SHARED), |
78399 | 53 |
options: List[Options.Spec] = Nil |
78580 | 54 |
): Host = { |
55 |
Path.split(dirs) // check |
|
78925 | 56 |
new Host(name, hostname, user, port, jobs, numa, dirs, shared, options) |
78580 | 57 |
} |
78401 | 58 |
|
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
59 |
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
|
60 |
def err(msg: String): Nothing = |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
61 |
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
|
62 |
|
78578 | 63 |
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
|
64 |
val more_specs = |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
65 |
try { |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
66 |
val n = str.length |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
67 |
val m = names.length |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
68 |
val l = |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
69 |
if (m == n) n |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
70 |
else if (str(m) == ':') m + 1 |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
71 |
else error("Missing \":\" after host name") |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
72 |
Options.Spec.parse(str.substring(l)) |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
73 |
} |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
74 |
catch { case ERROR(msg) => err(msg) } |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
75 |
|
78965 | 76 |
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
} |
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
81 |
|
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
82 |
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
|
83 |
yield { |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
84 |
val (params, options) = |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
85 |
try { |
78964
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
86 |
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
|
87 |
(parameters ++ specs1, { test_options ++ specs2; specs2 }) |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
88 |
} |
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
89 |
catch { case ERROR(msg) => err(msg) } |
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
90 |
|
78964
a2de1f6ff94e
support for "cluster" table with "hosts" array, and params/options as for "host" table;
wenzelm
parents:
78963
diff
changeset
|
91 |
apply(name = host, |
78925 | 92 |
hostname = params.string(HOSTNAME), |
78578 | 93 |
user = params.string(USER), |
94 |
port = params.int(PORT), |
|
95 |
jobs = params.int(JOBS), |
|
96 |
numa = params.bool(NUMA), |
|
78580 | 97 |
dirs = params.string(DIRS), |
78578 | 98 |
shared = params.bool(SHARED), |
99 |
options = options) |
|
100 |
} |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
101 |
} |
78943 | 102 |
|
78945
73162a487f94
build cluster host specifications are based on registry entries (table prefix "host");
wenzelm
parents:
78943
diff
changeset
|
103 |
def parse_single(registry: Registry, str: String): Host = |
79626 | 104 |
Library.the_single(parse(registry, str), message = "Single host expected: " + quote(str)) |
78399 | 105 |
} |
106 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
107 |
class Host( |
78427 | 108 |
val name: String, |
78925 | 109 |
val hostname: String, |
78427 | 110 |
val user: String, |
111 |
val port: Int, |
|
112 |
val jobs: Int, |
|
113 |
val numa: Boolean, |
|
78580 | 114 |
val dirs: String, |
78567 | 115 |
val shared: Boolean, |
78427 | 116 |
val options: List[Options.Spec] |
78399 | 117 |
) { |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
118 |
host => |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
119 |
|
78925 | 120 |
def ssh_host: String = proper_string(hostname) getOrElse name |
121 |
def is_local: Boolean = SSH.is_local(ssh_host) |
|
79619 | 122 |
def is_remote: Boolean = !is_local |
78413 | 123 |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
124 |
override def toString: String = print |
78399 | 125 |
|
126 |
def print: String = { |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
127 |
val params = |
78399 | 128 |
List( |
78925 | 129 |
if (host.hostname.isEmpty) "" else Options.Spec.print(Host.HOSTNAME, host.hostname), |
78560 | 130 |
if (host.user.isEmpty) "" else Options.Spec.print(Host.USER, host.user), |
131 |
if (host.port == 0) "" else Options.Spec.print(Host.PORT, host.port.toString), |
|
132 |
if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString), |
|
78567 | 133 |
if_proper(host.numa, Host.NUMA), |
78580 | 134 |
if_proper(dirs, Options.Spec.print(Host.DIRS, host.dirs)), |
78567 | 135 |
if_proper(host.shared, Host.SHARED) |
78399 | 136 |
).filter(_.nonEmpty) |
78560 | 137 |
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
|
138 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
139 |
SSH.print_local(host.name) + if_proper(rest, ":" + rest) |
78399 | 140 |
} |
141 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
142 |
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
|
143 |
|
78926 | 144 |
def open_ssh(options: Options): SSH.System = |
145 |
SSH.open_system(options ++ host.options, ssh_host, port = host.port, user = host.user) |
|
146 |
||
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
147 |
def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = { |
78926 | 148 |
val ssh_options = build_context.build_options ++ host.options |
149 |
val ssh = open_ssh(build_context.build_options) |
|
150 |
new Session(build_context, host, ssh_options, ssh, progress) |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
151 |
} |
78399 | 152 |
} |
78413 | 153 |
|
154 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
155 |
/* SSH sessions */ |
78413 | 156 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
157 |
class Session( |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
158 |
val build_context: Build.Context, |
78433 | 159 |
val host: Host, |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
160 |
val options: Options, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
161 |
val ssh: SSH.System, |
78433 | 162 |
val progress: Progress |
163 |
) extends AutoCloseable { |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
164 |
override def toString: String = ssh.toString |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
165 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
166 |
val remote_identifier: String = options.string("build_cluster_identifier") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
167 |
val remote_root: Path = Path.explode(options.string("build_cluster_root")) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
168 |
val remote_isabelle_home: Path = remote_root + Path.explode("isabelle") |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
169 |
val remote_afp_root: Option[Path] = |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
170 |
if (build_context.afp_root.isEmpty) None |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
171 |
else Some(remote_isabelle_home + Path.explode("AFP")) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
172 |
|
78443 | 173 |
lazy val remote_isabelle: Other_Isabelle = |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
174 |
Other_Isabelle(remote_isabelle_home, isabelle_identifier = remote_identifier, ssh = ssh) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
175 |
|
78443 | 176 |
def sync(): Other_Isabelle = { |
177 |
Sync.sync(options, Rsync.Context(ssh = ssh), remote_isabelle_home, |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
178 |
afp_root = build_context.afp_root, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
179 |
purge_heaps = true, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
180 |
preserve_jars = true) |
78443 | 181 |
remote_isabelle |
182 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
183 |
|
78443 | 184 |
def init(): Unit = remote_isabelle.init() |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
185 |
|
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
|
186 |
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
|
187 |
val script = |
79620 | 188 |
Build_Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home) |
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
|
189 |
remote_isabelle.bash(script).check |
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
|
190 |
} |
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
|
191 |
|
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
|
192 |
def start(): Process_Result = { |
78572 | 193 |
val remote_ml_platform = remote_isabelle.getenv("ML_PLATFORM") |
194 |
if (remote_ml_platform != build_context.ml_platform) { |
|
195 |
error("Bad ML_PLATFORM: found " + remote_ml_platform + |
|
196 |
", but expected " + build_context.ml_platform) |
|
197 |
} |
|
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
|
198 |
val build_options = |
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
|
199 |
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
|
200 |
val script = |
78558 | 201 |
Build.build_worker_command(host, |
78556 | 202 |
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
|
203 |
build_options = build_options.toList, |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
204 |
build_id = build_context.build_uuid, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
205 |
isabelle_home = remote_isabelle_home, |
78580 | 206 |
afp_root = remote_afp_root, |
78638
28a2c55648d5
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
wenzelm
parents:
78584
diff
changeset
|
207 |
dirs = Path.split(host.dirs).map(remote_isabelle.expand_path), |
28a2c55648d5
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
wenzelm
parents:
78584
diff
changeset
|
208 |
quiet = true) |
78584
92ef737f412c
removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);
wenzelm
parents:
78582
diff
changeset
|
209 |
remote_isabelle.bash(script).check |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
210 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
211 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
212 |
override def close(): Unit = ssh.close() |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
213 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
214 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
215 |
class Result(val host: Host, val process_result: Exn.Result[Process_Result]) { |
78443 | 216 |
def rc: Int = Process_Result.RC(process_result) |
217 |
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
|
218 |
} |
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
|
219 |
|
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
|
220 |
|
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
|
221 |
/* 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
|
222 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
223 |
object none extends Build_Cluster { |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
224 |
override def toString: String = "Build_Cluster.none" |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
225 |
} |
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
|
226 |
|
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
|
227 |
def make(build_context: Build.Context, progress: Progress = new Progress): Build_Cluster = { |
79619 | 228 |
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
|
229 |
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
|
230 |
else new Remote_Build_Cluster(build_context, remote_hosts, progress = progress) |
78413 | 231 |
} |
78398 | 232 |
} |
78413 | 233 |
|
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
|
234 |
// 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
|
235 |
trait Build_Cluster extends AutoCloseable { |
78443 | 236 |
def rc: Int = Process_Result.RC.ok |
237 |
def ok: Boolean = rc == Process_Result.RC.ok |
|
238 |
def return_code(rc: Int): Unit = () |
|
239 |
def return_code(res: Process_Result): Unit = return_code(res.rc) |
|
240 |
def return_code(exn: Throwable): Unit = return_code(Process_Result.RC(exn)) |
|
79627 | 241 |
def open(): Build_Cluster = this |
242 |
def init(): Build_Cluster = this |
|
243 |
def benchmark(): Build_Cluster = this |
|
244 |
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
|
245 |
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
|
246 |
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
|
247 |
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
|
248 |
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
|
249 |
} |
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
|
250 |
|
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 |
class Remote_Build_Cluster( |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
252 |
val build_context: Build.Context, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
253 |
val remote_hosts: List[Build_Cluster.Host], |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
254 |
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
|
255 |
) extends Build_Cluster { |
79619 | 256 |
require(remote_hosts.nonEmpty && remote_hosts.forall(_.is_remote), "remote hosts required") |
78413 | 257 |
|
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
|
258 |
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
|
259 |
remote_hosts.iterator.map(_.name).mkString("Build_Cluster(", ", ", ")") |
78413 | 260 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
261 |
|
78443 | 262 |
/* cumulative return code */ |
263 |
||
78581 | 264 |
private val _rc = Synchronized(Process_Result.RC.ok) |
78443 | 265 |
|
78581 | 266 |
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
|
267 |
|
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
|
268 |
override def return_code(rc: Int): Unit = |
78581 | 269 |
_rc.change(rc0 => Process_Result.RC.merge(rc0, rc)) |
78443 | 270 |
|
271 |
def capture[A](host: Build_Cluster.Host, op: String)( |
|
272 |
e: => A, |
|
273 |
msg: String = host.message(op + " ..."), |
|
78506 | 274 |
err: Throwable => String = { exn => |
275 |
return_code(exn) |
|
276 |
host.message("failed to " + op + "\n" + Exn.print(exn)) |
|
277 |
} |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
278 |
): Exn.Result[A] = { |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
279 |
progress.capture(e, msg = msg, err = err) |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
280 |
} |
78443 | 281 |
|
282 |
||
283 |
/* open remote sessions */ |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
284 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
285 |
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
|
286 |
|
79627 | 287 |
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
|
288 |
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
|
289 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
290 |
val attempts = |
78433 | 291 |
Par_List.map((host: Build_Cluster.Host) => |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
292 |
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
|
293 |
remote_hosts, thread = true) |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
294 |
|
78674 | 295 |
if (attempts.forall(Exn.is_res)) { |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
296 |
_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
|
297 |
_sessions |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
298 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
299 |
else { |
78592 | 300 |
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
|
301 |
error("Failed to connect build cluster") |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
302 |
} |
79627 | 303 |
|
304 |
this |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
305 |
} |
78413 | 306 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
307 |
|
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
|
308 |
/* init and benchmark remote Isabelle distributions */ |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
309 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
310 |
private var _init = List.empty[Future[Unit]] |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
311 |
|
79627 | 312 |
override def init(): Build_Cluster = synchronized { |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
313 |
require(_sessions.nonEmpty, "build cluster not yet open") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
314 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
315 |
if (_init.isEmpty) { |
78443 | 316 |
_init = |
78567 | 317 |
for (session <- _sessions if !session.host.shared) yield { |
78443 | 318 |
Future.thread(session.host.message("session")) { |
319 |
capture(session.host, "sync") { session.sync() } |
|
320 |
capture(session.host, "init") { session.init() } |
|
321 |
} |
|
322 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
323 |
} |
79627 | 324 |
|
325 |
this |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
326 |
} |
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
|
327 |
|
79627 | 328 |
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
|
329 |
_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
|
330 |
_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
|
331 |
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
|
332 |
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
|
333 |
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
|
334 |
} |
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
|
335 |
} |
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
|
336 |
_init.foreach(_.join) |
79627 | 337 |
|
338 |
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
|
339 |
} |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
340 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
341 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
342 |
/* workers */ |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
343 |
|
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
|
344 |
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
|
345 |
|
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
|
346 |
override def active(): Boolean = synchronized { _workers.nonEmpty } |
78413 | 347 |
|
79627 | 348 |
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
|
349 |
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
|
350 |
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
|
351 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
352 |
init() |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
353 |
_init.foreach(_.join) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
354 |
|
78443 | 355 |
_workers = |
356 |
for (session <- _sessions) yield { |
|
78582 | 357 |
Future.thread(session.host.message("work")) { |
358 |
Exn.release(capture(session.host, "work") { session.start() }) |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
359 |
} |
78443 | 360 |
} |
79627 | 361 |
|
362 |
this |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
363 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
364 |
|
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
|
365 |
override def join: List[Build_Cluster.Result] = synchronized { |
78443 | 366 |
_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
|
367 |
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
|
368 |
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
|
369 |
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
|
370 |
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
|
371 |
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
|
372 |
} |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
373 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
374 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
375 |
|
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
|
376 |
/* close */ |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
377 |
|
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
|
378 |
override def close(): Unit = synchronized { |
78441 | 379 |
_init.foreach(_.join) |
78639
ca56952b7322
proper stop of build_process shutdown, despite errors on workers;
wenzelm
parents:
78638
diff
changeset
|
380 |
_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
|
381 |
_sessions.foreach(_.close()) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
382 |
|
78443 | 383 |
_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
|
384 |
_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
|
385 |
_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
|
386 |
} |
78413 | 387 |
} |