src/Pure/Tools/build_process.scala
author wenzelm
Mon, 13 Mar 2023 17:22:43 +0100
changeset 77630 86ef80d13544
parent 77629 979baa91da0f
child 77631 89fffc5f5728
permissions -rw-r--r--
clarified signature: avoid confusion due to object-orientation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_process.scala
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     3
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     4
Build process for sessions, with build database, optional heap, and
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     5
optional presentation.
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     6
*/
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     7
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     8
package isabelle
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
     9
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    10
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
    11
import scala.collection.immutable.SortedMap
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    12
import scala.math.Ordering
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
    13
import scala.annotation.tailrec
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    14
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    15
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    16
object Build_Process {
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
    17
  /** static context **/
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    18
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    19
  object Context {
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    20
    def apply(
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    21
      store: Sessions.Store,
77453
e72b1f5fd88d tuned signature;
wenzelm
parents: 77452
diff changeset
    22
      build_deps: Sessions.Deps,
77315
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
    23
      progress: Progress = new Progress,
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
    24
      ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
77378
f047804f4860 clarified Build_Process.Context: cover all static information;
wenzelm
parents: 77375
diff changeset
    25
      hostname: String = Isabelle_System.hostname(),
f047804f4860 clarified Build_Process.Context: cover all static information;
wenzelm
parents: 77375
diff changeset
    26
      numa_shuffling: Boolean = false,
77315
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
    27
      build_heap: Boolean = false,
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
    28
      max_jobs: Int = 1,
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
    29
      fresh_build: Boolean = false,
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
    30
      no_build: Boolean = false,
77378
f047804f4860 clarified Build_Process.Context: cover all static information;
wenzelm
parents: 77375
diff changeset
    31
      session_setup: (String, Session) => Unit = (_, _) => (),
77579
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
    32
      build_uuid: String = UUID.random().toString,
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
    33
      master: Boolean = false,
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    34
    ): Context = {
77453
e72b1f5fd88d tuned signature;
wenzelm
parents: 77452
diff changeset
    35
      val sessions_structure = build_deps.sessions_structure
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    36
      val build_graph = sessions_structure.build_graph
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    37
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    38
      val sessions =
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    39
        Map.from(
77448
wenzelm
parents: 77447
diff changeset
    40
          for ((name, (info, _)) <- build_graph.iterator)
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    41
          yield {
77447
566e6e393126 proper deps from build_graph, not imports_graph (amending 0c704aba71e3);
wenzelm
parents: 77446
diff changeset
    42
            val deps = info.parent.toList
566e6e393126 proper deps from build_graph, not imports_graph (amending 0c704aba71e3);
wenzelm
parents: 77446
diff changeset
    43
            val ancestors = sessions_structure.build_requirements(deps)
77458
403748b23f13 clarified signature: prefer static data;
wenzelm
parents: 77457
diff changeset
    44
            val sources_shasum = build_deps.sources_shasum(name)
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77443
diff changeset
    45
            val session_context =
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77443
diff changeset
    46
              Build_Job.Session_Context.load(
77610
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
    47
                build_uuid, name, deps, ancestors, info.session_prefs, sources_shasum,
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
    48
                info.timeout, store, progress = progress)
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77443
diff changeset
    49
            name -> session_context
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    50
          })
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    51
77248
wenzelm
parents: 77247
diff changeset
    52
      val sessions_time = {
wenzelm
parents: 77247
diff changeset
    53
        val maximals = build_graph.maximals.toSet
wenzelm
parents: 77247
diff changeset
    54
        def descendants_time(name: String): Double = {
wenzelm
parents: 77247
diff changeset
    55
          if (maximals.contains(name)) sessions(name).old_time.seconds
wenzelm
parents: 77247
diff changeset
    56
          else {
wenzelm
parents: 77247
diff changeset
    57
            val descendants = build_graph.all_succs(List(name)).toSet
wenzelm
parents: 77247
diff changeset
    58
            val g = build_graph.restrict(descendants)
wenzelm
parents: 77247
diff changeset
    59
            (0.0 :: g.maximals.flatMap { desc =>
wenzelm
parents: 77247
diff changeset
    60
              val ps = g.all_preds(List(desc))
wenzelm
parents: 77247
diff changeset
    61
              if (ps.exists(p => !sessions.isDefinedAt(p))) None
wenzelm
parents: 77247
diff changeset
    62
              else Some(ps.map(p => sessions(p).old_time.seconds).sum)
wenzelm
parents: 77247
diff changeset
    63
            }).max
wenzelm
parents: 77247
diff changeset
    64
          }
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    65
        }
77248
wenzelm
parents: 77247
diff changeset
    66
        Map.from(
wenzelm
parents: 77247
diff changeset
    67
          for (name <- sessions.keysIterator)
wenzelm
parents: 77247
diff changeset
    68
          yield name -> descendants_time(name)).withDefaultValue(0.0)
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    69
      }
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    70
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    71
      val ordering =
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    72
        new Ordering[String] {
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    73
          def compare(name1: String, name2: String): Int =
77248
wenzelm
parents: 77247
diff changeset
    74
            sessions_time(name2) compare sessions_time(name1) match {
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    75
              case 0 =>
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    76
                sessions(name2).timeout compare sessions(name1).timeout match {
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    77
                  case 0 => name1 compare name2
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    78
                  case ord => ord
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    79
                }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    80
              case ord => ord
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    81
            }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    82
        }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    83
77477
f376aebca9c1 clarified modules;
wenzelm
parents: 77476
diff changeset
    84
      val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
    85
      new Context(store, build_deps, sessions, ordering, ml_platform, hostname, numa_nodes,
77317
b8ec3c0455db clarified modules: NUMA is managed by Build_Process;
wenzelm
parents: 77315
diff changeset
    86
        build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
77579
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
    87
        no_build = no_build, session_setup, build_uuid = build_uuid, master = master)
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    88
    }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    89
  }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    90
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    91
  final class Context private(
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
    92
    val store: Sessions.Store,
77453
e72b1f5fd88d tuned signature;
wenzelm
parents: 77452
diff changeset
    93
    val build_deps: Sessions.Deps,
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
    94
    val sessions: State.Sessions,
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
    95
    val ordering: Ordering[String],
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
    96
    val ml_platform: String,
77378
f047804f4860 clarified Build_Process.Context: cover all static information;
wenzelm
parents: 77375
diff changeset
    97
    val hostname: String,
77317
b8ec3c0455db clarified modules: NUMA is managed by Build_Process;
wenzelm
parents: 77315
diff changeset
    98
    val numa_nodes: List[Int],
77315
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
    99
    val build_heap: Boolean,
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
   100
    val max_jobs: Int,
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
   101
    val fresh_build: Boolean,
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
   102
    val no_build: Boolean,
77378
f047804f4860 clarified Build_Process.Context: cover all static information;
wenzelm
parents: 77375
diff changeset
   103
    val session_setup: (String, Session) => Unit,
77579
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
   104
    val build_uuid: String,
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
   105
    val master: Boolean
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   106
  ) {
77561
a24d77f2cfe9 tuned output;
wenzelm
parents: 77552
diff changeset
   107
    override def toString: String =
a24d77f2cfe9 tuned output;
wenzelm
parents: 77552
diff changeset
   108
      "Build_Process.Context(build_uuid = " + quote(build_uuid) + ")"
a24d77f2cfe9 tuned output;
wenzelm
parents: 77552
diff changeset
   109
77470
38503d9ff2e5 clarified modules;
wenzelm
parents: 77469
diff changeset
   110
    def build_options: Options = store.options
38503d9ff2e5 clarified modules;
wenzelm
parents: 77469
diff changeset
   111
77453
e72b1f5fd88d tuned signature;
wenzelm
parents: 77452
diff changeset
   112
    def sessions_structure: Sessions.Structure = build_deps.sessions_structure
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   113
77462
b474d39ddfee tuned signature;
wenzelm
parents: 77461
diff changeset
   114
    def sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum
77458
403748b23f13 clarified signature: prefer static data;
wenzelm
parents: 77457
diff changeset
   115
77462
b474d39ddfee tuned signature;
wenzelm
parents: 77461
diff changeset
   116
    def old_command_timings(name: String): List[Properties.T] =
b474d39ddfee tuned signature;
wenzelm
parents: 77461
diff changeset
   117
      sessions.get(name) match {
77444
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77443
diff changeset
   118
        case Some(session_context) =>
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77443
diff changeset
   119
          Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache)
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77443
diff changeset
   120
        case None => Nil
0c704aba71e3 clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents: 77443
diff changeset
   121
      }
77439
d6bf9ec39d12 avoid premature Properties.uncompress: allow blob to be stored in another database;
wenzelm
parents: 77438
diff changeset
   122
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   123
    def prepare_database(): Unit = {
77629
979baa91da0f clarified modules;
wenzelm
parents: 77610
diff changeset
   124
      using_option(store.open_build_database()) { db =>
77539
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   125
        db.transaction {
77596
dd8b08729458 clarified signature;
wenzelm
parents: 77594
diff changeset
   126
          Data.all_tables.create_lock(db)
77539
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   127
          Data.clean_build(db)
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   128
        }
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   129
        db.rebuild()
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   130
      }
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   131
    }
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   132
77463
4e8bec105ce5 tuned signature;
wenzelm
parents: 77462
diff changeset
   133
    def store_heap(name: String): Boolean =
77462
b474d39ddfee tuned signature;
wenzelm
parents: 77461
diff changeset
   134
      build_heap || Sessions.is_pure(name) ||
b474d39ddfee tuned signature;
wenzelm
parents: 77461
diff changeset
   135
      sessions.valuesIterator.exists(_.ancestors.contains(name))
77578
149d48a4801b support for "isabelle build -j0": require external workers to make progress;
wenzelm
parents: 77561
diff changeset
   136
77594
7723cf88658f proper test (amending 32f9e75c92e9);
wenzelm
parents: 77590
diff changeset
   137
    def worker_active: Boolean = max_jobs > 0
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   138
  }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   139
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   140
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   141
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   142
  /** dynamic state **/
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   143
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   144
  type Progress_Messages = SortedMap[Long, Progress.Message]
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   145
77585
89c42ec77a84 tuned signature;
wenzelm
parents: 77584
diff changeset
   146
  case class Task(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) {
77313
f8aa1647d156 more elementary data structures, to fit better to SQL database;
wenzelm
parents: 77312
diff changeset
   147
    def is_ready: Boolean = deps.isEmpty
77585
89c42ec77a84 tuned signature;
wenzelm
parents: 77584
diff changeset
   148
    def resolve(dep: String): Task =
77313
f8aa1647d156 more elementary data structures, to fit better to SQL database;
wenzelm
parents: 77312
diff changeset
   149
      if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this
f8aa1647d156 more elementary data structures, to fit better to SQL database;
wenzelm
parents: 77312
diff changeset
   150
  }
f8aa1647d156 more elementary data structures, to fit better to SQL database;
wenzelm
parents: 77312
diff changeset
   151
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   152
  case class Job(
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   153
    name: String,
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   154
    worker_uuid: String,
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   155
    node_info: Host.Node_Info,
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   156
    build: Option[Build_Job]
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   157
  ) {
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   158
    def no_build: Job = copy(build = None)
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   159
  }
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   160
77583
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   161
  case class Worker(
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   162
    worker_uuid: String,
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   163
    build_uuid: String,
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   164
    hostname: String,
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   165
    java_pid: Long,
77588
066d5df144f0 assume total operation: ProcessHandle.current().info.startInstant appears to work on all platforms;
wenzelm
parents: 77587
diff changeset
   166
    java_start: Date,
77583
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   167
    start: Date,
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   168
    stamp: Date,
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   169
    stop: Option[Date],
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   170
    serial: Long)
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   171
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   172
  case class Result(
77461
a553e419e9dc tuned signature;
wenzelm
parents: 77460
diff changeset
   173
    process_result: Process_Result,
77460
ccca589d7027 tuned signature: support general Build_Job instances;
wenzelm
parents: 77459
diff changeset
   174
    output_shasum: SHA1.Shasum,
77475
3bc611c80346 clarified modules;
wenzelm
parents: 77474
diff changeset
   175
    node_info: Host.Node_Info,
77461
a553e419e9dc tuned signature;
wenzelm
parents: 77460
diff changeset
   176
    current: Boolean
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   177
  ) {
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   178
    def ok: Boolean = process_result.ok
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   179
  }
77312
6a6231370432 clarified signature (see also 68a7ad1385bc);
wenzelm
parents: 77310
diff changeset
   180
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   181
  object State {
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   182
    type Sessions = Map[String, Build_Job.Session_Context]
77583
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   183
    type Workers = List[Worker]
77585
89c42ec77a84 tuned signature;
wenzelm
parents: 77584
diff changeset
   184
    type Pending = List[Task]
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   185
    type Running = Map[String, Job]
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   186
    type Results = Map[String, Result]
77513
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   187
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   188
    def inc_serial(serial: Long): Long = {
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   189
      require(serial < java.lang.Long.MAX_VALUE, "serial overflow")
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   190
      serial + 1
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   191
    }
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   192
  }
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   193
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   194
  sealed case class State(
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   195
    serial: Long = 0,
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   196
    progress_seen: Long = 0,
77525
de6fb423fd4b clarified database content: store actual value instead of index;
wenzelm
parents: 77522
diff changeset
   197
    numa_next: Int = 0,
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   198
    sessions: State.Sessions = Map.empty,   // static build targets
77583
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   199
    workers: State.Workers = Nil,           // available worker processes
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   200
    pending: State.Pending = Nil,           // dynamic build "queue"
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   201
    running: State.Running = Map.empty,     // presently running jobs
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   202
    results: State.Results = Map.empty      // finished results
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   203
  ) {
77513
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   204
    require(serial >= 0, "serial underflow")
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   205
    def inc_serial: State = copy(serial = State.inc_serial(serial))
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   206
    def set_serial(i: Long): State = {
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   207
      require(serial <= i, "non-monotonic change of serial")
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   208
      copy(serial = i)
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   209
    }
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   210
77522
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   211
    def progress_serial(message_serial: Long = serial): State =
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   212
      if (message_serial > progress_seen) copy(progress_seen = message_serial)
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   213
      else error("Bad serial " + message_serial + " for progress output (already seen)")
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   214
77583
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   215
    def set_workers(new_workers: State.Workers): State = copy(workers = new_workers)
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   216
77525
de6fb423fd4b clarified database content: store actual value instead of index;
wenzelm
parents: 77522
diff changeset
   217
    def numa_next_node(numa_nodes: List[Int]): (Option[Int], State) =
77343
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   218
      if (numa_nodes.isEmpty) (None, this)
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   219
      else {
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   220
        val available = numa_nodes.zipWithIndex
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   221
        val used =
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   222
          Set.from(for (job <- running.valuesIterator; i <- job.node_info.numa_node) yield i)
77525
de6fb423fd4b clarified database content: store actual value instead of index;
wenzelm
parents: 77522
diff changeset
   223
de6fb423fd4b clarified database content: store actual value instead of index;
wenzelm
parents: 77522
diff changeset
   224
        val numa_index = available.collectFirst({ case (n, i) if n == numa_next => i }).getOrElse(0)
77343
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   225
        val candidates = available.drop(numa_index) ::: available.take(numa_index)
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   226
        val (n, i) =
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   227
          candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   228
          candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
77525
de6fb423fd4b clarified database content: store actual value instead of index;
wenzelm
parents: 77522
diff changeset
   229
de6fb423fd4b clarified database content: store actual value instead of index;
wenzelm
parents: 77522
diff changeset
   230
        (Some(n), copy(numa_next = numa_nodes((i + 1) % numa_nodes.length)))
77343
db479840d6ad clarified signature;
wenzelm
parents: 77339
diff changeset
   231
      }
77337
1ab68d4370ec tuned signature;
wenzelm
parents: 77336
diff changeset
   232
77335
05b97b54cb3b tuned signature;
wenzelm
parents: 77334
diff changeset
   233
    def finished: Boolean = pending.isEmpty
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   234
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   235
    def remove_pending(name: String): State =
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   236
      copy(pending = pending.flatMap(
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   237
        entry => if (entry.name == name) None else Some(entry.resolve(name))))
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   238
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   239
    def is_running(name: String): Boolean = running.isDefinedAt(name)
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   240
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   241
    def stop_running(): Unit =
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   242
      for (job <- running.valuesIterator; build <- job.build) build.cancel()
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   243
77398
19e9cafaafc5 clarified signature: works for general Build_Job;
wenzelm
parents: 77396
diff changeset
   244
    def finished_running(): List[Build_Job] =
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   245
      List.from(
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   246
        for (job <- running.valuesIterator; build <- job.build if build.is_finished)
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   247
        yield build)
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   248
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   249
    def add_running(job: Job): State =
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   250
      copy(running = running + (job.name -> job))
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   251
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   252
    def remove_running(name: String): State =
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   253
      copy(running = running - name)
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   254
77336
e9beaaf955bf tuned signature;
wenzelm
parents: 77335
diff changeset
   255
    def make_result(
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   256
      name: String,
77461
a553e419e9dc tuned signature;
wenzelm
parents: 77460
diff changeset
   257
      process_result: Process_Result,
77460
ccca589d7027 tuned signature: support general Build_Job instances;
wenzelm
parents: 77459
diff changeset
   258
      output_shasum: SHA1.Shasum,
77475
3bc611c80346 clarified modules;
wenzelm
parents: 77474
diff changeset
   259
      node_info: Host.Node_Info = Host.Node_Info.none,
77461
a553e419e9dc tuned signature;
wenzelm
parents: 77460
diff changeset
   260
      current: Boolean = false
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   261
    ): State = {
77461
a553e419e9dc tuned signature;
wenzelm
parents: 77460
diff changeset
   262
      val entry = name -> Build_Process.Result(process_result, output_shasum, node_info, current)
a553e419e9dc tuned signature;
wenzelm
parents: 77460
diff changeset
   263
      copy(results = results + entry)
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   264
    }
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   265
  }
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   266
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
   267
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   268
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   269
  /** SQL data model **/
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   270
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   271
  object Data {
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   272
    def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   273
      SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body)
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   274
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   275
    object Generic {
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   276
      val build_uuid = SQL.Column.string("build_uuid")
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   277
      val worker_uuid = SQL.Column.string("worker_uuid")
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   278
      val name = SQL.Column.string("name")
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   279
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   280
      def sql(
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   281
        build_uuid: String = "",
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   282
        worker_uuid: String = "",
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   283
        name: String = "",
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   284
        names: Iterable[String] = Nil
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   285
      ): SQL.Source =
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   286
        SQL.and(
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   287
          if_proper(build_uuid, Generic.build_uuid.equal(build_uuid)),
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   288
          if_proper(worker_uuid, Generic.worker_uuid.equal(worker_uuid)),
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   289
          if_proper(name, Generic.name.equal(name)),
77375
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77374
diff changeset
   290
          if_proper(names, Generic.name.member(names)))
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   291
    }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   292
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   293
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   294
    /* base table */
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   295
77417
wenzelm
parents: 77416
diff changeset
   296
    object Base {
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   297
      val build_uuid = Generic.build_uuid.make_primary_key
77387
cd10b8edfdf5 clarified db content: avoid redundancy of historic ML_IDENTIFIER;
wenzelm
parents: 77385
diff changeset
   298
      val ml_platform = SQL.Column.string("ml_platform")
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   299
      val options = SQL.Column.string("options")
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   300
      val start = SQL.Column.date("start")
77545
4af88aca2a4f clarified database content;
wenzelm
parents: 77543
diff changeset
   301
      val stop = SQL.Column.date("stop")
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   302
77545
4af88aca2a4f clarified database content;
wenzelm
parents: 77543
diff changeset
   303
      val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
77536
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   304
    }
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   305
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   306
    def start_build(
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   307
      db: SQL.Database,
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   308
      build_uuid: String,
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   309
      ml_platform: String,
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   310
      options: String
7c7f1473e51a clarified database content and prepare/init stages;
wenzelm
parents: 77534
diff changeset
   311
    ): Unit = {
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   312
      db.execute_statement(Base.table.insert(), body =
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   313
        { stmt =>
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   314
          stmt.string(1) = build_uuid
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   315
          stmt.string(2) = ml_platform
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   316
          stmt.string(3) = options
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   317
          stmt.date(4) = db.now()
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   318
          stmt.date(5) = None
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   319
        })
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   320
    }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   321
77545
4af88aca2a4f clarified database content;
wenzelm
parents: 77543
diff changeset
   322
    def stop_build(db: SQL.Database, build_uuid: String): Unit =
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   323
      db.execute_statement(
77545
4af88aca2a4f clarified database content;
wenzelm
parents: 77543
diff changeset
   324
        Base.table.update(List(Base.stop), sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   325
        body = { stmt => stmt.date(1) = db.now() })
77538
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
   326
77539
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   327
    def clean_build(db: SQL.Database): Unit = {
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   328
      val old =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   329
        db.execute_query_statement(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   330
          Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.defined)),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   331
          List.from[String], res => res.string(Base.build_uuid))
77539
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   332
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   333
      if (old.nonEmpty) {
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   334
        for (table <- List(Base.table, Sessions.table, Progress.table, Workers.table)) {
77540
c537905c2125 tuned signature;
wenzelm
parents: 77539
diff changeset
   335
          db.execute_statement(table.delete(sql = Generic.build_uuid.where_member(old)))
77539
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   336
        }
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   337
      }
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   338
    }
2b996a0df1ce proper clean_build of old data at start of new process --- allow to inspect remains of the last process;
wenzelm
parents: 77538
diff changeset
   339
77416
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   340
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   341
    /* sessions */
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   342
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   343
    object Sessions {
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   344
      val name = Generic.name.make_primary_key
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   345
      val deps = SQL.Column.string("deps")
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   346
      val ancestors = SQL.Column.string("ancestors")
77610
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   347
      val options = SQL.Column.string("options")
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   348
      val sources = SQL.Column.string("sources")
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   349
      val timeout = SQL.Column.long("timeout")
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   350
      val old_time = SQL.Column.long("old_time")
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   351
      val old_command_timings = SQL.Column.bytes("old_command_timings")
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   352
      val build_uuid = Generic.build_uuid
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   353
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   354
      val table = make_table("sessions",
77610
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   355
        List(name, deps, ancestors, options, sources, timeout,
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   356
          old_time, old_command_timings, build_uuid))
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   357
    }
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   358
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   359
    def read_sessions_domain(db: SQL.Database): Set[String] =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   360
      db.execute_query_statement(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   361
        Sessions.table.select(List(Sessions.name)),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   362
        Set.from[String], res => res.string(Sessions.name))
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   363
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   364
    def read_sessions(db: SQL.Database, names: Iterable[String] = Nil): State.Sessions =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   365
      db.execute_query_statement(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   366
        Sessions.table.select(sql = if_proper(names, Sessions.name.where_member(names))),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   367
        Map.from[String, Build_Job.Session_Context],
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   368
        { res =>
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   369
          val name = res.string(Sessions.name)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   370
          val deps = split_lines(res.string(Sessions.deps))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   371
          val ancestors = split_lines(res.string(Sessions.ancestors))
77610
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   372
          val options = res.string(Sessions.options)
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   373
          val sources_shasum = SHA1.fake_shasum(res.string(Sessions.sources))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   374
          val timeout = Time.ms(res.long(Sessions.timeout))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   375
          val old_time = Time.ms(res.long(Sessions.old_time))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   376
          val old_command_timings_blob = res.bytes(Sessions.old_command_timings)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   377
          val build_uuid = res.string(Sessions.build_uuid)
77610
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   378
          name -> Build_Job.Session_Context(name, deps, ancestors, options, sources_shasum,
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   379
            timeout, old_time, old_command_timings_blob, build_uuid)
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   380
        }
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   381
      )
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   382
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   383
    def update_sessions(db:SQL.Database, sessions: State.Sessions): Boolean = {
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   384
      val old_sessions = read_sessions_domain(db)
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   385
      val insert = sessions.iterator.filterNot(p => old_sessions.contains(p._1)).toList
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   386
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   387
      for ((name, session) <- insert) {
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   388
        db.execute_statement(Sessions.table.insert(), body =
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   389
          { stmt =>
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   390
            stmt.string(1) = name
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   391
            stmt.string(2) = cat_lines(session.deps)
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   392
            stmt.string(3) = cat_lines(session.ancestors)
77610
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   393
            stmt.string(4) = session.session_prefs
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   394
            stmt.string(5) = session.sources_shasum.toString
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   395
            stmt.long(6) = session.timeout.ms
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   396
            stmt.long(7) = session.old_time.ms
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   397
            stmt.bytes(8) = session.old_command_timings_blob
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   398
            stmt.string(9) = session.build_uuid
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   399
          })
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   400
      }
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   401
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   402
      insert.nonEmpty
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   403
    }
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   404
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   405
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   406
    /* progress */
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   407
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   408
    object Progress {
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   409
      val serial = SQL.Column.long("serial").make_primary_key
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   410
      val kind = SQL.Column.int("kind")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   411
      val text = SQL.Column.string("text")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   412
      val verbose = SQL.Column.bool("verbose")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   413
      val build_uuid = Generic.build_uuid
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   414
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   415
      val table = make_table("progress", List(serial, kind, text, verbose, build_uuid))
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   416
    }
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   417
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   418
    def read_progress(db: SQL.Database, seen: Long = 0, build_uuid: String = ""): Progress_Messages =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   419
      db.execute_query_statement(
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   420
        Progress.table.select(
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   421
          sql =
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   422
            SQL.where(
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   423
              SQL.and(
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   424
                if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   425
                Generic.sql(build_uuid = build_uuid)))),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   426
        SortedMap.from[Long, isabelle.Progress.Message],
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   427
        { res =>
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   428
          val serial = res.long(Progress.serial)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   429
          val kind = isabelle.Progress.Kind(res.int(Progress.kind))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   430
          val text = res.string(Progress.text)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   431
          val verbose = res.bool(Progress.verbose)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   432
          serial -> isabelle.Progress.Message(kind, text, verbose = verbose)
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   433
        }
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   434
      )
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   435
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   436
    def write_progress(
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   437
      db: SQL.Database,
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   438
      message_serial: Long,
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   439
      message: isabelle.Progress.Message,
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   440
      build_uuid: String
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   441
    ): Unit = {
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   442
      db.execute_statement(Progress.table.insert(), body =
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   443
        { stmt =>
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   444
          stmt.long(1) = message_serial
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   445
          stmt.int(2) = message.kind.id
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   446
          stmt.string(3) = message.text
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   447
          stmt.bool(4) = message.verbose
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   448
          stmt.string(5) = build_uuid
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   449
        })
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   450
    }
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   451
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   452
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   453
    /* workers */
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   454
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   455
    object Workers {
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   456
      val worker_uuid = Generic.worker_uuid.make_primary_key
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   457
      val build_uuid = Generic.build_uuid
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   458
      val hostname = SQL.Column.string("hostname")
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   459
      val java_pid = SQL.Column.long("java_pid")
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   460
      val java_start = SQL.Column.date("java_start")
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   461
      val start = SQL.Column.date("start")
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   462
      val stamp = SQL.Column.date("stamp")
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   463
      val stop = SQL.Column.date("stop")
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   464
      val serial = SQL.Column.long("serial")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   465
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   466
      val table = make_table("workers",
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   467
        List(worker_uuid, build_uuid, hostname, java_pid, java_start, start, stamp, stop, serial))
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   468
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   469
      val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   470
    }
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   471
77586
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   472
    def read_workers(
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   473
      db: SQL.Database,
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   474
      build_uuid: String = "",
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   475
      worker_uuid: String = ""
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   476
    ): State.Workers = {
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   477
      db.execute_query_statement(
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   478
        Workers.table.select(sql =
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   479
          SQL.where(Generic.sql(build_uuid = build_uuid, worker_uuid = worker_uuid))),
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   480
          List.from[Worker],
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   481
          { res =>
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   482
            Worker(
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   483
              worker_uuid = res.string(Workers.worker_uuid),
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   484
              build_uuid = res.string(Workers.build_uuid),
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   485
              hostname = res.string(Workers.hostname),
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   486
              java_pid = res.long(Workers.java_pid),
77588
066d5df144f0 assume total operation: ProcessHandle.current().info.startInstant appears to work on all platforms;
wenzelm
parents: 77587
diff changeset
   487
              java_start = res.date(Workers.java_start),
77586
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   488
              start = res.date(Workers.start),
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   489
              stamp = res.date(Workers.stamp),
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   490
              stop = res.get_date(Workers.stop),
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   491
              serial = res.long(Workers.serial))
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   492
          })
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   493
    }
80021d645a01 tuned structure;
wenzelm
parents: 77585
diff changeset
   494
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   495
    def serial_max(db: SQL.Database): Long =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   496
      db.execute_query_statementO[Long](
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   497
        Workers.table.select(List(Workers.serial_max)),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   498
        res => res.long(Workers.serial)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   499
      ).getOrElse(0L)
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   500
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   501
    def start_worker(
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   502
      db: SQL.Database,
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   503
      worker_uuid: String,
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   504
      build_uuid: String,
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   505
      hostname: String,
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   506
      java_pid: Long,
77588
066d5df144f0 assume total operation: ProcessHandle.current().info.startInstant appears to work on all platforms;
wenzelm
parents: 77587
diff changeset
   507
      java_start: Date
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   508
    ): Long = {
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   509
      def err(msg: String): Nothing =
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   510
        error("Cannot start worker " + worker_uuid + if_proper(msg, "\n" + msg))
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   511
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   512
      val build_stop =
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   513
        db.execute_query_statementO(
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   514
          Base.table.select(List(Base.stop),
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   515
            sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   516
          res => res.get_date(Base.stop))
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   517
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   518
      build_stop match {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   519
        case Some(None) =>
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   520
        case Some(Some(_)) => err("for already stopped build process " + build_uuid)
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   521
        case None => err("for unknown build process " + build_uuid)
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   522
      }
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   523
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   524
      val serial = serial_max(db)
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   525
      db.execute_statement(Workers.table.insert(), body =
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   526
        { stmt =>
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   527
          val now = db.now()
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   528
          stmt.string(1) = worker_uuid
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   529
          stmt.string(2) = build_uuid
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   530
          stmt.string(3) = hostname
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   531
          stmt.long(4) = java_pid
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   532
          stmt.date(5) = java_start
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   533
          stmt.date(6) = now
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   534
          stmt.date(7) = now
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   535
          stmt.date(8) = None
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   536
          stmt.long(9) = serial
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   537
        })
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   538
      serial
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   539
    }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   540
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   541
    def stamp_worker(
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   542
      db: SQL.Database,
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   543
      worker_uuid: String,
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   544
      serial: Long,
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   545
      stop: Boolean = false
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   546
    ): Unit = {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   547
      val sql =
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   548
        Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial),
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   549
          sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   550
      db.execute_statement(sql, body =
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   551
        { stmt =>
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   552
          val now = db.now()
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   553
          stmt.date(1) = now
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   554
          stmt.date(2) = if (stop) Some(now) else None
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   555
          stmt.long(3) = serial
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   556
        })
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   557
    }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   558
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   559
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   560
    /* pending jobs */
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   561
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   562
    object Pending {
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   563
      val name = Generic.name.make_primary_key
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   564
      val deps = SQL.Column.string("deps")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   565
      val info = SQL.Column.string("info")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   566
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   567
      val table = make_table("pending", List(name, deps, info))
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   568
    }
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   569
77585
89c42ec77a84 tuned signature;
wenzelm
parents: 77584
diff changeset
   570
    def read_pending(db: SQL.Database): List[Task] =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   571
      db.execute_query_statement(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   572
        Pending.table.select(sql = SQL.order_by(List(Pending.name))),
77585
89c42ec77a84 tuned signature;
wenzelm
parents: 77584
diff changeset
   573
        List.from[Task],
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   574
        { res =>
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   575
          val name = res.string(Pending.name)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   576
          val deps = res.string(Pending.deps)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   577
          val info = res.string(Pending.info)
77585
89c42ec77a84 tuned signature;
wenzelm
parents: 77584
diff changeset
   578
          Task(name, split_lines(deps), info = JSON.Object.parse(info))
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   579
        })
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   580
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   581
    def update_pending(db: SQL.Database, pending: State.Pending): Boolean = {
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   582
      val old_pending = read_pending(db)
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   583
      val (delete, insert) = Library.symmetric_difference(old_pending, pending)
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   584
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   585
      if (delete.nonEmpty) {
77540
c537905c2125 tuned signature;
wenzelm
parents: 77539
diff changeset
   586
        db.execute_statement(
c537905c2125 tuned signature;
wenzelm
parents: 77539
diff changeset
   587
          Pending.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name)))))
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   588
      }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   589
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   590
      for (entry <- insert) {
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   591
        db.execute_statement(Pending.table.insert(), body =
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   592
          { stmt =>
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   593
            stmt.string(1) = entry.name
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   594
            stmt.string(2) = cat_lines(entry.deps)
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   595
            stmt.string(3) = JSON.Format(entry.info)
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   596
          })
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   597
      }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   598
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   599
      delete.nonEmpty || insert.nonEmpty
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   600
    }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   601
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   602
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   603
    /* running jobs */
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   604
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   605
    object Running {
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   606
      val name = Generic.name.make_primary_key
77587
8036d5f12997 more database content, e.g. for monitoring;
wenzelm
parents: 77586
diff changeset
   607
      val worker_uuid = Generic.worker_uuid
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   608
      val hostname = SQL.Column.string("hostname")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   609
      val numa_node = SQL.Column.int("numa_node")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   610
77587
8036d5f12997 more database content, e.g. for monitoring;
wenzelm
parents: 77586
diff changeset
   611
      val table = make_table("running", List(name, worker_uuid, hostname, numa_node))
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   612
    }
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   613
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   614
    def read_running(db: SQL.Database): List[Job] =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   615
      db.execute_query_statement(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   616
        Running.table.select(sql = SQL.order_by(List(Running.name))),
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   617
        List.from[Job],
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   618
        { res =>
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   619
          val name = res.string(Running.name)
77587
8036d5f12997 more database content, e.g. for monitoring;
wenzelm
parents: 77586
diff changeset
   620
          val worker_uuid = res.string(Running.worker_uuid)
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   621
          val hostname = res.string(Running.hostname)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   622
          val numa_node = res.get_int(Running.numa_node)
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   623
          Job(name, worker_uuid, Host.Node_Info(hostname, numa_node), None)
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   624
        }
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   625
      )
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   626
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   627
    def update_running(db: SQL.Database, running: State.Running): Boolean = {
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   628
      val running0 = read_running(db)
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   629
      val running1 = running.valuesIterator.map(_.no_build).toList
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   630
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   631
      val (delete, insert) = Library.symmetric_difference(running0, running1)
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   632
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   633
      if (delete.nonEmpty) {
77540
c537905c2125 tuned signature;
wenzelm
parents: 77539
diff changeset
   634
        db.execute_statement(
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   635
          Running.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name)))))
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   636
      }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   637
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   638
      for (job <- insert) {
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   639
        db.execute_statement(Running.table.insert(), body =
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   640
          { stmt =>
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   641
            stmt.string(1) = job.name
77587
8036d5f12997 more database content, e.g. for monitoring;
wenzelm
parents: 77586
diff changeset
   642
            stmt.string(2) = job.worker_uuid
8036d5f12997 more database content, e.g. for monitoring;
wenzelm
parents: 77586
diff changeset
   643
            stmt.string(3) = job.node_info.hostname
8036d5f12997 more database content, e.g. for monitoring;
wenzelm
parents: 77586
diff changeset
   644
            stmt.int(4) = job.node_info.numa_node
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   645
          })
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   646
      }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   647
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   648
      delete.nonEmpty || insert.nonEmpty
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   649
    }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   650
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   651
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   652
    /* job results */
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   653
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   654
    object Results {
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   655
      val name = Generic.name.make_primary_key
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   656
      val hostname = SQL.Column.string("hostname")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   657
      val numa_node = SQL.Column.string("numa_node")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   658
      val rc = SQL.Column.int("rc")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   659
      val out = SQL.Column.string("out")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   660
      val err = SQL.Column.string("err")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   661
      val timing_elapsed = SQL.Column.long("timing_elapsed")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   662
      val timing_cpu = SQL.Column.long("timing_cpu")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   663
      val timing_gc = SQL.Column.long("timing_gc")
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   664
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   665
      val table =
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   666
        make_table("results",
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   667
          List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc))
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   668
    }
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   669
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   670
    def read_results_domain(db: SQL.Database): Set[String] =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   671
      db.execute_query_statement(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   672
        Results.table.select(List(Results.name)),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   673
        Set.from[String], res => res.string(Results.name))
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   674
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   675
    def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] =
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   676
      db.execute_query_statement(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   677
        Results.table.select(sql = if_proper(names, Results.name.where_member(names))),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   678
        Map.from[String, Build_Job.Result],
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   679
        { res =>
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   680
          val name = res.string(Results.name)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   681
          val hostname = res.string(Results.hostname)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   682
          val numa_node = res.get_int(Results.numa_node)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   683
          val rc = res.int(Results.rc)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   684
          val out = res.string(Results.out)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   685
          val err = res.string(Results.err)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   686
          val timing =
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   687
            res.timing(
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   688
              Results.timing_elapsed,
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   689
              Results.timing_cpu,
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   690
              Results.timing_gc)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   691
          val node_info = Host.Node_Info(hostname, numa_node)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   692
          val process_result =
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   693
            Process_Result(rc,
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   694
              out_lines = split_lines(out),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   695
              err_lines = split_lines(err),
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   696
              timing = timing)
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   697
          name -> Build_Job.Result(node_info, process_result)
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   698
        }
77552
080422b3d914 clarified signature: reduce boilerplate;
wenzelm
parents: 77551
diff changeset
   699
      )
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   700
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   701
    def update_results(db: SQL.Database, results: State.Results): Boolean = {
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   702
      val old_results = read_results_domain(db)
77385
4a7c42c84743 proper filterNot, not filterNot-not;
wenzelm
parents: 77383
diff changeset
   703
      val insert = results.iterator.filterNot(p => old_results.contains(p._1)).toList
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   704
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   705
      for ((name, result) <- insert) {
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   706
        val node_info = result.node_info
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   707
        val process_result = result.process_result
77541
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   708
        db.execute_statement(Results.table.insert(), body =
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   709
          { stmt =>
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   710
            stmt.string(1) = name
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   711
            stmt.string(2) = node_info.hostname
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   712
            stmt.int(3) = node_info.numa_node
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   713
            stmt.int(4) = process_result.rc
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   714
            stmt.string(5) = cat_lines(process_result.out_lines)
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   715
            stmt.string(6) = cat_lines(process_result.err_lines)
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   716
            stmt.long(7) = process_result.timing.elapsed.ms
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   717
            stmt.long(8) = process_result.timing.cpu.ms
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   718
            stmt.long(9) = process_result.timing.gc.ms
9d9b30741fc4 tuned signature: reduce boilerplate;
wenzelm
parents: 77540
diff changeset
   719
          })
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   720
      }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   721
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   722
      insert.nonEmpty
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   723
    }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   724
77531
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   725
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   726
    /* collective operations */
3481e54bd8f1 tuned comments;
wenzelm
parents: 77530
diff changeset
   727
77596
dd8b08729458 clarified signature;
wenzelm
parents: 77594
diff changeset
   728
    val all_tables: SQL.Tables =
dd8b08729458 clarified signature;
wenzelm
parents: 77594
diff changeset
   729
      SQL.Tables(
77534
wenzelm
parents: 77533
diff changeset
   730
        Base.table,
wenzelm
parents: 77533
diff changeset
   731
        Workers.table,
wenzelm
parents: 77533
diff changeset
   732
        Progress.table,
wenzelm
parents: 77533
diff changeset
   733
        Sessions.table,
wenzelm
parents: 77533
diff changeset
   734
        Pending.table,
wenzelm
parents: 77533
diff changeset
   735
        Running.table,
wenzelm
parents: 77533
diff changeset
   736
        Results.table,
wenzelm
parents: 77533
diff changeset
   737
        Host.Data.Node_Info.table)
wenzelm
parents: 77533
diff changeset
   738
77416
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   739
    def update_database(
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   740
      db: SQL.Database,
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   741
      worker_uuid: String,
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   742
      build_uuid: String,
77416
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   743
      hostname: String,
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   744
      state: State
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   745
    ): State = {
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   746
      val changed =
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   747
        List(
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   748
          update_sessions(db, state.sessions),
77416
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   749
          update_pending(db, state.pending),
d88c12f22ab0 clarified scope of "serial" and "numa_index" within database;
wenzelm
parents: 77415
diff changeset
   750
          update_running(db, state.running),
77476
5f6f567a2661 clarified modules;
wenzelm
parents: 77475
diff changeset
   751
          update_results(db, state.results),
77525
de6fb423fd4b clarified database content: store actual value instead of index;
wenzelm
parents: 77522
diff changeset
   752
          Host.Data.update_numa_next(db, hostname, state.numa_next))
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   753
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   754
      val serial0 = serial_max(db)
77513
43bfb65ee9b3 more robust: proper bound checks;
wenzelm
parents: 77511
diff changeset
   755
      val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   756
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   757
      stamp_worker(db, worker_uuid, serial)
77583
9af2afc3f7b3 more explicit workers, e.g. for monitoring;
wenzelm
parents: 77580
diff changeset
   758
      state.set_serial(serial).set_workers(read_workers(db))
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   759
    }
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   760
  }
77396
f184fbac99bc clarified modules;
wenzelm
parents: 77395
diff changeset
   761
}
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   762
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   763
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   764
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   765
/** main process **/
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   766
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   767
class Build_Process(
77530
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   768
  protected final val build_context: Build_Process.Context,
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   769
  protected final val build_progress: Progress
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   770
)
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   771
extends AutoCloseable {
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   772
  /* context */
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   773
77530
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   774
  protected final val store: Sessions.Store = build_context.store
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   775
  protected final val build_options: Options = store.options
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   776
  protected final val build_deps: Sessions.Deps = build_context.build_deps
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   777
  protected final val build_uuid: String = build_context.build_uuid
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   778
  protected final val worker_uuid: String = UUID.random().toString
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   779
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   780
77437
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   781
  /* global state: internal var vs. external database */
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   782
77437
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   783
  private var _state: Build_Process.State = init_state(Build_Process.State())
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   784
77629
979baa91da0f clarified modules;
wenzelm
parents: 77610
diff changeset
   785
  private val _database: Option[SQL.Database] = store.open_build_database()
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   786
77466
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   787
  def close(): Unit = synchronized { _database.foreach(_.close()) }
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   788
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   789
  protected def synchronized_database[A](body: => A): A =
77438
0030eabbe6c3 more robust: synchronized access to database;
wenzelm
parents: 77437
diff changeset
   790
    synchronized {
77466
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   791
      _database match {
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   792
        case None => body
77596
dd8b08729458 clarified signature;
wenzelm
parents: 77594
diff changeset
   793
        case Some(db) => db.transaction_lock(Build_Process.Data.all_tables)(body)
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   794
      }
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   795
    }
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   796
77466
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   797
  private def sync_database(): Unit =
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   798
    synchronized_database {
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   799
      for (db <- _database) {
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   800
        _state =
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   801
          Build_Process.Data.update_database(
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   802
            db, worker_uuid, build_uuid, build_context.hostname, _state)
77466
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   803
      }
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   804
    }
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   805
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   806
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   807
  /* progress backed by database */
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   808
77533
wenzelm
parents: 77531
diff changeset
   809
  private def progress_output(message: Progress.Message, build_progress_output: => Unit): Unit = {
77522
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   810
    synchronized_database {
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   811
      val state1 = _state.inc_serial.progress_serial()
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   812
      for (db <- _database) {
77529
40ccee0fe19a separate static build_uuid from dynamic worker_uuid, to allow multiple worker processes participate in one build process;
wenzelm
parents: 77527
diff changeset
   813
        Build_Process.Data.write_progress(db, state1.serial, message, build_uuid)
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   814
        Build_Process.Data.stamp_worker(db, worker_uuid, state1.serial)
77522
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   815
      }
77533
wenzelm
parents: 77531
diff changeset
   816
      build_progress_output
77522
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   817
      _state = state1
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   818
    }
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   819
  }
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   820
77530
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   821
  protected object progress extends Progress {
77509
3bc49507bae5 clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents: 77505
diff changeset
   822
    override def verbose: Boolean = build_progress.verbose
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   823
77509
3bc49507bae5 clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents: 77505
diff changeset
   824
    override def output(message: Progress.Message): Unit =
77522
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   825
      progress_output(message, if (do_output(message)) build_progress.output(message))
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   826
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   827
    override def theory(theory: Progress.Theory): Unit =
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   828
      progress_output(theory.message, build_progress.theory(theory))
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   829
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   830
    override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
a1d30297cd61 more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents: 77521
diff changeset
   831
      build_progress.nodes_status(nodes_status)
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   832
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   833
    override def stop(): Unit = build_progress.stop()
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   834
    override def stopped: Boolean = build_progress.stopped
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   835
  }
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   836
77530
3362f84a300a tuned signature: avoid totally adhoc overriding;
wenzelm
parents: 77529
diff changeset
   837
  protected val log: Logger = Logger.make_system_log(progress, build_options)
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   838
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   839
77437
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   840
  /* policy operations */
77333
0bec014c0f9f tuned signature;
wenzelm
parents: 77332
diff changeset
   841
77415
6b928419f109 clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents: 77414
diff changeset
   842
  protected def init_state(state: Build_Process.State): Build_Process.State = {
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   843
    val sessions1 =
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   844
      build_context.sessions.foldLeft(state.sessions) { case (map, (name, session)) =>
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   845
        if (state.sessions.isDefinedAt(name)) map
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   846
        else map + (name -> session)
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   847
      }
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   848
77415
6b928419f109 clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents: 77414
diff changeset
   849
    val old_pending = state.pending.iterator.map(_.name).toSet
6b928419f109 clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents: 77414
diff changeset
   850
    val new_pending =
6b928419f109 clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents: 77414
diff changeset
   851
      List.from(
6b928419f109 clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents: 77414
diff changeset
   852
        for {
77449
wenzelm
parents: 77448
diff changeset
   853
          (name, session_context) <- build_context.sessions.iterator
77415
6b928419f109 clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents: 77414
diff changeset
   854
          if !old_pending(name)
77585
89c42ec77a84 tuned signature;
wenzelm
parents: 77584
diff changeset
   855
        } yield Build_Process.Task(name, session_context.deps))
77496
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   856
    val pending1 = new_pending ::: state.pending
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   857
f0d9f9196b9b more database content;
wenzelm
parents: 77495
diff changeset
   858
    state.copy(sessions = sessions1, pending = pending1)
77415
6b928419f109 clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents: 77414
diff changeset
   859
  }
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   860
77437
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   861
  protected def next_job(state: Build_Process.State): Option[String] =
77578
149d48a4801b support for "isabelle build -j0": require external workers to make progress;
wenzelm
parents: 77561
diff changeset
   862
    if (progress.stopped || state.running.size < build_context.max_jobs) {
77437
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   863
      state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
77313
f8aa1647d156 more elementary data structures, to fit better to SQL database;
wenzelm
parents: 77312
diff changeset
   864
        .sortBy(_.name)(build_context.ordering)
f8aa1647d156 more elementary data structures, to fit better to SQL database;
wenzelm
parents: 77312
diff changeset
   865
        .headOption.map(_.name)
77296
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   866
    }
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   867
    else None
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   868
77467
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   869
  protected def start_session(state: Build_Process.State, session_name: String): Build_Process.State = {
77468
wenzelm
parents: 77467
diff changeset
   870
    val ancestor_results =
wenzelm
parents: 77467
diff changeset
   871
      for (a <- build_context.sessions(session_name).ancestors) yield state.results(a)
77467
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   872
77460
ccca589d7027 tuned signature: support general Build_Job instances;
wenzelm
parents: 77459
diff changeset
   873
    val input_shasum =
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   874
      if (ancestor_results.isEmpty) {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   875
        SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   876
      }
77460
ccca589d7027 tuned signature: support general Build_Job instances;
wenzelm
parents: 77459
diff changeset
   877
      else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   878
77463
4e8bec105ce5 tuned signature;
wenzelm
parents: 77462
diff changeset
   879
    val store_heap = build_context.store_heap(session_name)
77469
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   880
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   881
    val (current, output_shasum) =
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   882
      store.check_output(session_name,
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   883
        sources_shasum = build_context.sources_shasum(session_name),
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   884
        input_shasum = input_shasum,
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   885
        fresh_build = build_context.fresh_build,
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   886
        store_heap = store_heap)
5af7e8ffcab7 clarified modules;
wenzelm
parents: 77468
diff changeset
   887
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   888
    val all_current = current && ancestor_results.forall(_.current)
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   889
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   890
    if (all_current) {
77467
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   891
      state
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   892
        .remove_pending(session_name)
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   893
        .make_result(session_name, Process_Result.ok, output_shasum, current = true)
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   894
    }
77315
f34559b24277 clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents: 77314
diff changeset
   895
    else if (build_context.no_build) {
77521
5642de4d225d clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77514
diff changeset
   896
      progress.echo("Skipping " + session_name + " ...", verbose = true)
77467
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   897
      state.
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   898
        remove_pending(session_name).
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   899
        make_result(session_name, Process_Result.error, output_shasum)
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   900
    }
77578
149d48a4801b support for "isabelle build -j0": require external workers to make progress;
wenzelm
parents: 77561
diff changeset
   901
    else if (progress.stopped || !ancestor_results.forall(_.ok)) {
77452
wenzelm
parents: 77449
diff changeset
   902
      progress.echo(session_name + " CANCELLED")
77467
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   903
      state
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   904
        .remove_pending(session_name)
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   905
        .make_result(session_name, Process_Result.undefined, output_shasum)
77452
wenzelm
parents: 77449
diff changeset
   906
    }
wenzelm
parents: 77449
diff changeset
   907
    else {
77551
ae6df8a8685a clarified messages;
wenzelm
parents: 77546
diff changeset
   908
      val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes)
ae6df8a8685a clarified messages;
wenzelm
parents: 77546
diff changeset
   909
      val node_info = Host.Node_Info(build_context.hostname, numa_node)
ae6df8a8685a clarified messages;
wenzelm
parents: 77546
diff changeset
   910
ae6df8a8685a clarified messages;
wenzelm
parents: 77546
diff changeset
   911
      progress.echo(
ae6df8a8685a clarified messages;
wenzelm
parents: 77546
diff changeset
   912
        (if (store_heap) "Building " else "Running ") + session_name +
ae6df8a8685a clarified messages;
wenzelm
parents: 77546
diff changeset
   913
          if_proper(node_info.numa_node, " on " + node_info) + " ...")
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   914
77472
a073ac3f3b56 clarified modules;
wenzelm
parents: 77470
diff changeset
   915
      store.init_output(session_name)
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   916
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   917
      val build =
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   918
        Build_Job.start_session(build_context, progress, log,
77505
7ee426daafa3 support progress backed by database;
wenzelm
parents: 77496
diff changeset
   919
          build_deps.background(session_name), input_shasum, node_info)
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   920
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   921
      state1.add_running(Build_Process.Job(session_name, worker_uuid, node_info, Some(build)))
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   922
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   923
  }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   924
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   925
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   926
  /* build process roles */
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   927
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   928
  final def start_build(): Unit = synchronized_database {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   929
    for (db <- _database) {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   930
      Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
77610
3b09ae9e40cb clarified session prefs (or "options" within the database);
wenzelm
parents: 77609
diff changeset
   931
        build_context.sessions_structure.session_prefs)
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   932
    }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   933
  }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   934
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   935
  final def stop_build(): Unit = synchronized_database {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   936
    for (db <- _database) {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   937
      Build_Process.Data.stop_build(db, build_uuid)
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   938
    }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   939
  }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   940
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   941
  final def start_worker(): Unit = synchronized_database {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   942
    for (db <- _database) {
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   943
      val java = ProcessHandle.current()
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   944
      val java_pid = java.pid
77588
066d5df144f0 assume total operation: ProcessHandle.current().info.startInstant appears to work on all platforms;
wenzelm
parents: 77587
diff changeset
   945
      val java_start = Date.instant(java.info.startInstant.get)
77584
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   946
      val serial =
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   947
        Build_Process.Data.start_worker(
42922317b676 more database content, e.g. for monitoring;
wenzelm
parents: 77583
diff changeset
   948
          db, worker_uuid, build_uuid, build_context.hostname, java_pid, java_start)
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   949
      _state = _state.set_serial(serial)
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   950
    }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   951
  }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   952
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   953
  final def stop_worker(): Unit = synchronized_database {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   954
    for (db <- _database) {
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   955
      Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop = true)
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   956
    }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   957
  }
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   958
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   959
77436
c10fa027caa0 tuned comments and outline;
wenzelm
parents: 77417
diff changeset
   960
  /* run */
77372
44fe9fe96130 support for build database: still inactive;
wenzelm
parents: 77344
diff changeset
   961
77579
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
   962
  def run(): Map[String, Process_Result] = {
77466
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
   963
    def finished(): Boolean = synchronized_database { _state.finished }
77400
f3e5b3fe230e clarified signature: more explicit "synchronized" regions;
wenzelm
parents: 77398
diff changeset
   964
77437
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   965
    def sleep(): Unit =
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   966
      Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   967
        build_options.seconds("editor_input_delay").sleep()
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   968
      }
dcbf96acae27 clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents: 77436
diff changeset
   969
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
   970
    def start_job(): Boolean = synchronized_database {
77467
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   971
      next_job(_state) match {
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   972
        case Some(name) =>
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   973
          if (Build_Job.is_session_name(name)) {
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   974
            _state = start_session(_state, name)
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   975
            true
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   976
          }
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   977
          else error("Unsupported build job name " + quote(name))
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   978
        case None => false
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   979
      }
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   980
    }
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
   981
77335
05b97b54cb3b tuned signature;
wenzelm
parents: 77334
diff changeset
   982
    if (finished()) {
05b97b54cb3b tuned signature;
wenzelm
parents: 77334
diff changeset
   983
      progress.echo_warning("Nothing to build")
05b97b54cb3b tuned signature;
wenzelm
parents: 77334
diff changeset
   984
      Map.empty[String, Process_Result]
05b97b54cb3b tuned signature;
wenzelm
parents: 77334
diff changeset
   985
    }
05b97b54cb3b tuned signature;
wenzelm
parents: 77334
diff changeset
   986
    else {
77579
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
   987
      if (build_context.master) start_build()
77578
149d48a4801b support for "isabelle build -j0": require external workers to make progress;
wenzelm
parents: 77561
diff changeset
   988
77580
32f9e75c92e9 clarified worker state: always maintain database content via worker_uuid;
wenzelm
parents: 77579
diff changeset
   989
      start_worker()
32f9e75c92e9 clarified worker state: always maintain database content via worker_uuid;
wenzelm
parents: 77579
diff changeset
   990
      if (build_context.master && !build_context.worker_active) {
32f9e75c92e9 clarified worker state: always maintain database content via worker_uuid;
wenzelm
parents: 77579
diff changeset
   991
        progress.echo("Waiting for external workers ...")
32f9e75c92e9 clarified worker state: always maintain database content via worker_uuid;
wenzelm
parents: 77579
diff changeset
   992
      }
77578
149d48a4801b support for "isabelle build -j0": require external workers to make progress;
wenzelm
parents: 77561
diff changeset
   993
77538
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
   994
      try {
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
   995
        while (!finished()) {
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
   996
          if (progress.stopped) synchronized_database { _state.stop_running() }
77310
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   997
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   998
          for (build <- synchronized_database { _state.finished_running() }) {
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
   999
            val job_name = build.job_name
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
  1000
            val (process_result, output_shasum) = build.join
77538
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1001
            synchronized_database {
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1002
              _state = _state.
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1003
                remove_pending(job_name).
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1004
                remove_running(job_name).
77630
86ef80d13544 clarified signature: avoid confusion due to object-orientation;
wenzelm
parents: 77629
diff changeset
  1005
                make_result(job_name, process_result, output_shasum, node_info = build.node_info)
77538
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1006
            }
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1007
          }
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1008
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
  1009
          if (!start_job()) {
77538
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1010
            sync_database()
fcda9a009213 more database content: formal end_build;
wenzelm
parents: 77536
diff changeset
  1011
            sleep()
77396
f184fbac99bc clarified modules;
wenzelm
parents: 77395
diff changeset
  1012
          }
f184fbac99bc clarified modules;
wenzelm
parents: 77395
diff changeset
  1013
        }
77310
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
  1014
      }
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
  1015
      finally {
77580
32f9e75c92e9 clarified worker state: always maintain database content via worker_uuid;
wenzelm
parents: 77579
diff changeset
  1016
        stop_worker()
77579
69d3547206db clarified signature: prefer Build_Process.Context for parameters;
wenzelm
parents: 77578
diff changeset
  1017
        if (build_context.master) stop_build()
77546
9b9179cda155 clarified build process roles: "worker" vs. "build";
wenzelm
parents: 77545
diff changeset
  1018
      }
77467
e27bc7957297 more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents: 77466
diff changeset
  1019
77466
94dcf2c3895a more thorough synchronized_database for internal *and* external state;
wenzelm
parents: 77465
diff changeset
  1020
      synchronized_database {
77334
0231e62956a6 clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents: 77333
diff changeset
  1021
        for ((name, result) <- _state.results) yield name -> result.process_result
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
  1022
      }
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
  1023
    }
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
  1024
  }
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
  1025
}