--- a/src/Pure/Tools/build_job.scala Mon Feb 27 14:15:14 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Feb 27 14:57:39 2023 +0100
@@ -17,7 +17,7 @@
def start(): Unit = ()
def terminate(): Unit = ()
def is_finished: Boolean = false
- def join: Process_Result = Process_Result.undefined
+ def finish: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info)
}
@@ -36,13 +36,28 @@
override def make_abstract: Abstract = this
}
- class Build_Session(progress: Progress,
+
+ /* build session */
+
+ def session_finished(session_name: String, timing: Timing): String =
+ "Finished " + session_name + " (" + timing.message_resources + ")"
+
+ def session_timing(session_name: String, props: Properties.T): String = {
+ val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
+ val timing = Markup.Timing_Properties.get(props)
+ "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
+ }
+
+ class Build_Session(
+ progress: Progress,
+ verbose: Boolean,
session_background: Sessions.Background,
store: Sessions.Store,
- val do_store: Boolean,
+ do_store: Boolean,
resources: Resources,
session_setup: (String, Session) => Unit,
- val input_heaps: SHA1.Shasum,
+ sources_shasum: SHA1.Shasum,
+ input_heaps: SHA1.Shasum,
override val node_info: Node_Info
) extends Build_Job {
def session_name: String = session_background.session_name
@@ -371,30 +386,78 @@
else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
}
- override def join: Process_Result = {
- val result = future_result.join
+ override lazy val finish: (Process_Result, SHA1.Shasum) = {
+ val process_result = {
+ val result = future_result.join
+
+ val was_timeout =
+ timeout_request match {
+ case None => false
+ case Some(request) => !request.cancel()
+ }
+
+ if (result.ok) result
+ else if (was_timeout) result.error(Output.error_message_text("Timeout")).timeout_rc
+ else if (result.interrupted) result.error(Output.error_message_text("Interrupt"))
+ else result
+ }
- val was_timeout =
- timeout_request match {
- case None => false
- case Some(request) => !request.cancel()
+ val output_heap =
+ if (process_result.ok && do_store && 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)
- if (result.ok) result
- else if (was_timeout) result.error(Output.error_message_text("Timeout")).timeout_rc
- else if (result.interrupted) result.error(Output.error_message_text("Interrupt"))
- else result
- }
+ // 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_shasum, input_heaps, output_heap,
+ process_result.rc, UUID.random().toString)))
+
+ // messages
+ process_result.err_lines.foreach(progress.echo)
- lazy val finish: SHA1.Shasum = {
- require(is_finished, "Build job not finished: " + quote(session_name))
- if (join.ok && do_store && store.output_heap(session_name).is_file) {
- SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
+ if (process_result.ok) {
+ if (verbose) {
+ progress.echo(Build_Job.session_timing(session_name, build_log.session_timing))
+ }
+ progress.echo(Build_Job.session_finished(session_name, process_result.timing))
}
- else SHA1.no_shasum
+ 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_heap)
}
}
+
/* theory markup/messages from session database */
def read_theory(
--- a/src/Pure/Tools/build_process.scala Mon Feb 27 14:15:14 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Feb 27 14:57:39 2023 +0100
@@ -485,19 +485,10 @@
state.copy(serial = serial)
}
}
+}
- /* main process */
-
- def session_finished(session_name: String, timing: Timing): String =
- "Finished " + session_name + " (" + timing.message_resources + ")"
-
- def session_timing(session_name: String, props: Properties.T): String = {
- val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
- val timing = Markup.Timing_Properties.get(props)
- "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
- }
-}
+/* main process */
class Build_Process(protected val build_context: Build_Process.Context) extends AutoCloseable {
protected val store: Sessions.Store = build_context.store
@@ -550,65 +541,6 @@
_state.finished_running()
}
- protected def finish_job(job: Build_Job.Build_Session): Unit = {
- val session_name = job.session_name
- val process_result = job.join
- val output_heap = job.finish
-
- 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, job.session_sources,
- build_log =
- if (process_result.timeout) build_log.error("Timeout") else build_log,
- build =
- Sessions.Build_Info(build_deps.sources_shasum(session_name), job.input_heaps,
- output_heap, process_result.rc, UUID.random().toString)))
-
- // messages
- process_result.err_lines.foreach(progress.echo)
-
- if (process_result.ok) {
- if (verbose) {
- progress.echo(Build_Process.session_timing(session_name, build_log.session_timing))
- }
- progress.echo(Build_Process.session_finished(session_name, process_result.timing))
- }
- else {
- progress.echo(
- session_name + " FAILED (see also \"isabelle log -H Error " + session_name + "\")")
- if (!process_result.interrupted) {
- val tail = job.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)))
- }
- }
-
- synchronized {
- _state = _state.
- remove_pending(session_name).
- remove_running(session_name).
- make_result(session_name, false, output_heap, process_result.copy(out_lines = log_lines),
- node_info = job.node_info)
- }
- }
-
protected def start_job(session_name: String): Unit = {
val ancestor_results = synchronized {
_state.get_results(
@@ -675,8 +607,9 @@
val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
val job =
- new Build_Job.Build_Session(progress, session_background, store, do_store,
- resources, build_context.session_setup, input_heaps, node_info)
+ new Build_Job.Build_Session(progress, verbose, session_background, store, do_store,
+ resources, build_context.session_setup, build_deps.sources_shasum(session_name),
+ input_heaps, node_info)
_state = state1.add_running(session_name, job)
job
}
@@ -725,7 +658,17 @@
while (!finished()) {
if (progress.stopped) stop_running()
- for (job <- finished_running()) finish_job(job)
+ for (job <- finished_running()) {
+ val session_name = job.session_name
+ val (process_result, output_heap) = job.finish
+ synchronized {
+ _state = _state.
+ remove_pending(session_name).
+ remove_running(session_name).
+ make_result(session_name, false, output_heap, process_result,
+ node_info = job.node_info)
+ }
+ }
next_pending() match {
case Some(name) =>