author | wenzelm |
Mon, 23 Nov 2020 15:14:58 +0100 | |
changeset 72692 | 22aeec526ffd |
parent 72683 | b5e6f0d137a7 |
child 72693 | 0201ae367518 |
permissions | -rw-r--r-- |
72662 | 1 |
/* Title: Pure/Tools/build_job.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build job running prover process, with rudimentary PIDE session. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import scala.collection.mutable |
|
11 |
||
12 |
||
13 |
class Build_Job(progress: Progress, |
|
14 |
session_name: String, |
|
15 |
val info: Sessions.Info, |
|
16 |
deps: Sessions.Deps, |
|
17 |
store: Sessions.Store, |
|
18 |
do_store: Boolean, |
|
19 |
presentation: Presentation.Context, |
|
20 |
verbose: Boolean, |
|
21 |
val numa_node: Option[Int], |
|
22 |
command_timings0: List[Properties.T]) |
|
23 |
{ |
|
24 |
val options: Options = NUMA.policy_options(info.options, numa_node) |
|
25 |
||
26 |
private val sessions_structure = deps.sessions_structure |
|
27 |
||
28 |
private val future_result: Future[Process_Result] = |
|
29 |
Future.thread("build", uninterruptible = true) { |
|
30 |
val parent = info.parent.getOrElse("") |
|
31 |
val base = deps(parent) |
|
32 |
||
33 |
val env = |
|
34 |
Isabelle_System.settings() + |
|
35 |
("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) |
|
36 |
||
37 |
val is_pure = Sessions.is_pure(session_name) |
|
38 |
||
39 |
val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil |
|
40 |
||
41 |
val eval_store = |
|
42 |
if (do_store) { |
|
43 |
(if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: |
|
44 |
List("ML_Heap.save_child " + |
|
45 |
ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) |
|
46 |
} |
|
47 |
else Nil |
|
48 |
||
49 |
val resources = new Resources(sessions_structure, base, command_timings = command_timings0) |
|
50 |
val session = |
|
51 |
new Session(options, resources) { |
|
52 |
override val xml_cache: XML.Cache = store.xml_cache |
|
53 |
override val xz_cache: XZ.Cache = store.xz_cache |
|
54 |
} |
|
55 |
||
56 |
object Build_Session_Errors |
|
57 |
{ |
|
58 |
private val promise: Promise[List[String]] = Future.promise |
|
59 |
||
60 |
def result: Exn.Result[List[String]] = promise.join_result |
|
61 |
def cancel: Unit = promise.cancel |
|
62 |
def apply(errs: List[String]) |
|
63 |
{ |
|
64 |
try { promise.fulfill(errs) } |
|
65 |
catch { case _: IllegalStateException => } |
|
66 |
} |
|
67 |
} |
|
68 |
||
69 |
val export_consumer = |
|
70 |
Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) |
|
71 |
||
72 |
val stdout = new StringBuilder(1000) |
|
73 |
val stderr = new StringBuilder(1000) |
|
74 |
val messages = new mutable.ListBuffer[XML.Elem] |
|
75 |
val command_timings = new mutable.ListBuffer[Properties.T] |
|
76 |
val theory_timings = new mutable.ListBuffer[Properties.T] |
|
77 |
val session_timings = new mutable.ListBuffer[Properties.T] |
|
78 |
val runtime_statistics = new mutable.ListBuffer[Properties.T] |
|
79 |
val task_statistics = new mutable.ListBuffer[Properties.T] |
|
80 |
val document_output = new mutable.ListBuffer[String] |
|
81 |
||
82 |
def fun( |
|
83 |
name: String, |
|
84 |
acc: mutable.ListBuffer[Properties.T], |
|
85 |
unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) = |
|
86 |
{ |
|
87 |
name -> ((msg: Prover.Protocol_Output) => |
|
88 |
unapply(msg.properties) match { |
|
89 |
case Some(props) => acc += props; true |
|
90 |
case _ => false |
|
91 |
}) |
|
92 |
} |
|
93 |
||
94 |
session.init_protocol_handler(new Session.Protocol_Handler |
|
95 |
{ |
|
96 |
override def exit() { Build_Session_Errors.cancel } |
|
97 |
||
98 |
private def build_session_finished(msg: Prover.Protocol_Output): Boolean = |
|
99 |
{ |
|
100 |
val (rc, errors) = |
|
101 |
try { |
|
102 |
val (rc, errs) = |
|
103 |
{ |
|
104 |
import XML.Decode._ |
|
105 |
pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) |
|
106 |
} |
|
107 |
val errors = |
|
108 |
for (err <- errs) yield { |
|
109 |
val prt = Protocol_Message.expose_no_reports(err) |
|
110 |
Pretty.string_of(prt, metric = Symbol.Metric) |
|
111 |
} |
|
112 |
(rc, errors) |
|
113 |
} |
|
114 |
catch { case ERROR(err) => (2, List(err)) } |
|
115 |
||
116 |
session.protocol_command("Prover.stop", rc.toString) |
|
117 |
Build_Session_Errors(errors) |
|
118 |
true |
|
119 |
} |
|
120 |
||
121 |
private def loading_theory(msg: Prover.Protocol_Output): Boolean = |
|
122 |
msg.properties match { |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
123 |
case Markup.Loading_Theory(Markup.Name(name)) => |
72662 | 124 |
progress.theory(Progress.Theory(name, session = session_name)) |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
125 |
false |
72662 | 126 |
case _ => false |
127 |
} |
|
128 |
||
129 |
private def export(msg: Prover.Protocol_Output): Boolean = |
|
130 |
msg.properties match { |
|
131 |
case Protocol.Export(args) => |
|
132 |
export_consumer(session_name, args, msg.bytes) |
|
133 |
true |
|
134 |
case _ => false |
|
135 |
} |
|
136 |
||
137 |
private def command_timing(props: Properties.T): Option[Properties.T] = |
|
138 |
for { |
|
139 |
props1 <- Markup.Command_Timing.unapply(props) |
|
140 |
elapsed <- Markup.Elapsed.unapply(props1) |
|
141 |
elapsed_time = Time.seconds(elapsed) |
|
142 |
if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") |
|
143 |
} yield props1.filter(p => Markup.command_timing_properties(p._1)) |
|
144 |
||
145 |
override val functions = |
|
146 |
List( |
|
147 |
Markup.Build_Session_Finished.name -> build_session_finished, |
|
148 |
Markup.Loading_Theory.name -> loading_theory, |
|
149 |
Markup.EXPORT -> export, |
|
150 |
fun(Markup.Command_Timing.name, command_timings, command_timing), |
|
151 |
fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), |
|
152 |
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), |
|
153 |
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) |
|
154 |
}) |
|
155 |
||
156 |
session.runtime_statistics += Session.Consumer("ML_statistics") |
|
157 |
{ |
|
158 |
case Session.Runtime_Statistics(props) => runtime_statistics += props |
|
159 |
} |
|
160 |
||
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
161 |
session.finished_theories += Session.Consumer[Command.State]("finished_theories") |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
162 |
{ |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
163 |
case st => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
164 |
val command = st.command |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
165 |
val theory_name = command.node_name.theory |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
166 |
val args = Protocol.Export.Args(theory_name = theory_name, name = Export.MARKUP) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
167 |
val xml = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
168 |
st.markups(Command.Markup_Index.markup) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
169 |
.to_XML(command.range, command.source, Markup.Elements.full) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
170 |
export_consumer(session_name, args, Bytes(YXML.string_of_body(xml))) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
171 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
172 |
|
72662 | 173 |
session.all_messages += Session.Consumer[Any]("build_session_output") |
174 |
{ |
|
175 |
case msg: Prover.Output => |
|
176 |
val message = msg.message |
|
177 |
if (msg.is_stdout) { |
|
178 |
stdout ++= Symbol.encode(XML.content(message)) |
|
179 |
} |
|
180 |
else if (msg.is_stderr) { |
|
181 |
stderr ++= Symbol.encode(XML.content(message)) |
|
182 |
} |
|
183 |
else if (Protocol.is_exported(message)) { |
|
184 |
messages += message |
|
185 |
} |
|
186 |
else if (msg.is_exit) { |
|
187 |
val err = |
|
188 |
"Prover terminated" + |
|
189 |
(msg.properties match { |
|
190 |
case Markup.Process_Result(result) => ": " + result.print_rc |
|
191 |
case _ => "" |
|
192 |
}) |
|
193 |
Build_Session_Errors(List(err)) |
|
194 |
} |
|
195 |
case _ => |
|
196 |
} |
|
197 |
||
198 |
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) |
|
199 |
||
200 |
val process = |
|
201 |
Isabelle_Process(session, options, sessions_structure, store, |
|
202 |
logic = parent, raw_ml_system = is_pure, |
|
203 |
use_prelude = use_prelude, eval_main = eval_main, |
|
204 |
cwd = info.dir.file, env = env) |
|
205 |
||
206 |
val build_errors = |
|
207 |
Isabelle_Thread.interrupt_handler(_ => process.terminate) { |
|
208 |
Exn.capture { process.await_startup } match { |
|
209 |
case Exn.Res(_) => |
|
210 |
val resources_yxml = resources.init_session_yxml |
|
211 |
val args_yxml = |
|
212 |
YXML.string_of_body( |
|
213 |
{ |
|
214 |
import XML.Encode._ |
|
215 |
pair(string, list(pair(Options.encode, list(pair(string, properties)))))( |
|
216 |
(session_name, info.theories)) |
|
217 |
}) |
|
218 |
session.protocol_command("build_session", resources_yxml, args_yxml) |
|
219 |
Build_Session_Errors.result |
|
220 |
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) |
|
221 |
} |
|
222 |
} |
|
223 |
||
224 |
val process_result = |
|
225 |
Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } |
|
226 |
||
227 |
val export_errors = |
|
228 |
export_consumer.shutdown(close = true).map(Output.error_message_text) |
|
229 |
||
230 |
val document_errors = |
|
231 |
try { |
|
72675 | 232 |
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) |
233 |
{ |
|
72673
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
234 |
val document_progress = |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
235 |
new Progress { |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
236 |
override def echo(msg: String): Unit = |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
237 |
document_output.synchronized { document_output += msg } |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
238 |
override def echo_document(msg: String): Unit = |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
239 |
progress.echo_document(msg) |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
240 |
} |
72662 | 241 |
val documents = |
72683 | 242 |
using(store.open_database_context(deps.sessions_structure))(db_context => |
243 |
Presentation.build_documents(session_name, deps, db_context, |
|
244 |
output_sources = info.document_output, |
|
245 |
output_pdf = info.document_output, |
|
246 |
progress = document_progress, |
|
247 |
verbose = verbose, |
|
248 |
verbose_latex = true)) |
|
72673
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
249 |
using(store.open_database(session_name, output = true))(db => |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
250 |
for ((doc, pdf) <- documents) { |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
251 |
db.transaction { |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
252 |
Presentation.write_document(db, session_name, doc, pdf) |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
253 |
} |
8ff7a0e394f9
clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents:
72663
diff
changeset
|
254 |
}) |
72662 | 255 |
} |
256 |
Nil |
|
257 |
} |
|
258 |
catch { case Exn.Interrupt.ERROR(msg) => List(msg) } |
|
259 |
||
260 |
val result = |
|
261 |
{ |
|
262 |
val more_output = |
|
263 |
Library.trim_line(stdout.toString) :: |
|
264 |
messages.toList.map(message => |
|
265 |
Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) ::: |
|
266 |
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: |
|
267 |
theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: |
|
268 |
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: |
|
269 |
runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: |
|
270 |
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: |
|
271 |
document_output.toList |
|
272 |
||
273 |
val more_errors = |
|
274 |
Library.trim_line(stderr.toString) :: export_errors ::: document_errors |
|
275 |
||
276 |
process_result.output(more_output).errors(more_errors) |
|
277 |
} |
|
278 |
||
279 |
build_errors match { |
|
280 |
case Exn.Res(build_errs) => |
|
281 |
val errs = build_errs ::: document_errors |
|
282 |
if (errs.isEmpty) result |
|
283 |
else { |
|
284 |
result.error_rc.output( |
|
285 |
errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: |
|
286 |
errs.map(Protocol.Error_Message_Marker.apply)) |
|
287 |
} |
|
288 |
case Exn.Exn(Exn.Interrupt()) => |
|
289 |
if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result |
|
290 |
case Exn.Exn(exn) => throw exn |
|
291 |
} |
|
292 |
} |
|
293 |
||
294 |
def terminate: Unit = future_result.cancel |
|
295 |
def is_finished: Boolean = future_result.is_finished |
|
296 |
||
297 |
private val timeout_request: Option[Event_Timer.Request] = |
|
298 |
{ |
|
299 |
if (info.timeout > Time.zero) |
|
300 |
Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) |
|
301 |
else None |
|
302 |
} |
|
303 |
||
304 |
def join: (Process_Result, Option[String]) = |
|
305 |
{ |
|
306 |
val result1 = future_result.join |
|
307 |
||
308 |
val was_timeout = |
|
309 |
timeout_request match { |
|
310 |
case None => false |
|
311 |
case Some(request) => !request.cancel |
|
312 |
} |
|
313 |
||
314 |
val result2 = |
|
315 |
if (result1.interrupted) { |
|
316 |
if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout |
|
317 |
else result1.error(Output.error_message_text("Interrupt")) |
|
318 |
} |
|
319 |
else result1 |
|
320 |
||
321 |
val heap_digest = |
|
322 |
if (result2.ok && do_store && store.output_heap(session_name).is_file) |
|
323 |
Some(Sessions.write_heap_digest(store.output_heap(session_name))) |
|
324 |
else None |
|
325 |
||
326 |
(result2, heap_digest) |
|
327 |
} |
|
328 |
} |