src/Pure/Tools/build_cluster.scala
author wenzelm
Tue, 22 Aug 2023 09:39:37 +0200
changeset 78559 020fecb4da0c
parent 78558 ca0fe2802123
child 78560 39f6f180008d
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78398
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_cluster.scala
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
     3
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
     4
Management of build cluster: independent ssh hosts with access to shared
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
     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
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
    10
*/
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
    11
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
    12
package isabelle
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
    13
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
    14
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
    15
object Build_Cluster {
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
    16
  /* host specifications */
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
    17
78399
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
    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
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
    37
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
    38
    def apply(
78416
f26eba6281b1 tuned signature;
wenzelm
parents: 78413
diff changeset
    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
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
    44
      options: List[Options.Spec] = Nil
78416
f26eba6281b1 tuned signature;
wenzelm
parents: 78413
diff changeset
    45
    ): Host = new Host(name, user, port, jobs, numa, options)
78401
822ddccda899 proforma support for remote build hosts;
wenzelm
parents: 78399
diff changeset
    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
f26eba6281b1 tuned signature;
wenzelm
parents: 78413
diff changeset
    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
f26eba6281b1 tuned signature;
wenzelm
parents: 78413
diff changeset
    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
645b54f3244a tuned output;
wenzelm
parents: 78421
diff changeset
    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
f26eba6281b1 tuned signature;
wenzelm
parents: 78413
diff changeset
    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
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    74
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    75
    def print_name(s: String): String =
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    76
      Token.quote_name(Options.specs_syntax.keywords, s)
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    77
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    78
    def print_option(spec: Options.Spec): String = {
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    79
      def print_value =
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    80
        spec.value.get match {
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    81
          case s@Value.Boolean(_) => s
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    82
          case s@Value.Long(_) => s
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    83
          case s@Value.Double(_) => s
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    84
          case s => print_name(s)
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    85
        }
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    86
      spec.name + if_proper(spec.value, "=" + print_value)
0be7e94fd243 more accurate print vs. parse;
wenzelm
parents: 78425
diff changeset
    87
    }
78399
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
    88
  }
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
    89
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
    90
  class Host(
78427
5b7d1cb073db tuned signature;
wenzelm
parents: 78426
diff changeset
    91
    val name: String,
5b7d1cb073db tuned signature;
wenzelm
parents: 78426
diff changeset
    92
    val user: String,
5b7d1cb073db tuned signature;
wenzelm
parents: 78426
diff changeset
    93
    val port: Int,
5b7d1cb073db tuned signature;
wenzelm
parents: 78426
diff changeset
    94
    val jobs: Int,
5b7d1cb073db tuned signature;
wenzelm
parents: 78426
diff changeset
    95
    val numa: Boolean,
5b7d1cb073db tuned signature;
wenzelm
parents: 78426
diff changeset
    96
    val options: List[Options.Spec]
78399
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
    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
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   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
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
   103
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
   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
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
   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
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
   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
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
   115
    }
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
   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)
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   118
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   119
    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
   120
      val session_options = build_context.build_options ++ host.options
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   121
      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
   122
      new Session(build_context, host, session_options, ssh, progress)
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   123
    }
78399
facf1a324807 more operations;
wenzelm
parents: 78398
diff changeset
   124
  }
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   125
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   126
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   127
  /* SSH sessions */
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   128
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   129
  class Session(
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   130
    val build_context: Build.Context,
78433
872f10c80810 tuned signature;
wenzelm
parents: 78430
diff changeset
   131
    val host: Host,
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   132
    val options: Options,
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   133
    val ssh: SSH.System,
78433
872f10c80810 tuned signature;
wenzelm
parents: 78430
diff changeset
   134
    val progress: Progress
872f10c80810 tuned signature;
wenzelm
parents: 78430
diff changeset
   135
  ) extends AutoCloseable {
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   136
    override def toString: String = ssh.toString
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   137
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   138
    val remote_identifier: String = options.string("build_cluster_identifier")
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   139
    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
   140
    val remote_isabelle_home: Path = remote_root + Path.explode("isabelle")
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   141
    val remote_afp_root: Option[Path] =
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   142
      if (build_context.afp_root.isEmpty) None
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   143
      else Some(remote_isabelle_home + Path.explode("AFP"))
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   144
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   145
    lazy val remote_isabelle: Other_Isabelle =
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   146
      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
   147
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   148
    def sync(): Other_Isabelle = {
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   149
      Sync.sync(options, Rsync.Context(ssh = ssh), remote_isabelle_home,
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   150
        afp_root = build_context.afp_root,
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   151
        purge_heaps = true,
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   152
        preserve_jars = true)
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   153
      remote_isabelle
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   154
    }
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   155
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   156
    def init(): Unit = remote_isabelle.init()
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   157
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
   158
    def start(): Process_Result = {
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   159
      val script =
78558
ca0fe2802123 tuned signature;
wenzelm
parents: 78556
diff changeset
   160
        Build.build_worker_command(host,
78556
20360824863a more robust command options;
wenzelm
parents: 78508
diff changeset
   161
          ssh = ssh,
78559
020fecb4da0c tuned signature;
wenzelm
parents: 78558
diff changeset
   162
          build_options = List(options.spec("build_database_server")),
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   163
          build_id = build_context.build_uuid,
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   164
          isabelle_home = remote_isabelle_home,
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   165
          afp_root = remote_afp_root)
78505
8cd399b25dac more robust;
wenzelm
parents: 78499
diff changeset
   166
      remote_isabelle.bash(script).print.check
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   167
    }
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   168
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   169
    override def close(): Unit = ssh.close()
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   170
  }
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   171
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   172
  class Result(val host: Host, val process_result: Exn.Result[Process_Result]) {
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   173
    def rc: Int = Process_Result.RC(process_result)
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   174
    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
   175
  }
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
   176
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
  /* 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
   179
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   180
  object none extends Build_Cluster {
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   181
    override def toString: String = "Build_Cluster.none"
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   182
  }
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
   183
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
   184
  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
   185
    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
   186
    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
   187
    else new Remote_Build_Cluster(build_context, remote_hosts, progress = progress)
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   188
  }
78398
ea5adf7acc2d support for management of build cluster;
wenzelm
parents:
diff changeset
   189
}
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   190
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
   191
// 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
   192
trait Build_Cluster extends AutoCloseable {
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   193
  def rc: Int = Process_Result.RC.ok
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   194
  def ok: Boolean = rc == Process_Result.RC.ok
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   195
  def return_code(rc: Int): Unit = ()
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   196
  def return_code(res: Process_Result): Unit = return_code(res.rc)
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   197
  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
   198
  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
   199
  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
   200
  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
   201
  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
   202
  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
   203
  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
   204
  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
   205
}
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
   206
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
   207
class Remote_Build_Cluster(
78436
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   208
  val build_context: Build.Context,
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   209
  val remote_hosts: List[Build_Cluster.Host],
5f5f909206bb clarified signature: more "object-oriented" style;
wenzelm
parents: 78434
diff changeset
   210
  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
   211
) extends Build_Cluster {
78424
e5908be41a36 clarified signature (again);
wenzelm
parents: 78423
diff changeset
   212
  require(remote_hosts.nonEmpty && !remote_hosts.exists(_.is_local), "remote hosts required")
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   213
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
   214
  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
   215
    remote_hosts.iterator.map(_.name).mkString("Build_Cluster(", ", ", ")")
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   216
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   217
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   218
  /* cumulative return code */
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   219
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   220
  private var _rc: Int = Process_Result.RC.ok
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   221
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
   222
  override def rc: Int = _rc.synchronized { _rc }
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
   223
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
   224
  override def return_code(rc: Int): Unit =
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
   225
    _rc.synchronized { _rc = Process_Result.RC.merge(_rc, rc) }
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   226
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   227
  def capture[A](host: Build_Cluster.Host, op: String)(
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   228
    e: => A,
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   229
    msg: String = host.message(op + " ..."),
78506
14da1177d1c3 more informative error;
wenzelm
parents: 78505
diff changeset
   230
    err: Throwable => String = { exn =>
14da1177d1c3 more informative error;
wenzelm
parents: 78505
diff changeset
   231
      return_code(exn)
14da1177d1c3 more informative error;
wenzelm
parents: 78505
diff changeset
   232
      host.message("failed to " + op + "\n" + Exn.print(exn))
14da1177d1c3 more informative error;
wenzelm
parents: 78505
diff changeset
   233
    }
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   234
  ): Exn.Result[A] = {
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   235
    progress.capture(e, msg = msg, err = err)
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   236
  }
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   237
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   238
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   239
  /* open remote sessions */
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   240
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   241
  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
   242
78434
b4ec7ea073da clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents: 78433
diff changeset
   243
  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
   244
    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
   245
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   246
    val attempts =
78433
872f10c80810 tuned signature;
wenzelm
parents: 78430
diff changeset
   247
      Par_List.map((host: Build_Cluster.Host) =>
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   248
        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
   249
        remote_hosts, thread = true)
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
    if (attempts.forall(Exn.the_res.isDefinedAt)) {
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   252
      _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
   253
      _sessions
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   254
    }
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   255
    else {
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   256
      for (Exn.Res(session) <- attempts) session.close()
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   257
      error("Failed to connect build cluster")
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   258
    }
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   259
  }
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   260
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   261
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   262
  /* init remote Isabelle distributions */
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   263
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   264
  private var _init = List.empty[Future[Unit]]
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
  override def init(): Unit = synchronized {
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   267
    require(_sessions.nonEmpty, "build cluster not yet open")
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   268
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   269
    if (_init.isEmpty) {
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   270
      _init =
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   271
        for (session <- _sessions) yield {
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   272
          Future.thread(session.host.message("session")) {
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   273
            capture(session.host, "sync") { session.sync() }
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   274
            capture(session.host, "init") { session.init() }
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   275
          }
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   276
        }
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   277
    }
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
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   280
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   281
  /* workers */
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   282
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
   283
  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
   284
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
   285
  override def active(): Boolean = synchronized { _workers.nonEmpty }
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
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 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
   288
    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
   289
    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
   290
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   291
    init()
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   292
    _init.foreach(_.join)
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   293
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   294
    _workers =
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   295
      for (session <- _sessions) yield {
78444
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   296
        Future.thread(session.host.message("start")) {
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   297
          Exn.release(capture(session.host, "start") { session.start() })
3d1746a716fa clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents: 78443
diff changeset
   298
        }
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   299
      }
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   300
  }
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   301
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
   302
  override def join: List[Build_Cluster.Result] = synchronized {
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   303
    _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
   304
    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
   305
    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
   306
      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
   307
      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
   308
        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
   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
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   312
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
   313
  /* close */
78430
0461fc9d43e8 more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents: 78427
diff changeset
   314
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
   315
  override def close(): Unit = synchronized {
78441
3153311f0f6c more robust;
wenzelm
parents: 78440
diff changeset
   316
    _init.foreach(_.join)
3153311f0f6c more robust;
wenzelm
parents: 78440
diff changeset
   317
    _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
   318
    _sessions.foreach(_.close())
78440
126a12483c67 support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents: 78436
diff changeset
   319
78443
a8e1d9202dd9 clarified exception handling and return_code;
wenzelm
parents: 78441
diff changeset
   320
    _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
   321
    _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
   322
    _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
   323
  }
78413
6f3066a9b609 more pro-forma support for Build_Cluster;
wenzelm
parents: 78408
diff changeset
   324
}