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