# HG changeset patch # User wenzelm # Date 1677506259 -3600 # Node ID f184fbac99bc46b70c18bd2502f50e2148bddb79 # Parent 7ed337926ed81c6c18c73314a7d22e7b3cb88b1f clarified modules; diff -r 7ed337926ed8 -r f184fbac99bc src/Pure/Tools/build_job.scala --- 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( diff -r 7ed337926ed8 -r f184fbac99bc src/Pure/Tools/build_process.scala --- 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) =>