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 {
|
|
123 |
case Markup.Loading_Theory(name) =>
|
|
124 |
progress.theory(Progress.Theory(name, session = session_name))
|
|
125 |
true
|
|
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 |
|
|
161 |
session.all_messages += Session.Consumer[Any]("build_session_output")
|
|
162 |
{
|
|
163 |
case msg: Prover.Output =>
|
|
164 |
val message = msg.message
|
|
165 |
if (msg.is_stdout) {
|
|
166 |
stdout ++= Symbol.encode(XML.content(message))
|
|
167 |
}
|
|
168 |
else if (msg.is_stderr) {
|
|
169 |
stderr ++= Symbol.encode(XML.content(message))
|
|
170 |
}
|
|
171 |
else if (Protocol.is_exported(message)) {
|
|
172 |
messages += message
|
|
173 |
}
|
|
174 |
else if (msg.is_exit) {
|
|
175 |
val err =
|
|
176 |
"Prover terminated" +
|
|
177 |
(msg.properties match {
|
|
178 |
case Markup.Process_Result(result) => ": " + result.print_rc
|
|
179 |
case _ => ""
|
|
180 |
})
|
|
181 |
Build_Session_Errors(List(err))
|
|
182 |
}
|
|
183 |
case _ =>
|
|
184 |
}
|
|
185 |
|
|
186 |
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
|
|
187 |
|
|
188 |
val process =
|
|
189 |
Isabelle_Process(session, options, sessions_structure, store,
|
|
190 |
logic = parent, raw_ml_system = is_pure,
|
|
191 |
use_prelude = use_prelude, eval_main = eval_main,
|
|
192 |
cwd = info.dir.file, env = env)
|
|
193 |
|
|
194 |
val build_errors =
|
|
195 |
Isabelle_Thread.interrupt_handler(_ => process.terminate) {
|
|
196 |
Exn.capture { process.await_startup } match {
|
|
197 |
case Exn.Res(_) =>
|
|
198 |
val resources_yxml = resources.init_session_yxml
|
|
199 |
val args_yxml =
|
|
200 |
YXML.string_of_body(
|
|
201 |
{
|
|
202 |
import XML.Encode._
|
|
203 |
pair(string, list(pair(Options.encode, list(pair(string, properties)))))(
|
|
204 |
(session_name, info.theories))
|
|
205 |
})
|
|
206 |
session.protocol_command("build_session", resources_yxml, args_yxml)
|
|
207 |
Build_Session_Errors.result
|
|
208 |
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
|
|
209 |
}
|
|
210 |
}
|
|
211 |
|
|
212 |
val process_result =
|
|
213 |
Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
|
|
214 |
|
|
215 |
val export_errors =
|
|
216 |
export_consumer.shutdown(close = true).map(Output.error_message_text)
|
|
217 |
|
|
218 |
val document_errors =
|
|
219 |
try {
|
|
220 |
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) {
|
|
221 |
val documents =
|
|
222 |
if (info.documents.isEmpty) Nil
|
|
223 |
else {
|
|
224 |
val document_progress =
|
|
225 |
new Progress {
|
|
226 |
override def echo(msg: String): Unit =
|
|
227 |
document_output.synchronized { document_output += msg }
|
|
228 |
override def echo_document(path: Path): Unit =
|
|
229 |
progress.echo_document(path)
|
|
230 |
}
|
|
231 |
val documents =
|
|
232 |
Presentation.build_documents(session_name, deps, store, verbose = verbose,
|
|
233 |
verbose_latex = true, progress = document_progress)
|
|
234 |
using(store.open_database(session_name, output = true))(db =>
|
|
235 |
for ((doc, pdf) <- documents) {
|
|
236 |
db.transaction {
|
|
237 |
Presentation.write_document(db, session_name, doc, pdf)
|
|
238 |
}
|
|
239 |
})
|
|
240 |
documents
|
|
241 |
}
|
|
242 |
if (presentation.enabled(info)) {
|
|
243 |
val dir = Presentation.session_html(session_name, deps, store, presentation)
|
|
244 |
for ((doc, pdf) <- documents) Bytes.write(dir + doc.path.pdf, pdf)
|
|
245 |
if (verbose) progress.echo("Browser info at " + dir.absolute)
|
|
246 |
}
|
|
247 |
}
|
|
248 |
Nil
|
|
249 |
}
|
|
250 |
catch { case Exn.Interrupt.ERROR(msg) => List(msg) }
|
|
251 |
|
|
252 |
val result =
|
|
253 |
{
|
|
254 |
val more_output =
|
|
255 |
Library.trim_line(stdout.toString) ::
|
|
256 |
messages.toList.map(message =>
|
|
257 |
Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
|
|
258 |
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
|
|
259 |
theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
|
|
260 |
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
|
|
261 |
runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
|
|
262 |
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
|
|
263 |
document_output.toList
|
|
264 |
|
|
265 |
val more_errors =
|
|
266 |
Library.trim_line(stderr.toString) :: export_errors ::: document_errors
|
|
267 |
|
|
268 |
process_result.output(more_output).errors(more_errors)
|
|
269 |
}
|
|
270 |
|
|
271 |
build_errors match {
|
|
272 |
case Exn.Res(build_errs) =>
|
|
273 |
val errs = build_errs ::: document_errors
|
|
274 |
if (errs.isEmpty) result
|
|
275 |
else {
|
|
276 |
result.error_rc.output(
|
|
277 |
errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
|
|
278 |
errs.map(Protocol.Error_Message_Marker.apply))
|
|
279 |
}
|
|
280 |
case Exn.Exn(Exn.Interrupt()) =>
|
|
281 |
if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
|
|
282 |
case Exn.Exn(exn) => throw exn
|
|
283 |
}
|
|
284 |
}
|
|
285 |
|
|
286 |
def terminate: Unit = future_result.cancel
|
|
287 |
def is_finished: Boolean = future_result.is_finished
|
|
288 |
|
|
289 |
private val timeout_request: Option[Event_Timer.Request] =
|
|
290 |
{
|
|
291 |
if (info.timeout > Time.zero)
|
|
292 |
Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
|
|
293 |
else None
|
|
294 |
}
|
|
295 |
|
|
296 |
def join: (Process_Result, Option[String]) =
|
|
297 |
{
|
|
298 |
val result1 = future_result.join
|
|
299 |
|
|
300 |
val was_timeout =
|
|
301 |
timeout_request match {
|
|
302 |
case None => false
|
|
303 |
case Some(request) => !request.cancel
|
|
304 |
}
|
|
305 |
|
|
306 |
val result2 =
|
|
307 |
if (result1.interrupted) {
|
|
308 |
if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
|
|
309 |
else result1.error(Output.error_message_text("Interrupt"))
|
|
310 |
}
|
|
311 |
else result1
|
|
312 |
|
|
313 |
val heap_digest =
|
|
314 |
if (result2.ok && do_store && store.output_heap(session_name).is_file)
|
|
315 |
Some(Sessions.write_heap_digest(store.output_heap(session_name)))
|
|
316 |
else None
|
|
317 |
|
|
318 |
(result2, heap_digest)
|
|
319 |
}
|
|
320 |
}
|