--- 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
}
--- 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).