author | wenzelm |
Mon, 13 Feb 2023 11:35:46 +0100 | |
changeset 77289 | c7d893278aec |
parent 77288 | e9f1fcb9b358 |
child 77290 | 12fd873af77c |
permissions | -rw-r--r-- |
77238 | 1 |
/* Title: Pure/Tools/build_process.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build process for sessions, with build database, optional heap, and |
|
5 |
optional presentation. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
77246 | 11 |
import scala.math.Ordering |
77257 | 12 |
import scala.collection.immutable.SortedSet |
13 |
import scala.annotation.tailrec |
|
77246 | 14 |
|
15 |
||
77238 | 16 |
object Build_Process { |
77244 | 17 |
/* static information */ |
77238 | 18 |
|
77244 | 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 | 22 |
|
77246 | 23 |
def apply( |
77239 | 24 |
session: String, |
77249
f3f1b7ad1d0d
clarified data structure: more direct access to timeout;
wenzelm
parents:
77248
diff
changeset
|
25 |
timeout: Time, |
77239 | 26 |
store: Sessions.Store, |
27 |
progress: Progress = new Progress |
|
77244 | 28 |
): Session_Context = { |
77239 | 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 | 31 |
case Some(db) => |
32 |
def ignore_error(msg: String) = { |
|
33 |
progress.echo_warning("Ignoring bad database " + db + |
|
77239 | 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 | 36 |
} |
37 |
try { |
|
77239 | 38 |
val command_timings = store.read_command_timings(db, session) |
39 |
val elapsed = |
|
40 |
store.read_session_timing(db, session) match { |
|
41 |
case Markup.Elapsed(s) => Time.seconds(s) |
|
42 |
case _ => Time.zero |
|
77238 | 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 | 45 |
} |
46 |
catch { |
|
47 |
case ERROR(msg) => ignore_error(msg) |
|
48 |
case exn: java.lang.Error => ignore_error(Exn.message(exn)) |
|
49 |
case _: XML.Error => ignore_error("XML.Error") |
|
50 |
} |
|
51 |
finally { db.close() } |
|
52 |
} |
|
53 |
} |
|
54 |
} |
|
77239 | 55 |
|
77244 | 56 |
final class Session_Context( |
77239 | 57 |
val session: String, |
77249
f3f1b7ad1d0d
clarified data structure: more direct access to timeout;
wenzelm
parents:
77248
diff
changeset
|
58 |
val timeout: Time, |
77244 | 59 |
val old_time: Time, |
60 |
val old_command_timings: List[Properties.T] |
|
77239 | 61 |
) { |
77244 | 62 |
def is_empty: Boolean = old_time.is_zero && old_command_timings.isEmpty |
77240 | 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 | 65 |
} |
77246 | 66 |
|
67 |
object Context { |
|
68 |
def apply( |
|
69 |
store: Sessions.Store, |
|
77257 | 70 |
deps: Sessions.Deps, |
77246 | 71 |
progress: Progress = new Progress |
72 |
): Context = { |
|
77257 | 73 |
val sessions_structure = deps.sessions_structure |
77247 | 74 |
val build_graph = sessions_structure.build_graph |
75 |
||
77246 | 76 |
val sessions = |
77 |
Map.from( |
|
77247 | 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 | 83 |
|
77248 | 84 |
val sessions_time = { |
85 |
val maximals = build_graph.maximals.toSet |
|
86 |
def descendants_time(name: String): Double = { |
|
87 |
if (maximals.contains(name)) sessions(name).old_time.seconds |
|
88 |
else { |
|
89 |
val descendants = build_graph.all_succs(List(name)).toSet |
|
90 |
val g = build_graph.restrict(descendants) |
|
91 |
(0.0 :: g.maximals.flatMap { desc => |
|
92 |
val ps = g.all_preds(List(desc)) |
|
93 |
if (ps.exists(p => !sessions.isDefinedAt(p))) None |
|
94 |
else Some(ps.map(p => sessions(p).old_time.seconds).sum) |
|
95 |
}).max |
|
96 |
} |
|
77247 | 97 |
} |
77248 | 98 |
Map.from( |
99 |
for (name <- sessions.keysIterator) |
|
100 |
yield name -> descendants_time(name)).withDefaultValue(0.0) |
|
77247 | 101 |
} |
102 |
||
77246 | 103 |
val ordering = |
104 |
new Ordering[String] { |
|
105 |
def compare(name1: String, name2: String): Int = |
|
77248 | 106 |
sessions_time(name2) compare sessions_time(name1) match { |
77246 | 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 | 109 |
case 0 => name1 compare name2 |
110 |
case ord => ord |
|
111 |
} |
|
112 |
case ord => ord |
|
113 |
} |
|
114 |
} |
|
115 |
||
77257 | 116 |
new Context(store, deps, sessions, ordering, progress) |
77246 | 117 |
} |
118 |
} |
|
119 |
||
120 |
final class Context private( |
|
77257 | 121 |
val store: Sessions.Store, |
122 |
val deps: Sessions.Deps, |
|
77246 | 123 |
sessions: Map[String, Session_Context], |
77257 | 124 |
val ordering: Ordering[String], |
125 |
val progress: Progress |
|
77246 | 126 |
) { |
77257 | 127 |
def sessions_structure: Sessions.Structure = deps.sessions_structure |
128 |
||
77246 | 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 | 132 |
def build_heap(session: String): Boolean = |
133 |
Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session) |
|
77246 | 134 |
} |
77257 | 135 |
|
136 |
||
137 |
/* main */ |
|
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 | 163 |
private val log = |
164 |
build_options.string("system_log") match { |
|
165 |
case "" => No_Logger |
|
166 |
case "-" => Logger.make(progress) |
|
167 |
case log_file => Logger.make(Some(Path.explode(log_file))) |
|
168 |
} |
|
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 { |
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
183 |
_build_order.iterator |
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
184 |
.dropWhile(name => _running.isDefinedAt(name) || !_build_graph.is_minimal(name)) |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
185 |
.nextOption() |
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
186 |
} |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
187 |
|
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
188 |
private def used_node(i: Int): Boolean = synchronized { |
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
189 |
_running.valuesIterator.exists(job => job.numa_node.isDefined && job.numa_node.get == i) |
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
190 |
} |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
191 |
|
77257 | 192 |
private def session_finished(session_name: String, process_result: Process_Result): String = |
193 |
"Finished " + session_name + " (" + process_result.timing.message_resources + ")" |
|
194 |
||
195 |
private def session_timing(session_name: String, build_log: Build_Log.Session_Info): String = { |
|
196 |
val props = build_log.session_timing |
|
197 |
val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 |
|
198 |
val timing = Markup.Timing_Properties.get(props) |
|
199 |
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")" |
|
200 |
} |
|
201 |
||
77285 | 202 |
private def finish_job(session_name: String, job: Build_Job): Unit = { |
77260 | 203 |
val process_result = job.join |
77257 | 204 |
|
77260 | 205 |
val output_heap = |
206 |
if (process_result.ok && job.do_store && store.output_heap(session_name).is_file) { |
|
207 |
SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) |
|
208 |
} |
|
209 |
else SHA1.no_shasum |
|
77257 | 210 |
|
77260 | 211 |
val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) |
212 |
val process_result_tail = { |
|
213 |
val tail = job.info.options.int("process_output_tail") |
|
214 |
process_result.copy( |
|
215 |
out_lines = |
|
216 |
"(more details via \"isabelle log -H Error " + session_name + "\")" :: |
|
217 |
(if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) |
|
218 |
} |
|
77257 | 219 |
|
77260 | 220 |
val build_log = |
221 |
Build_Log.Log_File(session_name, process_result.out_lines). |
|
222 |
parse_session_info( |
|
223 |
command_timings = true, |
|
224 |
theory_timings = true, |
|
225 |
ml_statistics = true, |
|
226 |
task_statistics = true) |
|
227 |
||
228 |
// write log file |
|
229 |
if (process_result.ok) { |
|
230 |
File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) |
|
231 |
} |
|
232 |
else File.write(store.output_log(session_name), terminate_lines(log_lines)) |
|
77257 | 233 |
|
77260 | 234 |
// write database |
235 |
using(store.open_database(session_name, output = true))(db => |
|
236 |
store.write_session_info(db, session_name, job.session_sources, |
|
237 |
build_log = |
|
238 |
if (process_result.timeout) build_log.error("Timeout") else build_log, |
|
239 |
build = |
|
77285 | 240 |
Sessions.Build_Info(build_deps.sources_shasum(session_name), job.input_heaps, |
77260 | 241 |
output_heap, process_result.rc, UUID.random().toString))) |
77257 | 242 |
|
77260 | 243 |
// messages |
244 |
process_result.err_lines.foreach(progress.echo) |
|
77257 | 245 |
|
77260 | 246 |
if (process_result.ok) { |
247 |
if (verbose) progress.echo(session_timing(session_name, build_log)) |
|
248 |
progress.echo(session_finished(session_name, process_result)) |
|
249 |
} |
|
250 |
else { |
|
251 |
progress.echo(session_name + " FAILED") |
|
252 |
if (!process_result.interrupted) progress.echo(process_result_tail.out) |
|
253 |
} |
|
77257 | 254 |
|
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
255 |
synchronized { |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
256 |
remove_pending(session_name) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
257 |
_running -= session_name |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
258 |
_results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail)) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
259 |
} |
77260 | 260 |
} |
77257 | 261 |
|
77260 | 262 |
private def start_job(session_name: String): Unit = { |
263 |
val ancestor_results = |
|
264 |
build_deps.sessions_structure.build_requirements(List(session_name)). |
|
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
265 |
filterNot(_ == session_name).map(_results(_)) |
77260 | 266 |
val input_heaps = |
267 |
if (ancestor_results.isEmpty) { |
|
268 |
SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) |
|
269 |
} |
|
270 |
else SHA1.flat_shasum(ancestor_results.map(_.output_heap)) |
|
77257 | 271 |
|
77260 | 272 |
val do_store = build_heap || build_context.build_heap(session_name) |
273 |
val (current, output_heap) = { |
|
274 |
store.try_open_database(session_name) match { |
|
275 |
case Some(db) => |
|
276 |
using(db)(store.read_build(_, session_name)) match { |
|
277 |
case Some(build) => |
|
278 |
val output_heap = store.find_heap_shasum(session_name) |
|
279 |
val current = |
|
280 |
!fresh_build && |
|
281 |
build.ok && |
|
282 |
build.sources == build_deps.sources_shasum(session_name) && |
|
283 |
build.input_heaps == input_heaps && |
|
284 |
build.output_heap == output_heap && |
|
285 |
!(do_store && output_heap.is_empty) |
|
286 |
(current, output_heap) |
|
287 |
case None => (false, SHA1.no_shasum) |
|
288 |
} |
|
289 |
case None => (false, SHA1.no_shasum) |
|
290 |
} |
|
291 |
} |
|
292 |
val all_current = current && ancestor_results.forall(_.current) |
|
77257 | 293 |
|
77260 | 294 |
if (all_current) { |
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
295 |
synchronized { |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
296 |
remove_pending(session_name) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
297 |
_results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok)) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
298 |
} |
77260 | 299 |
} |
300 |
else if (no_build) { |
|
301 |
progress.echo_if(verbose, "Skipping " + session_name + " ...") |
|
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
302 |
synchronized { |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
303 |
remove_pending(session_name) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
304 |
_results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error)) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
305 |
} |
77260 | 306 |
} |
307 |
else if (ancestor_results.forall(_.ok) && !progress.stopped) { |
|
308 |
progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") |
|
309 |
||
310 |
store.clean_output(session_name) |
|
311 |
using(store.open_database(session_name, output = true))( |
|
312 |
store.init_session_info(_, session_name)) |
|
77257 | 313 |
|
77260 | 314 |
val session_background = build_deps.background(session_name) |
315 |
val resources = |
|
316 |
new Resources(session_background, log = log, |
|
317 |
command_timings = build_context(session_name).old_command_timings) |
|
77257 | 318 |
|
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
319 |
synchronized { |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
320 |
val numa_node = _numa_nodes.next(used_node) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
321 |
val job = |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
322 |
new Build_Job(progress, session_background, store, do_store, |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
323 |
resources, session_setup, input_heaps, numa_node) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
324 |
_running += (session_name -> job) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
325 |
} |
77260 | 326 |
} |
327 |
else { |
|
328 |
progress.echo(session_name + " CANCELLED") |
|
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
329 |
synchronized { |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
330 |
remove_pending(session_name) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
331 |
_results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined)) |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
332 |
} |
77260 | 333 |
} |
334 |
} |
|
77257 | 335 |
|
77260 | 336 |
private def sleep(): Unit = |
337 |
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { |
|
338 |
build_options.seconds("editor_input_delay").sleep() |
|
339 |
} |
|
77257 | 340 |
|
77260 | 341 |
def run(): Map[String, Build_Process.Result] = { |
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
342 |
while (synchronized { !_build_graph.is_empty }) { |
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
343 |
if (progress.stopped) synchronized { _running.valuesIterator.foreach(_.terminate()) } |
77260 | 344 |
|
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
345 |
synchronized { _running } .find({ case (_, job) => job.is_finished }) match { |
77285 | 346 |
case Some((session_name, job)) => finish_job(session_name, job) |
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
347 |
case None if synchronized { _running.size } < (max_jobs max 1) => |
77260 | 348 |
next_pending() match { |
349 |
case Some(session_name) => start_job(session_name) |
|
350 |
case None => sleep() |
|
351 |
} |
|
352 |
case None => sleep() |
|
77257 | 353 |
} |
354 |
} |
|
355 |
||
77289
c7d893278aec
proper synchronized access to mutable state, to support concurrency eventually;
wenzelm
parents:
77288
diff
changeset
|
356 |
synchronized { _results } |
77257 | 357 |
} |
77238 | 358 |
} |