146 else None |
146 else None |
147 } |
147 } |
148 } |
148 } |
149 |
149 |
150 |
150 |
151 /* PIDE protocol handler */ |
|
152 |
|
153 /* job: running prover process */ |
|
154 |
|
155 private class Job(progress: Progress, |
|
156 session_name: String, |
|
157 val info: Sessions.Info, |
|
158 deps: Sessions.Deps, |
|
159 store: Sessions.Store, |
|
160 do_store: Boolean, |
|
161 presentation: Presentation.Context, |
|
162 verbose: Boolean, |
|
163 val numa_node: Option[Int], |
|
164 command_timings0: List[Properties.T]) |
|
165 { |
|
166 val options: Options = NUMA.policy_options(info.options, numa_node) |
|
167 |
|
168 private val sessions_structure = deps.sessions_structure |
|
169 |
|
170 private val future_result: Future[Process_Result] = |
|
171 Future.thread("build", uninterruptible = true) { |
|
172 val parent = info.parent.getOrElse("") |
|
173 val base = deps(parent) |
|
174 |
|
175 val env = |
|
176 Isabelle_System.settings() + |
|
177 ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) |
|
178 |
|
179 val is_pure = Sessions.is_pure(session_name) |
|
180 |
|
181 val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil |
|
182 |
|
183 val eval_store = |
|
184 if (do_store) { |
|
185 (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: |
|
186 List("ML_Heap.save_child " + |
|
187 ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) |
|
188 } |
|
189 else Nil |
|
190 |
|
191 val resources = new Resources(sessions_structure, base, command_timings = command_timings0) |
|
192 val session = |
|
193 new Session(options, resources) { |
|
194 override val xml_cache: XML.Cache = store.xml_cache |
|
195 override val xz_cache: XZ.Cache = store.xz_cache |
|
196 } |
|
197 |
|
198 object Build_Session_Errors |
|
199 { |
|
200 private val promise: Promise[List[String]] = Future.promise |
|
201 |
|
202 def result: Exn.Result[List[String]] = promise.join_result |
|
203 def cancel: Unit = promise.cancel |
|
204 def apply(errs: List[String]) |
|
205 { |
|
206 try { promise.fulfill(errs) } |
|
207 catch { case _: IllegalStateException => } |
|
208 } |
|
209 } |
|
210 |
|
211 val export_consumer = |
|
212 Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) |
|
213 |
|
214 val stdout = new StringBuilder(1000) |
|
215 val stderr = new StringBuilder(1000) |
|
216 val messages = new mutable.ListBuffer[XML.Elem] |
|
217 val command_timings = new mutable.ListBuffer[Properties.T] |
|
218 val theory_timings = new mutable.ListBuffer[Properties.T] |
|
219 val session_timings = new mutable.ListBuffer[Properties.T] |
|
220 val runtime_statistics = new mutable.ListBuffer[Properties.T] |
|
221 val task_statistics = new mutable.ListBuffer[Properties.T] |
|
222 val document_output = new mutable.ListBuffer[String] |
|
223 |
|
224 def fun( |
|
225 name: String, |
|
226 acc: mutable.ListBuffer[Properties.T], |
|
227 unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) = |
|
228 { |
|
229 name -> ((msg: Prover.Protocol_Output) => |
|
230 unapply(msg.properties) match { |
|
231 case Some(props) => acc += props; true |
|
232 case _ => false |
|
233 }) |
|
234 } |
|
235 |
|
236 session.init_protocol_handler(new Session.Protocol_Handler |
|
237 { |
|
238 override def exit() { Build_Session_Errors.cancel } |
|
239 |
|
240 private def build_session_finished(msg: Prover.Protocol_Output): Boolean = |
|
241 { |
|
242 val (rc, errors) = |
|
243 try { |
|
244 val (rc, errs) = |
|
245 { |
|
246 import XML.Decode._ |
|
247 pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) |
|
248 } |
|
249 val errors = |
|
250 for (err <- errs) yield { |
|
251 val prt = Protocol_Message.expose_no_reports(err) |
|
252 Pretty.string_of(prt, metric = Symbol.Metric) |
|
253 } |
|
254 (rc, errors) |
|
255 } |
|
256 catch { case ERROR(err) => (2, List(err)) } |
|
257 |
|
258 session.protocol_command("Prover.stop", rc.toString) |
|
259 Build_Session_Errors(errors) |
|
260 true |
|
261 } |
|
262 |
|
263 private def loading_theory(msg: Prover.Protocol_Output): Boolean = |
|
264 msg.properties match { |
|
265 case Markup.Loading_Theory(name) => |
|
266 progress.theory(Progress.Theory(name, session = session_name)) |
|
267 true |
|
268 case _ => false |
|
269 } |
|
270 |
|
271 private def export(msg: Prover.Protocol_Output): Boolean = |
|
272 msg.properties match { |
|
273 case Protocol.Export(args) => |
|
274 export_consumer(session_name, args, msg.bytes) |
|
275 true |
|
276 case _ => false |
|
277 } |
|
278 |
|
279 private def command_timing(props: Properties.T): Option[Properties.T] = |
|
280 for { |
|
281 props1 <- Markup.Command_Timing.unapply(props) |
|
282 elapsed <- Markup.Elapsed.unapply(props1) |
|
283 elapsed_time = Time.seconds(elapsed) |
|
284 if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") |
|
285 } yield props1.filter(p => Markup.command_timing_properties(p._1)) |
|
286 |
|
287 override val functions = |
|
288 List( |
|
289 Markup.Build_Session_Finished.name -> build_session_finished, |
|
290 Markup.Loading_Theory.name -> loading_theory, |
|
291 Markup.EXPORT -> export, |
|
292 fun(Markup.Command_Timing.name, command_timings, command_timing), |
|
293 fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), |
|
294 fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), |
|
295 fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) |
|
296 }) |
|
297 |
|
298 session.runtime_statistics += Session.Consumer("ML_statistics") |
|
299 { |
|
300 case Session.Runtime_Statistics(props) => runtime_statistics += props |
|
301 } |
|
302 |
|
303 session.all_messages += Session.Consumer[Any]("build_session_output") |
|
304 { |
|
305 case msg: Prover.Output => |
|
306 val message = msg.message |
|
307 if (msg.is_stdout) { |
|
308 stdout ++= Symbol.encode(XML.content(message)) |
|
309 } |
|
310 else if (msg.is_stderr) { |
|
311 stderr ++= Symbol.encode(XML.content(message)) |
|
312 } |
|
313 else if (Protocol.is_exported(message)) { |
|
314 messages += message |
|
315 } |
|
316 else if (msg.is_exit) { |
|
317 val err = |
|
318 "Prover terminated" + |
|
319 (msg.properties match { |
|
320 case Markup.Process_Result(result) => ": " + result.print_rc |
|
321 case _ => "" |
|
322 }) |
|
323 Build_Session_Errors(List(err)) |
|
324 } |
|
325 case _ => |
|
326 } |
|
327 |
|
328 val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) |
|
329 |
|
330 val process = |
|
331 Isabelle_Process(session, options, sessions_structure, store, |
|
332 logic = parent, raw_ml_system = is_pure, |
|
333 use_prelude = use_prelude, eval_main = eval_main, |
|
334 cwd = info.dir.file, env = env) |
|
335 |
|
336 val build_errors = |
|
337 Isabelle_Thread.interrupt_handler(_ => process.terminate) { |
|
338 Exn.capture { process.await_startup } match { |
|
339 case Exn.Res(_) => |
|
340 val resources_yxml = resources.init_session_yxml |
|
341 val args_yxml = |
|
342 YXML.string_of_body( |
|
343 { |
|
344 import XML.Encode._ |
|
345 pair(string, list(pair(Options.encode, list(pair(string, properties)))))( |
|
346 (session_name, info.theories)) |
|
347 }) |
|
348 session.protocol_command("build_session", resources_yxml, args_yxml) |
|
349 Build_Session_Errors.result |
|
350 case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) |
|
351 } |
|
352 } |
|
353 |
|
354 val process_result = |
|
355 Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } |
|
356 |
|
357 val export_errors = |
|
358 export_consumer.shutdown(close = true).map(Output.error_message_text) |
|
359 |
|
360 val document_errors = |
|
361 try { |
|
362 if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) { |
|
363 val documents = |
|
364 if (info.documents.isEmpty) Nil |
|
365 else { |
|
366 val document_progress = |
|
367 new Progress { |
|
368 override def echo(msg: String): Unit = |
|
369 document_output.synchronized { document_output += msg } |
|
370 override def echo_document(path: Path): Unit = |
|
371 progress.echo_document(path) |
|
372 } |
|
373 val documents = |
|
374 Presentation.build_documents(session_name, deps, store, verbose = verbose, |
|
375 verbose_latex = true, progress = document_progress) |
|
376 using(store.open_database(session_name, output = true))(db => |
|
377 for ((doc, pdf) <- documents) { |
|
378 db.transaction { |
|
379 Presentation.write_document(db, session_name, doc, pdf) |
|
380 } |
|
381 }) |
|
382 documents |
|
383 } |
|
384 if (presentation.enabled(info)) { |
|
385 val dir = Presentation.session_html(session_name, deps, store, presentation) |
|
386 for ((doc, pdf) <- documents) Bytes.write(dir + doc.path.pdf, pdf) |
|
387 if (verbose) progress.echo("Browser info at " + dir.absolute) |
|
388 } |
|
389 } |
|
390 Nil |
|
391 } |
|
392 catch { case Exn.Interrupt.ERROR(msg) => List(msg) } |
|
393 |
|
394 val result = |
|
395 { |
|
396 val more_output = |
|
397 Library.trim_line(stdout.toString) :: |
|
398 messages.toList.map(message => |
|
399 Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) ::: |
|
400 command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: |
|
401 theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: |
|
402 session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: |
|
403 runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: |
|
404 task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: |
|
405 document_output.toList |
|
406 |
|
407 val more_errors = |
|
408 Library.trim_line(stderr.toString) :: export_errors ::: document_errors |
|
409 |
|
410 process_result.output(more_output).errors(more_errors) |
|
411 } |
|
412 |
|
413 build_errors match { |
|
414 case Exn.Res(build_errs) => |
|
415 val errs = build_errs ::: document_errors |
|
416 if (errs.isEmpty) result |
|
417 else { |
|
418 result.error_rc.output( |
|
419 errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: |
|
420 errs.map(Protocol.Error_Message_Marker.apply)) |
|
421 } |
|
422 case Exn.Exn(Exn.Interrupt()) => |
|
423 if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result |
|
424 case Exn.Exn(exn) => throw exn |
|
425 } |
|
426 } |
|
427 |
|
428 def terminate: Unit = future_result.cancel |
|
429 def is_finished: Boolean = future_result.is_finished |
|
430 |
|
431 private val timeout_request: Option[Event_Timer.Request] = |
|
432 { |
|
433 if (info.timeout > Time.zero) |
|
434 Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) |
|
435 else None |
|
436 } |
|
437 |
|
438 def join: (Process_Result, Option[String]) = |
|
439 { |
|
440 val result1 = future_result.join |
|
441 |
|
442 val was_timeout = |
|
443 timeout_request match { |
|
444 case None => false |
|
445 case Some(request) => !request.cancel |
|
446 } |
|
447 |
|
448 val result2 = |
|
449 if (result1.interrupted) { |
|
450 if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout |
|
451 else result1.error(Output.error_message_text("Interrupt")) |
|
452 } |
|
453 else result1 |
|
454 |
|
455 val heap_digest = |
|
456 if (result2.ok && do_store && store.output_heap(session_name).is_file) |
|
457 Some(Sessions.write_heap_digest(store.output_heap(session_name))) |
|
458 else None |
|
459 |
|
460 (result2, heap_digest) |
|
461 } |
|
462 } |
|
463 |
|
464 |
|
465 |
151 |
466 /** build with results **/ |
152 /** build with results **/ |
467 |
153 |
468 class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) |
154 class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) |
469 { |
155 { |