author | wenzelm |
Mon, 13 Feb 2023 11:25:01 +0100 | |
changeset 77288 | e9f1fcb9b358 |
parent 77287 | d060545f01a2 |
child 77289 | c7d893278aec |
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 |
|
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
177 |
private def remove_pending(name: String): Unit = { |
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 |
|
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
182 |
private def next_pending(): Option[String] = |
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() |
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
186 |
|
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
187 |
private def used_node(i: Int): Boolean = |
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
188 |
_running.valuesIterator.exists(job => job.numa_node.isDefined && job.numa_node.get == i) |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
189 |
|
77257 | 190 |
private def session_finished(session_name: String, process_result: Process_Result): String = |
191 |
"Finished " + session_name + " (" + process_result.timing.message_resources + ")" |
|
192 |
||
193 |
private def session_timing(session_name: String, build_log: Build_Log.Session_Info): String = { |
|
194 |
val props = build_log.session_timing |
|
195 |
val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 |
|
196 |
val timing = Markup.Timing_Properties.get(props) |
|
197 |
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")" |
|
198 |
} |
|
199 |
||
77285 | 200 |
private def finish_job(session_name: String, job: Build_Job): Unit = { |
77260 | 201 |
val process_result = job.join |
77257 | 202 |
|
77260 | 203 |
val output_heap = |
204 |
if (process_result.ok && job.do_store && store.output_heap(session_name).is_file) { |
|
205 |
SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) |
|
206 |
} |
|
207 |
else SHA1.no_shasum |
|
77257 | 208 |
|
77260 | 209 |
val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) |
210 |
val process_result_tail = { |
|
211 |
val tail = job.info.options.int("process_output_tail") |
|
212 |
process_result.copy( |
|
213 |
out_lines = |
|
214 |
"(more details via \"isabelle log -H Error " + session_name + "\")" :: |
|
215 |
(if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) |
|
216 |
} |
|
77257 | 217 |
|
77260 | 218 |
val build_log = |
219 |
Build_Log.Log_File(session_name, process_result.out_lines). |
|
220 |
parse_session_info( |
|
221 |
command_timings = true, |
|
222 |
theory_timings = true, |
|
223 |
ml_statistics = true, |
|
224 |
task_statistics = true) |
|
225 |
||
226 |
// write log file |
|
227 |
if (process_result.ok) { |
|
228 |
File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) |
|
229 |
} |
|
230 |
else File.write(store.output_log(session_name), terminate_lines(log_lines)) |
|
77257 | 231 |
|
77260 | 232 |
// write database |
233 |
using(store.open_database(session_name, output = true))(db => |
|
234 |
store.write_session_info(db, session_name, job.session_sources, |
|
235 |
build_log = |
|
236 |
if (process_result.timeout) build_log.error("Timeout") else build_log, |
|
237 |
build = |
|
77285 | 238 |
Sessions.Build_Info(build_deps.sources_shasum(session_name), job.input_heaps, |
77260 | 239 |
output_heap, process_result.rc, UUID.random().toString))) |
77257 | 240 |
|
77260 | 241 |
// messages |
242 |
process_result.err_lines.foreach(progress.echo) |
|
77257 | 243 |
|
77260 | 244 |
if (process_result.ok) { |
245 |
if (verbose) progress.echo(session_timing(session_name, build_log)) |
|
246 |
progress.echo(session_finished(session_name, process_result)) |
|
247 |
} |
|
248 |
else { |
|
249 |
progress.echo(session_name + " FAILED") |
|
250 |
if (!process_result.interrupted) progress.echo(process_result_tail.out) |
|
251 |
} |
|
77257 | 252 |
|
77260 | 253 |
remove_pending(session_name) |
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
254 |
_running -= session_name |
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
255 |
_results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail)) |
77260 | 256 |
} |
77257 | 257 |
|
77260 | 258 |
private def start_job(session_name: String): Unit = { |
259 |
val ancestor_results = |
|
260 |
build_deps.sessions_structure.build_requirements(List(session_name)). |
|
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
261 |
filterNot(_ == session_name).map(_results(_)) |
77260 | 262 |
val input_heaps = |
263 |
if (ancestor_results.isEmpty) { |
|
264 |
SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) |
|
265 |
} |
|
266 |
else SHA1.flat_shasum(ancestor_results.map(_.output_heap)) |
|
77257 | 267 |
|
77260 | 268 |
val do_store = build_heap || build_context.build_heap(session_name) |
269 |
val (current, output_heap) = { |
|
270 |
store.try_open_database(session_name) match { |
|
271 |
case Some(db) => |
|
272 |
using(db)(store.read_build(_, session_name)) match { |
|
273 |
case Some(build) => |
|
274 |
val output_heap = store.find_heap_shasum(session_name) |
|
275 |
val current = |
|
276 |
!fresh_build && |
|
277 |
build.ok && |
|
278 |
build.sources == build_deps.sources_shasum(session_name) && |
|
279 |
build.input_heaps == input_heaps && |
|
280 |
build.output_heap == output_heap && |
|
281 |
!(do_store && output_heap.is_empty) |
|
282 |
(current, output_heap) |
|
283 |
case None => (false, SHA1.no_shasum) |
|
284 |
} |
|
285 |
case None => (false, SHA1.no_shasum) |
|
286 |
} |
|
287 |
} |
|
288 |
val all_current = current && ancestor_results.forall(_.current) |
|
77257 | 289 |
|
77260 | 290 |
if (all_current) { |
291 |
remove_pending(session_name) |
|
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
292 |
_results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok)) |
77260 | 293 |
} |
294 |
else if (no_build) { |
|
295 |
progress.echo_if(verbose, "Skipping " + session_name + " ...") |
|
296 |
remove_pending(session_name) |
|
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
297 |
_results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error)) |
77260 | 298 |
} |
299 |
else if (ancestor_results.forall(_.ok) && !progress.stopped) { |
|
300 |
progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") |
|
301 |
||
302 |
store.clean_output(session_name) |
|
303 |
using(store.open_database(session_name, output = true))( |
|
304 |
store.init_session_info(_, session_name)) |
|
77257 | 305 |
|
77260 | 306 |
val session_background = build_deps.background(session_name) |
307 |
val resources = |
|
308 |
new Resources(session_background, log = log, |
|
309 |
command_timings = build_context(session_name).old_command_timings) |
|
77257 | 310 |
|
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
311 |
val numa_node = _numa_nodes.next(used_node) |
77260 | 312 |
val job = |
313 |
new Build_Job(progress, session_background, store, do_store, |
|
77285 | 314 |
resources, session_setup, input_heaps, numa_node) |
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
315 |
_running += (session_name -> job) |
77260 | 316 |
} |
317 |
else { |
|
318 |
progress.echo(session_name + " CANCELLED") |
|
319 |
remove_pending(session_name) |
|
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
320 |
_results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined)) |
77260 | 321 |
} |
322 |
} |
|
77257 | 323 |
|
77260 | 324 |
private def sleep(): Unit = |
325 |
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { |
|
326 |
build_options.seconds("editor_input_delay").sleep() |
|
327 |
} |
|
77257 | 328 |
|
77260 | 329 |
def run(): Map[String, Build_Process.Result] = { |
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
330 |
while (!_build_graph.is_empty) { |
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
331 |
if (progress.stopped) _running.valuesIterator.foreach(_.terminate()) |
77260 | 332 |
|
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
333 |
_running.find({ case (_, job) => job.is_finished }) match { |
77285 | 334 |
case Some((session_name, job)) => finish_job(session_name, job) |
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
335 |
case None if _running.size < (max_jobs max 1) => |
77260 | 336 |
next_pending() match { |
337 |
case Some(session_name) => start_job(session_name) |
|
338 |
case None => sleep() |
|
339 |
} |
|
340 |
case None => sleep() |
|
77257 | 341 |
} |
342 |
} |
|
343 |
||
77288
e9f1fcb9b358
tuned signature: explicit marker for mutable global state;
wenzelm
parents:
77287
diff
changeset
|
344 |
_results |
77257 | 345 |
} |
77238 | 346 |
} |