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