# HG changeset patch # User wenzelm # Date 1677773124 -3600 # Node ID 032c76e044755a9dd0012a088ad3ca82c7a7e7f5 # Parent 911d3dbf2033a8d9ab67b9d819397d6077a07e6c clarified execution context: main work happens within Future.thread; clarified signature: only one "join" operation; diff -r 911d3dbf2033 -r 032c76e04475 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Mar 02 16:39:42 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Thu Mar 02 17:05:24 2023 +0100 @@ -14,9 +14,9 @@ trait Build_Job { def job_name: String def node_info: Host.Node_Info - def terminate(): Unit = () + def cancel(): Unit = () def is_finished: Boolean = false - def finish: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) + def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info) } @@ -119,7 +119,7 @@ val store_heap = build_context.store_heap(session_name) - private val future_result: Future[Process_Result] = + private val future_result: Future[(Process_Result, SHA1.Shasum)] = Future.thread("build", uninterruptible = true) { val env = Isabelle_System.settings( @@ -161,6 +161,9 @@ } } + + /* session */ + val resources = new Resources(session_background, log = build_context.log, command_timings = build_context.old_command_timings(session_name)) @@ -333,6 +336,9 @@ val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) + + /* process */ + val process = Isabelle_Process.start(options, session, session_background, session_heaps, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) @@ -399,6 +405,9 @@ case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } + + /* process result */ + val result1 = { val theory_timing = theory_timings.iterator.flatMap( @@ -447,76 +456,74 @@ else if (result2.interrupted) result2.error(Output.error_message_text("Interrupt")) else result2 - process_result + + /* output heap */ + + val output_shasum = + if (process_result.ok && store_heap && store.output_heap(session_name).is_file) { + SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) + } + else SHA1.no_shasum + + val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) + + val build_log = + Build_Log.Log_File(session_name, process_result.out_lines). + parse_session_info( + command_timings = true, + theory_timings = true, + ml_statistics = true, + task_statistics = true) + + // write log file + if (process_result.ok) { + File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) + } + else File.write(store.output_log(session_name), terminate_lines(log_lines)) + + // write database + using(store.open_database(session_name, output = true))(db => + store.write_session_info(db, session_name, session_sources, + build_log = + if (process_result.timeout) build_log.error("Timeout") else build_log, + build = + Sessions.Build_Info( + sources = build_context.sources_shasum(session_name), + input_heaps = input_shasum, + output_heap = output_shasum, + process_result.rc, build_context.uuid))) + + // messages + process_result.err_lines.foreach(progress.echo) + + if (process_result.ok) { + if (verbose) { + val props = build_log.session_timing + val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 + val timing = Markup.Timing_Properties.get(props) + progress.echo( + "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")") + } + progress.echo( + "Finished " + session_name + " (" + process_result.timing.message_resources + ")") + } + else { + progress.echo( + session_name + " FAILED (see also \"isabelle log -H Error " + session_name + "\")") + if (!process_result.interrupted) { + val tail = info.options.int("process_output_tail") + val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0) + val prefix = if (log_lines.length == suffix.length) Nil else List("...") + progress.echo(Library.trim_line(cat_lines(prefix ::: suffix))) + } + } + + (process_result.copy(out_lines = log_lines), output_shasum) } - override def terminate(): Unit = future_result.cancel() + override def cancel(): Unit = future_result.cancel() override def is_finished: Boolean = future_result.is_finished - - override lazy val finish: (Process_Result, SHA1.Shasum) = { - val process_result = future_result.join - - val output_shasum = - if (process_result.ok && store_heap && store.output_heap(session_name).is_file) { - SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) - } - else SHA1.no_shasum - - val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) - - val build_log = - Build_Log.Log_File(session_name, process_result.out_lines). - parse_session_info( - command_timings = true, - theory_timings = true, - ml_statistics = true, - task_statistics = true) - - // write log file - if (process_result.ok) { - File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) - } - else File.write(store.output_log(session_name), terminate_lines(log_lines)) - - // write database - using(store.open_database(session_name, output = true))(db => - store.write_session_info(db, session_name, session_sources, - build_log = - if (process_result.timeout) build_log.error("Timeout") else build_log, - build = - Sessions.Build_Info( - sources = build_context.sources_shasum(session_name), - input_heaps = input_shasum, - output_heap = output_shasum, - process_result.rc, build_context.uuid))) - - // messages - process_result.err_lines.foreach(progress.echo) - - if (process_result.ok) { - if (verbose) { - val props = build_log.session_timing - val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 - val timing = Markup.Timing_Properties.get(props) - progress.echo( - "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")") - } - progress.echo( - "Finished " + session_name + " (" + process_result.timing.message_resources + ")") - } - else { - progress.echo( - session_name + " FAILED (see also \"isabelle log -H Error " + session_name + "\")") - if (!process_result.interrupted) { - val tail = info.options.int("process_output_tail") - val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0) - val prefix = if (log_lines.length == suffix.length) Nil else List("...") - progress.echo(Library.trim_line(cat_lines(prefix ::: suffix))) - } - } - - (process_result.copy(out_lines = log_lines), output_shasum) - } + override def join: (Process_Result, SHA1.Shasum) = future_result.join } diff -r 911d3dbf2033 -r 032c76e04475 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Thu Mar 02 16:39:42 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Thu Mar 02 17:05:24 2023 +0100 @@ -173,7 +173,7 @@ def is_running(name: String): Boolean = running.isDefinedAt(name) - def stop_running(): Unit = running.valuesIterator.foreach(_.terminate()) + def stop_running(): Unit = running.valuesIterator.foreach(_.cancel()) def finished_running(): List[Build_Job] = List.from(running.valuesIterator.filter(_.is_finished)) @@ -614,7 +614,7 @@ for (job <- synchronized_database { _state.finished_running() }) { val job_name = job.job_name - val (process_result, output_shasum) = job.finish + val (process_result, output_shasum) = job.join synchronized_database { _state = _state. remove_pending(job_name).