author | wenzelm |
Sun, 23 Jul 2023 19:21:54 +0200 | |
changeset 78443 | a8e1d9202dd9 |
parent 78441 | 3153311f0f6c |
child 78444 | 3d1746a716fa |
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" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
25 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
26 |
val parameters: Options = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
27 |
Options.inline(""" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
28 |
option user : string = "" -- "explicit SSH user" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
29 |
option port : int = 0 -- "explicit SSH port" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
30 |
option jobs : int = 1 -- "maximum number of parallel jobs" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
31 |
option numa : bool = false -- "cyclic shuffling of NUMA CPU nodes" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
32 |
""") |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
33 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
34 |
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
|
35 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
36 |
lazy val test_options: Options = Options.init0() |
78399 | 37 |
|
38 |
def apply( |
|
78416 | 39 |
name: String = "", |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
40 |
user: String = parameters.string(USER), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
41 |
port: Int = parameters.int(PORT), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
42 |
jobs: Int = parameters.int(JOBS), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
43 |
numa: Boolean = parameters.bool(NUMA), |
78399 | 44 |
options: List[Options.Spec] = Nil |
78416 | 45 |
): Host = new Host(name, user, port, jobs, numa, options) |
78401 | 46 |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
47 |
def parse(str: String): Host = { |
78416 | 48 |
val name = str.takeWhile(c => !rfc822_specials.contains(c)) |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
49 |
val (params, options) = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
50 |
try { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
51 |
val rest = { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
52 |
val n = str.length |
78416 | 53 |
val m = name.length |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
54 |
val l = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
55 |
if (m == n) n |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
56 |
else if (str(m) == ':') m + 1 |
78423 | 57 |
else error("Missing \":\" after host name") |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
58 |
str.substring(l) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
59 |
} |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
60 |
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
|
61 |
(parameters ++ specs1, { test_options ++ specs2; specs2 }) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
62 |
} |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
63 |
catch { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
64 |
case ERROR(msg) => |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
65 |
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
|
66 |
} |
78416 | 67 |
apply(name = name, |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
68 |
user = params.string(USER), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
69 |
port = params.int(PORT), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
70 |
jobs = params.int(JOBS), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
71 |
numa = params.bool(NUMA), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
72 |
options = options) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
73 |
} |
78426 | 74 |
|
75 |
def print_name(s: String): String = |
|
76 |
Token.quote_name(Options.specs_syntax.keywords, s) |
|
77 |
||
78 |
def print_option(spec: Options.Spec): String = { |
|
79 |
def print_value = |
|
80 |
spec.value.get match { |
|
81 |
case s@Value.Boolean(_) => s |
|
82 |
case s@Value.Long(_) => s |
|
83 |
case s@Value.Double(_) => s |
|
84 |
case s => print_name(s) |
|
85 |
} |
|
86 |
spec.name + if_proper(spec.value, "=" + print_value) |
|
87 |
} |
|
78399 | 88 |
} |
89 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
90 |
class Host( |
78427 | 91 |
val name: String, |
92 |
val user: String, |
|
93 |
val port: Int, |
|
94 |
val jobs: Int, |
|
95 |
val numa: Boolean, |
|
96 |
val options: List[Options.Spec] |
|
78399 | 97 |
) { |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
98 |
host => |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
99 |
|
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
100 |
def is_local: Boolean = SSH.is_local(host.name) |
78413 | 101 |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
102 |
override def toString: String = print |
78399 | 103 |
|
104 |
def print: String = { |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
105 |
val params = |
78399 | 106 |
List( |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
107 |
if (host.user.isEmpty) "" else Properties.Eq(Host.USER, Host.print_name(host.user)), |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
108 |
if (host.port == 0) "" else Properties.Eq(Host.PORT, host.port.toString), |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
109 |
if (host.jobs == 1) "" else Properties.Eq(Host.JOBS, host.jobs.toString), |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
110 |
if_proper(host.numa, Host.NUMA) |
78399 | 111 |
).filter(_.nonEmpty) |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
112 |
val rest = (params ::: host.options.map(Host.print_option)).mkString(",") |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
113 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
114 |
SSH.print_local(host.name) + if_proper(rest, ":" + rest) |
78399 | 115 |
} |
116 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
117 |
def message(msg: String): String = "Host " + quote(host.name) + if_proper(msg, ": " + msg) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
118 |
def err_message(msg: String)(exn: Throwable): String = message(msg + "\n" + Exn.message(exn)) |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
119 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
120 |
def open_session( |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
121 |
options: Options, |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
122 |
afp_root: Option[Path] = None, |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
123 |
progress: Progress = new Progress |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
124 |
): Session = { |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
125 |
val session_options = options ++ host.options |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
126 |
val ssh = SSH.open_session(session_options, host.name, port = host.port, user = host.user) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
127 |
new Session(host, session_options, afp_root, ssh, progress) |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
128 |
} |
78399 | 129 |
} |
78413 | 130 |
|
131 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
132 |
/* SSH sessions */ |
78413 | 133 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
134 |
class Session( |
78433 | 135 |
val host: Host, |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
136 |
val options: Options, |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
137 |
val afp_root: Option[Path], |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
138 |
val ssh: SSH.System, |
78433 | 139 |
val progress: Progress |
140 |
) extends AutoCloseable { |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
141 |
override def toString: String = ssh.toString |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
142 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
143 |
val remote_identifier: String = options.string("build_cluster_identifier") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
144 |
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
|
145 |
val remote_isabelle_home: Path = remote_root + Path.explode("isabelle") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
146 |
val remote_afp: Path = remote_isabelle_home + Path.explode("AFP") |
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, |
|
153 |
afp_root = afp_root, purge_heaps = true, preserve_jars = true) |
|
154 |
remote_isabelle |
|
155 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
156 |
|
78443 | 157 |
def init(): Unit = remote_isabelle.init() |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
158 |
|
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
|
159 |
def start(): 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
|
160 |
Process_Result.ok // FIXME |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
161 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
162 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
163 |
override def close(): Unit = ssh.close() |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
164 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
165 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
166 |
class Result(val host: Host, val process_result: Exn.Result[Process_Result]) { |
78443 | 167 |
def rc: Int = Process_Result.RC(process_result) |
168 |
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
|
169 |
} |
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
|
170 |
|
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
|
171 |
|
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
|
172 |
/* 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
|
173 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
174 |
object none extends Build_Cluster { |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
175 |
override def toString: String = "Build_Cluster.none" |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
176 |
} |
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
|
177 |
|
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
else new Remote_Build_Cluster(build_context, remote_hosts, progress = progress) |
78413 | 182 |
} |
78398 | 183 |
} |
78413 | 184 |
|
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 |
// 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
|
186 |
trait Build_Cluster extends AutoCloseable { |
78443 | 187 |
def rc: Int = Process_Result.RC.ok |
188 |
def ok: Boolean = rc == Process_Result.RC.ok |
|
189 |
def return_code(rc: Int): Unit = () |
|
190 |
def return_code(res: Process_Result): Unit = return_code(res.rc) |
|
191 |
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
|
192 |
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
|
193 |
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
|
194 |
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
|
195 |
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
|
196 |
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
|
197 |
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
|
198 |
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
|
199 |
} |
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
|
200 |
|
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 |
class Remote_Build_Cluster( |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
202 |
val build_context: Build.Context, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
203 |
val remote_hosts: List[Build_Cluster.Host], |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
204 |
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
|
205 |
) extends Build_Cluster { |
78424 | 206 |
require(remote_hosts.nonEmpty && !remote_hosts.exists(_.is_local), "remote hosts required") |
78413 | 207 |
|
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 |
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
|
209 |
remote_hosts.iterator.map(_.name).mkString("Build_Cluster(", ", ", ")") |
78413 | 210 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
211 |
|
78443 | 212 |
/* cumulative return code */ |
213 |
||
214 |
private var _rc: Int = Process_Result.RC.ok |
|
215 |
||
216 |
override def rc: Int = synchronized { _rc } |
|
217 |
override def return_code(rc: Int): Unit = synchronized { _rc = Process_Result.RC.merge(_rc, rc) } |
|
218 |
||
219 |
def capture[A](host: Build_Cluster.Host, op: String)( |
|
220 |
e: => A, |
|
221 |
msg: String = host.message(op + " ..."), |
|
222 |
err: Throwable => String = { exn => return_code(exn); host.message("failed to " + op) } |
|
223 |
): Exn.Result[A] = progress.capture(e, msg = msg, err = err) |
|
224 |
||
225 |
||
226 |
/* open remote sessions */ |
|
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 |
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
|
229 |
|
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
|
230 |
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
|
231 |
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
|
232 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
233 |
val attempts = |
78433 | 234 |
Par_List.map((host: Build_Cluster.Host) => |
78443 | 235 |
capture(host, "open") { host.open_session(build_context.build_options, progress = progress) }, |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
236 |
remote_hosts, thread = true) |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
237 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
238 |
if (attempts.forall(Exn.the_res.isDefinedAt)) { |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
239 |
_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
|
240 |
_sessions |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
241 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
242 |
else { |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
243 |
for (Exn.Res(session) <- attempts) session.close() |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
244 |
error("Failed to connect build cluster") |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
245 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
246 |
} |
78413 | 247 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
248 |
|
78443 | 249 |
/* init remote Isabelle distributions */ |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
250 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
251 |
private var _init = List.empty[Future[Unit]] |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
252 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
253 |
override def init(): Unit = synchronized { |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
254 |
require(_sessions.nonEmpty, "build cluster not yet open") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
255 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
256 |
if (_init.isEmpty) { |
78443 | 257 |
_init = |
258 |
for (session <- _sessions) yield { |
|
259 |
Future.thread(session.host.message("session")) { |
|
260 |
capture(session.host, "sync") { session.sync() } |
|
261 |
capture(session.host, "init") { session.init() } |
|
262 |
} |
|
263 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
264 |
} |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
265 |
} |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
266 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
267 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
268 |
/* workers */ |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
269 |
|
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
|
270 |
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
|
271 |
|
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 |
override def active(): Boolean = synchronized { _workers.nonEmpty } |
78413 | 273 |
|
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
|
274 |
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
|
275 |
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
|
276 |
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
|
277 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
278 |
init() |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
279 |
_init.foreach(_.join) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
280 |
|
78443 | 281 |
_workers = |
282 |
for (session <- _sessions) yield { |
|
283 |
Future.thread(session.host.message("worker")) { session.start() } |
|
284 |
} |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
285 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
286 |
|
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
|
287 |
override def join: List[Build_Cluster.Result] = synchronized { |
78443 | 288 |
_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
|
289 |
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
|
290 |
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
|
291 |
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
|
292 |
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
|
293 |
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
|
294 |
} |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
295 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
296 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
297 |
|
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
|
298 |
/* close */ |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
299 |
|
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
|
300 |
override def close(): Unit = synchronized { |
78441 | 301 |
_init.foreach(_.join) |
302 |
_workers.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
|
303 |
_sessions.foreach(_.close()) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
304 |
|
78443 | 305 |
_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
|
306 |
_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
|
307 |
_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
|
308 |
} |
78413 | 309 |
} |