# HG changeset patch # User wenzelm # Date 1676231635 -3600 # Node ID 61fc2afe4c8b2aceded6b99b52a0e34c161a6450 # Parent ca8eda3c1808d88cb754d8002e24b51013994514 clarified signature: prefer stateful object-oriented style, to make it fit better into physical world; diff -r ca8eda3c1808 -r 61fc2afe4c8b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Feb 12 15:33:02 2023 +0100 +++ b/src/Pure/Tools/build.scala Sun Feb 12 20:53:55 2023 +0100 @@ -155,9 +155,11 @@ } else { Isabelle_Thread.uninterruptible { - Build_Process.main(build_context, build_heap = build_heap, - numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, - no_build = no_build, verbose = verbose, session_setup = session_setup) + val build_process = + new Build_Process(build_context, build_heap = build_heap, + numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, + no_build = no_build, verbose = verbose, session_setup = session_setup) + build_process.run() } } diff -r ca8eda3c1808 -r 61fc2afe4c8b src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Sun Feb 12 15:33:02 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Sun Feb 12 20:53:55 2023 +0100 @@ -136,6 +136,63 @@ /* main */ + case class Result( + current: Boolean, + output_heap: SHA1.Shasum, + process_result: Process_Result + ) { + def ok: Boolean = process_result.ok + } +} + +class Build_Process( + build_context: Build_Process.Context, + build_heap: Boolean = false, + numa_shuffling: Boolean = false, + max_jobs: Int = 1, + fresh_build: Boolean = false, + no_build: Boolean = false, + verbose: Boolean = false, + session_setup: (String, Session) => Unit = (_, _) => () +) { + private val store = build_context.store + private val build_options = store.options + private val build_deps = build_context.deps + private val progress = build_context.progress + + // global state + private val numa_nodes = new NUMA.Nodes(numa_shuffling) + private var build_graph = build_context.sessions_structure.build_graph + private var build_order = SortedSet.from(build_graph.keys)(build_context.ordering) + private var running = Map.empty[String, (SHA1.Shasum, Build_Job)] + private var results = Map.empty[String, Build_Process.Result] + + private def sleep(): Unit = + Isabelle_Thread.interrupt_handler(_ => progress.stop()) { + build_options.seconds("editor_input_delay").sleep() + } + + private val log = + build_options.string("system_log") match { + case "" => No_Logger + case "-" => Logger.make(progress) + case log_file => Logger.make(Some(Path.explode(log_file))) + } + + private def remove_pending(name: String): Unit = { + build_graph = build_graph.del_node(name) + build_order = build_order - name + } + + private def next_pending(): Option[String] = + build_order.iterator + .dropWhile(name => running.isDefinedAt(name) || !build_graph.is_minimal(name)) + .nextOption() + + private def used_node(i: Int): Boolean = + running.iterator.exists( + { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i }) + private def session_finished(session_name: String, process_result: Process_Result): String = "Finished " + session_name + " (" + process_result.timing.message_resources + ")" @@ -146,62 +203,7 @@ "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")" } - case class Result( - current: Boolean, - output_heap: SHA1.Shasum, - process_result: Process_Result - ) { - def ok: Boolean = process_result.ok - } - - def main( - build_context: Context, - build_heap: Boolean = false, - numa_shuffling: Boolean = false, - max_jobs: Int = 1, - fresh_build: Boolean = false, - no_build: Boolean = false, - verbose: Boolean = false, - session_setup: (String, Session) => Unit = (_, _) => () - ): Map[String, Result] = { - val store = build_context.store - val build_options = store.options - val build_deps = build_context.deps - val progress = build_context.progress - - def sleep(): Unit = - Isabelle_Thread.interrupt_handler(_ => progress.stop()) { - build_options.seconds("editor_input_delay").sleep() - } - - val log = - build_options.string("system_log") match { - case "" => No_Logger - case "-" => Logger.make(progress) - case log_file => Logger.make(Some(Path.explode(log_file))) - } - - // global state - val numa_nodes = new NUMA.Nodes(numa_shuffling) - var build_graph = build_context.sessions_structure.build_graph - var build_order = SortedSet.from(build_graph.keys)(build_context.ordering) - var running = Map.empty[String, (SHA1.Shasum, Build_Job)] - var results = Map.empty[String, Result] - - def remove_pending(name: String): Unit = { - build_graph = build_graph.del_node(name) - build_order = build_order - name - } - - def next_pending(): Option[String] = - build_order.iterator - .dropWhile(name => running.isDefinedAt(name) || !build_graph.is_minimal(name)) - .nextOption() - - def used_node(i: Int): Boolean = - running.iterator.exists( - { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i }) - + def run(): Map[String, Build_Process.Result] = { @tailrec def loop(): Unit = { if (!build_graph.is_empty) { if (progress.stopped) { @@ -266,7 +268,7 @@ remove_pending(session_name) running -= session_name - results += (session_name -> Result(false, output_heap, process_result_tail)) + results += (session_name -> Build_Process.Result(false, output_heap, process_result_tail)) loop() //}}} case None if running.size < (max_jobs max 1) => @@ -306,13 +308,13 @@ if (all_current) { remove_pending(session_name) - results += (session_name -> Result(true, output_heap, Process_Result.ok)) + results += (session_name -> Build_Process.Result(true, output_heap, Process_Result.ok)) loop() } else if (no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") remove_pending(session_name) - results += (session_name -> Result(false, output_heap, Process_Result.error)) + results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.error)) loop() } else if (ancestor_results.forall(_.ok) && !progress.stopped) { @@ -337,7 +339,7 @@ else { progress.echo(session_name + " CANCELLED") remove_pending(session_name) - results += (session_name -> Result(false, output_heap, Process_Result.undefined)) + results += (session_name -> Build_Process.Result(false, output_heap, Process_Result.undefined)) loop() } case None => sleep(); loop()