src/Pure/Tools/build_process.scala
author wenzelm
Mon, 20 Feb 2023 10:29:45 +0100
changeset 77310 6754b5eceb12
parent 77297 226a880d0423
child 77312 6a6231370432
permissions -rw-r--r--
clarified modules; clarified signature;
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
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    11
import scala.math.Ordering
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
    12
import scala.collection.immutable.SortedSet
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 {
77244
2e5a3955bc69 clarified signature and terminology;
wenzelm
parents: 77241
diff changeset
    17
  /* static information */
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    18
77244
2e5a3955bc69 clarified signature and terminology;
wenzelm
parents: 77241
diff changeset
    19
  object Session_Context {
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    20
    def empty(session: String, timeout: Time): Session_Context =
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    21
      new Session_Context(session, timeout, Time.zero, Nil)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    22
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    23
    def apply(
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    24
      session: String,
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    25
      timeout: Time,
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    26
      store: Sessions.Store,
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    27
      progress: Progress = new Progress
77244
2e5a3955bc69 clarified signature and terminology;
wenzelm
parents: 77241
diff changeset
    28
    ): Session_Context = {
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    29
      store.try_open_database(session) match {
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    30
        case None => empty(session, timeout)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    31
        case Some(db) =>
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    32
          def ignore_error(msg: String) = {
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    33
            progress.echo_warning("Ignoring bad database " + db +
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    34
              " for session " + quote(session) + (if (msg == "") "" else ":\n" + msg))
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    35
            empty(session, timeout)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    36
          }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    37
          try {
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    38
            val command_timings = store.read_command_timings(db, session)
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    39
            val elapsed =
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    40
              store.read_session_timing(db, session) match {
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    41
                case Markup.Elapsed(s) => Time.seconds(s)
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    42
                case _ => Time.zero
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    43
              }
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    44
            new Session_Context(session, timeout, elapsed, command_timings)
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    45
          }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    46
          catch {
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    47
            case ERROR(msg) => ignore_error(msg)
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    48
            case exn: java.lang.Error => ignore_error(Exn.message(exn))
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    49
            case _: XML.Error => ignore_error("XML.Error")
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    50
          }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    51
          finally { db.close() }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    52
      }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    53
    }
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
    54
  }
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    55
77244
2e5a3955bc69 clarified signature and terminology;
wenzelm
parents: 77241
diff changeset
    56
  final class Session_Context(
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    57
    val session: String,
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    58
    val timeout: Time,
77244
2e5a3955bc69 clarified signature and terminology;
wenzelm
parents: 77241
diff changeset
    59
    val old_time: Time,
2e5a3955bc69 clarified signature and terminology;
wenzelm
parents: 77241
diff changeset
    60
    val old_command_timings: List[Properties.T]
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    61
  ) {
77244
2e5a3955bc69 clarified signature and terminology;
wenzelm
parents: 77241
diff changeset
    62
    def is_empty: Boolean = old_time.is_zero && old_command_timings.isEmpty
77240
2ff94ba22140 tuned signature: more operations;
wenzelm
parents: 77239
diff changeset
    63
77245
1e2670d9dc18 tuned message: old_time not sufficiently prominent nor accurate to be printed;
wenzelm
parents: 77244
diff changeset
    64
    override def toString: String = session
77239
b9bf4c0bd47d clarified signature: more explicit types;
wenzelm
parents: 77238
diff changeset
    65
  }
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    66
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    67
  object Context {
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    68
    def apply(
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    69
      store: Sessions.Store,
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
    70
      deps: Sessions.Deps,
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    71
      progress: Progress = new Progress
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    72
    ): Context = {
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
    73
      val sessions_structure = deps.sessions_structure
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    74
      val build_graph = sessions_structure.build_graph
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    75
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    76
      val sessions =
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
    77
        Map.from(
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    78
          for (name <- build_graph.keys_iterator)
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    79
          yield {
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    80
            val timeout = sessions_structure(name).timeout
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    81
            name -> Build_Process.Session_Context(name, timeout, store, progress = progress)
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
    82
          })
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    83
77248
wenzelm
parents: 77247
diff changeset
    84
      val sessions_time = {
wenzelm
parents: 77247
diff changeset
    85
        val maximals = build_graph.maximals.toSet
wenzelm
parents: 77247
diff changeset
    86
        def descendants_time(name: String): Double = {
wenzelm
parents: 77247
diff changeset
    87
          if (maximals.contains(name)) sessions(name).old_time.seconds
wenzelm
parents: 77247
diff changeset
    88
          else {
wenzelm
parents: 77247
diff changeset
    89
            val descendants = build_graph.all_succs(List(name)).toSet
wenzelm
parents: 77247
diff changeset
    90
            val g = build_graph.restrict(descendants)
wenzelm
parents: 77247
diff changeset
    91
            (0.0 :: g.maximals.flatMap { desc =>
wenzelm
parents: 77247
diff changeset
    92
              val ps = g.all_preds(List(desc))
wenzelm
parents: 77247
diff changeset
    93
              if (ps.exists(p => !sessions.isDefinedAt(p))) None
wenzelm
parents: 77247
diff changeset
    94
              else Some(ps.map(p => sessions(p).old_time.seconds).sum)
wenzelm
parents: 77247
diff changeset
    95
            }).max
wenzelm
parents: 77247
diff changeset
    96
          }
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
    97
        }
77248
wenzelm
parents: 77247
diff changeset
    98
        Map.from(
wenzelm
parents: 77247
diff changeset
    99
          for (name <- sessions.keysIterator)
wenzelm
parents: 77247
diff changeset
   100
          yield name -> descendants_time(name)).withDefaultValue(0.0)
77247
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
   101
      }
6ed94a0ec723 misc tuning and clarification;
wenzelm
parents: 77246
diff changeset
   102
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   103
      val ordering =
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   104
        new Ordering[String] {
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   105
          def compare(name1: String, name2: String): Int =
77248
wenzelm
parents: 77247
diff changeset
   106
            sessions_time(name2) compare sessions_time(name1) match {
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   107
              case 0 =>
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
   108
                sessions(name2).timeout compare sessions(name1).timeout match {
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   109
                  case 0 => name1 compare name2
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   110
                  case ord => ord
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   111
                }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   112
              case ord => ord
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   113
            }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   114
        }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   115
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   116
      new Context(store, deps, sessions, ordering, progress)
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   117
    }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   118
  }
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   119
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   120
  final class Context private(
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   121
    val store: Sessions.Store,
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   122
    val deps: Sessions.Deps,
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   123
    sessions: Map[String, Session_Context],
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   124
    val ordering: Ordering[String],
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   125
    val progress: Progress
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   126
  ) {
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   127
    def sessions_structure: Sessions.Structure = deps.sessions_structure
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   128
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   129
    def apply(session: String): Session_Context =
77249
f3f1b7ad1d0d clarified data structure: more direct access to timeout;
wenzelm
parents: 77248
diff changeset
   130
      sessions.getOrElse(session, Session_Context.empty(session, Time.zero))
77255
b810e99b5afb clarified static build_context vs. dynamic queue;
wenzelm
parents: 77254
diff changeset
   131
77256
25e923c57af7 clarified signature;
wenzelm
parents: 77255
diff changeset
   132
    def build_heap(session: String): Boolean =
25e923c57af7 clarified signature;
wenzelm
parents: 77255
diff changeset
   133
      Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)
77246
173c2fb78290 clarified modules;
wenzelm
parents: 77245
diff changeset
   134
  }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   135
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   136
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   137
  /* main */
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   138
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   139
  case class Result(
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   140
    current: Boolean,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   141
    output_heap: SHA1.Shasum,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   142
    process_result: Process_Result
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   143
  ) {
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   144
    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
   145
  }
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   146
}
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   147
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   148
class Build_Process(
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   149
  build_context: Build_Process.Context,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   150
  build_heap: Boolean = false,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   151
  numa_shuffling: Boolean = false,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   152
  max_jobs: Int = 1,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   153
  fresh_build: Boolean = false,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   154
  no_build: Boolean = false,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   155
  verbose: Boolean = false,
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   156
  session_setup: (String, Session) => Unit = (_, _) => ()
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   157
) {
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   158
  private val store = build_context.store
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   159
  private val build_options = store.options
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   160
  private val build_deps = build_context.deps
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   161
  private val progress = build_context.progress
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   162
77287
wenzelm
parents: 77285
diff changeset
   163
  private val log =
wenzelm
parents: 77285
diff changeset
   164
    build_options.string("system_log") match {
wenzelm
parents: 77285
diff changeset
   165
      case "" => No_Logger
wenzelm
parents: 77285
diff changeset
   166
      case "-" => Logger.make(progress)
wenzelm
parents: 77285
diff changeset
   167
      case log_file => Logger.make(Some(Path.explode(log_file)))
wenzelm
parents: 77285
diff changeset
   168
    }
wenzelm
parents: 77285
diff changeset
   169
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   170
  // global state
77288
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
wenzelm
parents: 77287
diff changeset
   171
  private val _numa_nodes = new NUMA.Nodes(numa_shuffling)
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
wenzelm
parents: 77287
diff changeset
   172
  private var _build_graph = build_context.sessions_structure.build_graph
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
wenzelm
parents: 77287
diff changeset
   173
  private var _build_order = SortedSet.from(_build_graph.keys)(build_context.ordering)
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
wenzelm
parents: 77287
diff changeset
   174
  private var _running = Map.empty[String, Build_Job]
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
wenzelm
parents: 77287
diff changeset
   175
  private var _results = Map.empty[String, Build_Process.Result]
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   176
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   177
  private def remove_pending(name: String): Unit = synchronized {
77288
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
wenzelm
parents: 77287
diff changeset
   178
    _build_graph = _build_graph.del_node(name)
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
wenzelm
parents: 77287
diff changeset
   179
    _build_order = _build_order - name
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   180
  }
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   181
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   182
  private def next_pending(): Option[String] = synchronized {
77296
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   183
    if (_running.size < (max_jobs max 1)) {
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   184
      _build_order.iterator
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   185
        .dropWhile(name => _running.isDefinedAt(name) || !_build_graph.is_minimal(name))
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   186
        .nextOption()
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   187
    }
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   188
    else None
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   189
  }
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   190
77290
12fd873af77c clarified signature: proper scope of synchronized operation;
wenzelm
parents: 77289
diff changeset
   191
  private def next_numa_node(): Option[Int] = synchronized {
12fd873af77c clarified signature: proper scope of synchronized operation;
wenzelm
parents: 77289
diff changeset
   192
    _numa_nodes.next(used =
12fd873af77c clarified signature: proper scope of synchronized operation;
wenzelm
parents: 77289
diff changeset
   193
      Set.from(for { job <- _running.valuesIterator; i <- job.numa_node } yield i))
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   194
  }
77259
61fc2afe4c8b clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents: 77258
diff changeset
   195
77295
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   196
  private def test_running(): Boolean = synchronized { !_build_graph.is_empty }
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   197
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   198
  private def stop_running(): Unit = synchronized { _running.valuesIterator.foreach(_.terminate()) }
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   199
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   200
  private def finished_running(): List[Build_Job.Build_Session] = synchronized {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   201
    List.from(
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   202
      _running.valuesIterator.flatMap {
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   203
        case job: Build_Job.Build_Session if job.is_finished => Some(job)
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   204
        case _ => None
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   205
      })
77296
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   206
  }
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   207
77292
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   208
  private def job_running(name: String, job: Build_Job): Build_Job = synchronized {
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   209
    _running += (name -> job)
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   210
    job
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   211
  }
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   212
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   213
  private def remove_running(name: String): Unit = synchronized {
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   214
    _running -= name
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   215
  }
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   216
77293
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   217
  private def add_result(
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   218
    name: String,
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   219
    current: Boolean,
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   220
    output_heap: SHA1.Shasum,
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   221
    process_result: Process_Result
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   222
  ): Unit = synchronized {
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   223
    _results += (name -> Build_Process.Result(current, output_heap, process_result))
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   224
  }
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   225
77295
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   226
  private def get_results(names: List[String]): List[Build_Process.Result] = synchronized {
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   227
    names.map(_results.apply)
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   228
  }
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   229
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   230
  private def session_finished(session_name: String, process_result: Process_Result): String =
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   231
    "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   232
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   233
  private def session_timing(session_name: String, build_log: Build_Log.Session_Info): String = {
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   234
    val props = build_log.session_timing
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   235
    val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   236
    val timing = Markup.Timing_Properties.get(props)
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   237
    "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   238
  }
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   239
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   240
  private def finish_job(job: Build_Job.Build_Session): Unit = {
77296
eeaa2872320b clarified signature: more explicit synchronized operations;
wenzelm
parents: 77295
diff changeset
   241
    val session_name = job.session_name
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   242
    val process_result = job.join
77294
3f2b1419f598 clarified modules (again);
wenzelm
parents: 77293
diff changeset
   243
    val output_heap = job.finish
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   244
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   245
    val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   246
    val process_result_tail = {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   247
      val tail = job.info.options.int("process_output_tail")
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   248
      process_result.copy(
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   249
        out_lines =
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   250
          "(more details via \"isabelle log -H Error " + session_name + "\")" ::
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   251
          (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   252
    }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   253
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   254
    val build_log =
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   255
      Build_Log.Log_File(session_name, process_result.out_lines).
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   256
        parse_session_info(
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   257
          command_timings = true,
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   258
          theory_timings = true,
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   259
          ml_statistics = true,
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   260
          task_statistics = true)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   261
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   262
    // write log file
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   263
    if (process_result.ok) {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   264
      File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   265
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   266
    else File.write(store.output_log(session_name), terminate_lines(log_lines))
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   267
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   268
    // write database
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   269
    using(store.open_database(session_name, output = true))(db =>
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   270
      store.write_session_info(db, session_name, job.session_sources,
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   271
        build_log =
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   272
          if (process_result.timeout) build_log.error("Timeout") else build_log,
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   273
        build =
77285
f04672649483 clarified signature;
wenzelm
parents: 77284
diff changeset
   274
          Sessions.Build_Info(build_deps.sources_shasum(session_name), job.input_heaps,
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   275
            output_heap, process_result.rc, UUID.random().toString)))
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   276
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   277
    // messages
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   278
    process_result.err_lines.foreach(progress.echo)
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   279
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   280
    if (process_result.ok) {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   281
      if (verbose) progress.echo(session_timing(session_name, build_log))
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   282
      progress.echo(session_finished(session_name, process_result))
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   283
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   284
    else {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   285
      progress.echo(session_name + " FAILED")
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   286
      if (!process_result.interrupted) progress.echo(process_result_tail.out)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   287
    }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   288
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   289
    synchronized {
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   290
      remove_pending(session_name)
77292
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   291
      remove_running(session_name)
77293
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   292
      add_result(session_name, false, output_heap, process_result_tail)
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   293
    }
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   294
  }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   295
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   296
  private def start_job(session_name: String): Unit = {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   297
    val ancestor_results =
77295
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   298
      get_results(
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   299
        build_deps.sessions_structure.build_requirements(List(session_name)).
ab13ac27c74a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77294
diff changeset
   300
          filterNot(_ == session_name))
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   301
    val input_heaps =
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   302
      if (ancestor_results.isEmpty) {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   303
        SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   304
      }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   305
      else SHA1.flat_shasum(ancestor_results.map(_.output_heap))
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   306
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   307
    val do_store = build_heap || build_context.build_heap(session_name)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   308
    val (current, output_heap) = {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   309
      store.try_open_database(session_name) match {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   310
        case Some(db) =>
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   311
          using(db)(store.read_build(_, session_name)) match {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   312
            case Some(build) =>
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   313
              val output_heap = store.find_heap_shasum(session_name)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   314
              val current =
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   315
                !fresh_build &&
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   316
                build.ok &&
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   317
                build.sources == build_deps.sources_shasum(session_name) &&
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   318
                build.input_heaps == input_heaps &&
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   319
                build.output_heap == output_heap &&
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   320
                !(do_store && output_heap.is_empty)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   321
              (current, output_heap)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   322
            case None => (false, SHA1.no_shasum)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   323
          }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   324
        case None => (false, SHA1.no_shasum)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   325
      }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   326
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   327
    val all_current = current && ancestor_results.forall(_.current)
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   328
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   329
    if (all_current) {
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   330
      synchronized {
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   331
        remove_pending(session_name)
77293
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   332
        add_result(session_name, true, output_heap, Process_Result.ok)
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   333
      }
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   334
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   335
    else if (no_build) {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   336
      progress.echo_if(verbose, "Skipping " + session_name + " ...")
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   337
      synchronized {
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   338
        remove_pending(session_name)
77293
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   339
        add_result(session_name, false, output_heap, Process_Result.error)
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   340
      }
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   341
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   342
    else if (ancestor_results.forall(_.ok) && !progress.stopped) {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   343
      progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   344
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   345
      store.clean_output(session_name)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   346
      using(store.open_database(session_name, output = true))(
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   347
        store.init_session_info(_, session_name))
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   348
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   349
      val session_background = build_deps.background(session_name)
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   350
      val resources =
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   351
        new Resources(session_background, log = log,
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   352
          command_timings = build_context(session_name).old_command_timings)
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   353
77291
f7e413e8d269 more robust: first register job, then start job;
wenzelm
parents: 77290
diff changeset
   354
      val job =
f7e413e8d269 more robust: first register job, then start job;
wenzelm
parents: 77290
diff changeset
   355
        synchronized {
f7e413e8d269 more robust: first register job, then start job;
wenzelm
parents: 77290
diff changeset
   356
          val numa_node = next_numa_node()
77292
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   357
          job_running(session_name,
77297
226a880d0423 clarified types: support a variety of Build_Job instances;
wenzelm
parents: 77296
diff changeset
   358
            new Build_Job.Build_Session(progress, session_background, store, do_store,
77292
9cb8fb31e245 clarified signature: more explicit synchronized operations;
wenzelm
parents: 77291
diff changeset
   359
              resources, session_setup, input_heaps, numa_node))
77291
f7e413e8d269 more robust: first register job, then start job;
wenzelm
parents: 77290
diff changeset
   360
        }
f7e413e8d269 more robust: first register job, then start job;
wenzelm
parents: 77290
diff changeset
   361
      job.start()
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   362
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   363
    else {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   364
      progress.echo(session_name + " CANCELLED")
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   365
      synchronized {
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   366
        remove_pending(session_name)
77293
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
wenzelm
parents: 77292
diff changeset
   367
        add_result(session_name, false, output_heap, Process_Result.undefined)
77289
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents: 77288
diff changeset
   368
      }
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   369
    }
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   370
  }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   371
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   372
  private def sleep(): Unit =
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   373
    Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   374
      build_options.seconds("editor_input_delay").sleep()
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   375
    }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   376
77310
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   377
  def run(): Map[String, Process_Result] = {
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   378
    if (test_running()) {
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   379
      while (test_running()) {
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   380
        if (progress.stopped) stop_running()
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   381
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   382
        for (job <- finished_running()) finish_job(job)
77260
58397b40df2b clarified main operations;
wenzelm
parents: 77259
diff changeset
   383
77310
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   384
        next_pending() match {
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   385
          case Some(session_name) => start_job(session_name)
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   386
          case None => sleep()
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   387
        }
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   388
      }
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   389
      synchronized {
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   390
        for ((name, result) <- _results) yield name -> result.process_result
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   391
      }
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   392
    }
77310
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   393
    else {
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   394
      progress.echo_warning("Nothing to build")
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   395
      Map.empty[String, Process_Result]
6754b5eceb12 clarified modules;
wenzelm
parents: 77297
diff changeset
   396
    }
77257
68a7ad1385bc clarified modules;
wenzelm
parents: 77256
diff changeset
   397
  }
77238
02308a0ddf30 clarified modules;
wenzelm
parents:
diff changeset
   398
}