author | wenzelm |
Sun, 03 Sep 2023 19:28:59 +0200 | |
changeset 78643 | d5a1d64a563d |
parent 78639 | ca56952b7322 |
parent 78592 | fdfe9b91d96e |
child 78674 | 88f47c70187a |
permissions | -rw-r--r-- |
78398 | 1 |
/* Title: Pure/Tools/build_cluster.scala |
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 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
21 |
private val USER = "user" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
22 |
private val PORT = "port" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
23 |
private val JOBS = "jobs" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
24 |
private val NUMA = "numa" |
78580 | 25 |
private val DIRS = "dirs" |
78567 | 26 |
private val SHARED = "shared" |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
27 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
28 |
val parameters: Options = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
29 |
Options.inline(""" |
78567 | 30 |
option user : string = "" -- "explicit SSH user" |
31 |
option port : int = 0 -- "explicit SSH port" |
|
32 |
option jobs : int = 1 -- "maximum number of parallel jobs" |
|
33 |
option numa : bool = false -- "cyclic shuffling of NUMA CPU nodes" |
|
78580 | 34 |
option dirs : string = "" -- "additional session directories (separated by colon)" |
78567 | 35 |
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
|
36 |
""") |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
37 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
38 |
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
|
39 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
40 |
lazy val test_options: Options = Options.init0() |
78399 | 41 |
|
42 |
def apply( |
|
78416 | 43 |
name: String = "", |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
44 |
user: String = parameters.string(USER), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
45 |
port: Int = parameters.int(PORT), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
46 |
jobs: Int = parameters.int(JOBS), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
47 |
numa: Boolean = parameters.bool(NUMA), |
78580 | 48 |
dirs: String = parameters.string(DIRS), |
78567 | 49 |
shared: Boolean = parameters.bool(SHARED), |
78399 | 50 |
options: List[Options.Spec] = Nil |
78580 | 51 |
): Host = { |
52 |
Path.split(dirs) // check |
|
53 |
new Host(name, user, port, jobs, numa, dirs, shared, options) |
|
54 |
} |
|
78401 | 55 |
|
78578 | 56 |
def parse(str: String): List[Host] = { |
57 |
val names = str.takeWhile(c => !rfc822_specials.contains(c) || c == ',') |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
58 |
val (params, options) = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
59 |
try { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
60 |
val rest = { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
61 |
val n = str.length |
78578 | 62 |
val m = names.length |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
63 |
val l = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
64 |
if (m == n) n |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
65 |
else if (str(m) == ':') m + 1 |
78423 | 66 |
else error("Missing \":\" after host name") |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
67 |
str.substring(l) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
68 |
} |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
69 |
val (specs1, specs2) = Options.parse_specs(rest).partition(is_parameter) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
70 |
(parameters ++ specs1, { test_options ++ specs2; specs2 }) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
71 |
} |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
72 |
catch { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
73 |
case ERROR(msg) => |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
74 |
cat_error(msg, "The error(s) above occurred in host specification " + quote(str)) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
75 |
} |
78578 | 76 |
for (name <- space_explode(',', names)) yield { |
77 |
apply(name = name, |
|
78 |
user = params.string(USER), |
|
79 |
port = params.int(PORT), |
|
80 |
jobs = params.int(JOBS), |
|
81 |
numa = params.bool(NUMA), |
|
78580 | 82 |
dirs = params.string(DIRS), |
78578 | 83 |
shared = params.bool(SHARED), |
84 |
options = options) |
|
85 |
} |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
86 |
} |
78399 | 87 |
} |
88 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
89 |
class Host( |
78427 | 90 |
val name: String, |
91 |
val user: String, |
|
92 |
val port: Int, |
|
93 |
val jobs: Int, |
|
94 |
val numa: Boolean, |
|
78580 | 95 |
val dirs: String, |
78567 | 96 |
val shared: Boolean, |
78427 | 97 |
val options: List[Options.Spec] |
78399 | 98 |
) { |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
99 |
host => |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
100 |
|
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
101 |
def is_local: Boolean = SSH.is_local(host.name) |
78413 | 102 |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
103 |
override def toString: String = print |
78399 | 104 |
|
105 |
def print: String = { |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
106 |
val params = |
78399 | 107 |
List( |
78560 | 108 |
if (host.user.isEmpty) "" else Options.Spec.print(Host.USER, host.user), |
109 |
if (host.port == 0) "" else Options.Spec.print(Host.PORT, host.port.toString), |
|
110 |
if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString), |
|
78567 | 111 |
if_proper(host.numa, Host.NUMA), |
78580 | 112 |
if_proper(dirs, Options.Spec.print(Host.DIRS, host.dirs)), |
78567 | 113 |
if_proper(host.shared, Host.SHARED) |
78399 | 114 |
).filter(_.nonEmpty) |
78560 | 115 |
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
|
116 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
117 |
SSH.print_local(host.name) + if_proper(rest, ":" + rest) |
78399 | 118 |
} |
119 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
120 |
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
|
121 |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
122 |
def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = { |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
123 |
val session_options = build_context.build_options ++ host.options |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
124 |
val ssh = SSH.open_session(session_options, host.name, port = host.port, user = host.user) |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
125 |
new Session(build_context, host, session_options, ssh, progress) |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
126 |
} |
78399 | 127 |
} |
78413 | 128 |
|
129 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
130 |
/* SSH sessions */ |
78413 | 131 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
132 |
class Session( |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
133 |
val build_context: Build.Context, |
78433 | 134 |
val host: Host, |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
135 |
val options: Options, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
136 |
val ssh: SSH.System, |
78433 | 137 |
val progress: Progress |
138 |
) extends AutoCloseable { |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
139 |
override def toString: String = ssh.toString |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
140 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
141 |
val remote_identifier: String = options.string("build_cluster_identifier") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
142 |
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
|
143 |
val remote_isabelle_home: Path = remote_root + Path.explode("isabelle") |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
144 |
val remote_afp_root: Option[Path] = |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
145 |
if (build_context.afp_root.isEmpty) None |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
146 |
else Some(remote_isabelle_home + Path.explode("AFP")) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
147 |
|
78443 | 148 |
lazy val remote_isabelle: Other_Isabelle = |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
149 |
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
|
150 |
|
78443 | 151 |
def sync(): Other_Isabelle = { |
152 |
Sync.sync(options, Rsync.Context(ssh = ssh), remote_isabelle_home, |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
153 |
afp_root = build_context.afp_root, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
154 |
purge_heaps = true, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
155 |
preserve_jars = true) |
78443 | 156 |
remote_isabelle |
157 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
158 |
|
78443 | 159 |
def init(): Unit = remote_isabelle.init() |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
160 |
|
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
|
161 |
def start(): Process_Result = { |
78572 | 162 |
val remote_ml_platform = remote_isabelle.getenv("ML_PLATFORM") |
163 |
if (remote_ml_platform != build_context.ml_platform) { |
|
164 |
error("Bad ML_PLATFORM: found " + remote_ml_platform + |
|
165 |
", but expected " + build_context.ml_platform) |
|
166 |
} |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
167 |
val script = |
78558 | 168 |
Build.build_worker_command(host, |
78556 | 169 |
ssh = ssh, |
78559 | 170 |
build_options = List(options.spec("build_database_server")), |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
171 |
build_id = build_context.build_uuid, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
172 |
isabelle_home = remote_isabelle_home, |
78580 | 173 |
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
|
174 |
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
|
175 |
quiet = true) |
78584
92ef737f412c
removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);
wenzelm
parents:
78582
diff
changeset
|
176 |
remote_isabelle.bash(script).check |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
177 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
178 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
179 |
override def close(): Unit = ssh.close() |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
180 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
181 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
182 |
class Result(val host: Host, val process_result: Exn.Result[Process_Result]) { |
78443 | 183 |
def rc: Int = Process_Result.RC(process_result) |
184 |
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
|
185 |
} |
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
|
186 |
|
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
|
187 |
|
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
|
188 |
/* 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
|
189 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
190 |
object none extends Build_Cluster { |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
191 |
override def toString: String = "Build_Cluster.none" |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
192 |
} |
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
|
193 |
|
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
|
194 |
def make(build_context: Build.Context, progress: Progress = new Progress): Build_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
|
195 |
val remote_hosts = build_context.build_hosts.filterNot(_.is_local) |
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
|
196 |
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
|
197 |
else new Remote_Build_Cluster(build_context, remote_hosts, progress = progress) |
78413 | 198 |
} |
78398 | 199 |
} |
78413 | 200 |
|
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
|
201 |
// 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
|
202 |
trait Build_Cluster extends AutoCloseable { |
78443 | 203 |
def rc: Int = Process_Result.RC.ok |
204 |
def ok: Boolean = rc == Process_Result.RC.ok |
|
205 |
def return_code(rc: Int): Unit = () |
|
206 |
def return_code(res: Process_Result): Unit = return_code(res.rc) |
|
207 |
def return_code(exn: Throwable): Unit = return_code(Process_Result.RC(exn)) |
|
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
|
208 |
def open(): 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
|
209 |
def init(): 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
|
210 |
def start(): 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
|
211 |
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
|
212 |
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
|
213 |
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
|
214 |
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
|
215 |
} |
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
|
216 |
|
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
|
217 |
class Remote_Build_Cluster( |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
218 |
val build_context: Build.Context, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
219 |
val remote_hosts: List[Build_Cluster.Host], |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
220 |
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
|
221 |
) extends Build_Cluster { |
78424 | 222 |
require(remote_hosts.nonEmpty && !remote_hosts.exists(_.is_local), "remote hosts required") |
78413 | 223 |
|
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
|
224 |
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
|
225 |
remote_hosts.iterator.map(_.name).mkString("Build_Cluster(", ", ", ")") |
78413 | 226 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
227 |
|
78443 | 228 |
/* cumulative return code */ |
229 |
||
78581 | 230 |
private val _rc = Synchronized(Process_Result.RC.ok) |
78443 | 231 |
|
78581 | 232 |
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
|
233 |
|
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
|
234 |
override def return_code(rc: Int): Unit = |
78581 | 235 |
_rc.change(rc0 => Process_Result.RC.merge(rc0, rc)) |
78443 | 236 |
|
237 |
def capture[A](host: Build_Cluster.Host, op: String)( |
|
238 |
e: => A, |
|
239 |
msg: String = host.message(op + " ..."), |
|
78506 | 240 |
err: Throwable => String = { exn => |
241 |
return_code(exn) |
|
242 |
host.message("failed to " + op + "\n" + Exn.print(exn)) |
|
243 |
} |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
244 |
): Exn.Result[A] = { |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
245 |
progress.capture(e, msg = msg, err = err) |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
246 |
} |
78443 | 247 |
|
248 |
||
249 |
/* open remote sessions */ |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
250 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
251 |
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
|
252 |
|
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
|
253 |
override def open(): Unit = synchronized { |
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
|
254 |
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
|
255 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
256 |
val attempts = |
78433 | 257 |
Par_List.map((host: Build_Cluster.Host) => |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
258 |
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
|
259 |
remote_hosts, thread = true) |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
260 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
261 |
if (attempts.forall(Exn.the_res.isDefinedAt)) { |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
262 |
_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
|
263 |
_sessions |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
264 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
265 |
else { |
78592 | 266 |
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
|
267 |
error("Failed to connect build cluster") |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
268 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
269 |
} |
78413 | 270 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
271 |
|
78443 | 272 |
/* init remote Isabelle distributions */ |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
273 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
274 |
private var _init = List.empty[Future[Unit]] |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
275 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
276 |
override def init(): Unit = synchronized { |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
277 |
require(_sessions.nonEmpty, "build cluster not yet open") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
278 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
279 |
if (_init.isEmpty) { |
78443 | 280 |
_init = |
78567 | 281 |
for (session <- _sessions if !session.host.shared) yield { |
78443 | 282 |
Future.thread(session.host.message("session")) { |
283 |
capture(session.host, "sync") { session.sync() } |
|
284 |
capture(session.host, "init") { session.init() } |
|
285 |
} |
|
286 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
287 |
} |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
288 |
} |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
289 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
290 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
291 |
/* workers */ |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
292 |
|
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
|
293 |
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
|
294 |
|
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
|
295 |
override def active(): Boolean = synchronized { _workers.nonEmpty } |
78413 | 296 |
|
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 |
override def start(): Unit = synchronized { |
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
|
298 |
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
|
299 |
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
|
300 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
301 |
init() |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
302 |
_init.foreach(_.join) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
303 |
|
78443 | 304 |
_workers = |
305 |
for (session <- _sessions) yield { |
|
78582 | 306 |
Future.thread(session.host.message("work")) { |
307 |
Exn.release(capture(session.host, "work") { session.start() }) |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
308 |
} |
78443 | 309 |
} |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
310 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
311 |
|
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
|
312 |
override def join: List[Build_Cluster.Result] = synchronized { |
78443 | 313 |
_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
|
314 |
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
|
315 |
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
|
316 |
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
|
317 |
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
|
318 |
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
|
319 |
} |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
320 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
321 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
322 |
|
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
|
323 |
/* close */ |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
324 |
|
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
|
325 |
override def close(): Unit = synchronized { |
78441 | 326 |
_init.foreach(_.join) |
78639
ca56952b7322
proper stop of build_process shutdown, despite errors on workers;
wenzelm
parents:
78638
diff
changeset
|
327 |
_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
|
328 |
_sessions.foreach(_.close()) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
329 |
|
78443 | 330 |
_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
|
331 |
_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
|
332 |
_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
|
333 |
} |
78413 | 334 |
} |