# HG changeset patch # User wenzelm # Date 1676145264 -3600 # Node ID 173c2fb78290e80a3ce313d192b628353355edf5 # Parent 1e2670d9dc18206f37b2faa0bb654230919a36d3 clarified modules; clarified signature; diff -r 1e2670d9dc18 -r 173c2fb78290 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Feb 11 20:09:37 2023 +0100 +++ b/src/Pure/Tools/build.scala Sat Feb 11 20:54:24 2023 +0100 @@ -31,74 +31,36 @@ /* queue with scheduling information */ private object Queue { - def make_session_timing( - sessions_structure: Sessions.Structure, - timing: Map[String, Double] - ) : Map[String, Double] = { - val maximals = sessions_structure.build_graph.maximals.toSet - def desc_timing(session_name: String): Double = { - if (maximals.contains(session_name)) timing(session_name) - else { - val descendants = sessions_structure.build_descendants(List(session_name)).toSet - val g = sessions_structure.build_graph.restrict(descendants) - (0.0 :: g.maximals.flatMap { desc => - val ps = g.all_preds(List(desc)) - if (ps.exists(p => !timing.isDefinedAt(p))) None - else Some(ps.map(timing(_)).sum) - }).max - } - } - timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) - } - def apply( - progress: Progress, sessions_structure: Sessions.Structure, - store: Sessions.Store - ) : Queue = { - val graph = sessions_structure.build_graph - val sessions = graph.keys - - val timings = - for (session <- graph.keys) - yield Build_Process.Session_Context.load(session, store, progress = progress) - val command_timings = - timings.map(timing => timing.session -> timing.old_command_timings).toMap.withDefaultValue(Nil) - val session_timing = - make_session_timing(sessions_structure, - timings.map(timing => timing.session -> timing.old_time.seconds).toMap) - - object Ordering extends scala.math.Ordering[String] { - def compare(name1: String, name2: String): Int = - session_timing(name2) compare session_timing(name1) match { - case 0 => - sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { - case 0 => name1 compare name2 - case ord => ord - } - case ord => ord - } - } - - new Queue(graph, SortedSet.from(sessions)(Ordering), command_timings) + store: Sessions.Store, + progress: Progress = new Progress + ): Queue = { + val context = Build_Process.Context(sessions_structure, store, progress = progress) + val build_graph = sessions_structure.build_graph + val sessions = SortedSet.from(build_graph.keys)(context.ordering) + new Queue(context, build_graph, sessions) } } private class Queue( - graph: Graph[String, Sessions.Info], - order: SortedSet[String], - val command_timings: String => List[Properties.T] + context: Build_Process.Context, + build_graph: Graph[String, Sessions.Info], + order: SortedSet[String] ) { - def is_inner(name: String): Boolean = !graph.is_maximal(name) + def old_command_timings(name: String): List[Properties.T] = + context(name).old_command_timings - def is_empty: Boolean = graph.is_empty + def is_inner(name: String): Boolean = !build_graph.is_maximal(name) + + def is_empty: Boolean = build_graph.is_empty def - (name: String): Queue = - new Queue(graph.del_node(name), order - name, command_timings) + new Queue(context, build_graph.del_node(name), order - name) def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] = { - val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name)) - if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) } + val it = order.iterator.dropWhile(name => skip(name) || !build_graph.is_minimal(name)) + if (it.hasNext) { val name = it.next(); Some((name, build_graph.get_node(name))) } else None } } @@ -225,7 +187,7 @@ /* main build process */ - val queue = Queue(progress, build_deps.sessions_structure, store) + val queue = Queue(build_deps.sessions_structure, store, progress = progress) store.prepare_output_dir() @@ -400,7 +362,7 @@ val session_background = build_deps.background(session_name) val resources = new Resources(session_background, log = log, - command_timings = queue.command_timings(session_name)) + command_timings = queue.old_command_timings(session_name)) val numa_node = numa_nodes.next(used_node) val job = diff -r 1e2670d9dc18 -r 173c2fb78290 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Sat Feb 11 20:09:37 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Sat Feb 11 20:54:24 2023 +0100 @@ -8,13 +8,16 @@ package isabelle +import scala.math.Ordering + + object Build_Process { /* static information */ object Session_Context { def empty(session: String): Session_Context = new Session_Context(session, Time.zero, Nil) - def load( + def apply( session: String, store: Sessions.Store, progress: Progress = new Progress @@ -55,4 +58,64 @@ override def toString: String = session } + + object Context { + private def make_session_timing( + sessions_structure: Sessions.Structure, + timing: Map[String, Double] + ) : Map[String, Double] = { + val maximals = sessions_structure.build_graph.maximals.toSet + def desc_timing(session_name: String): Double = { + if (maximals.contains(session_name)) timing(session_name) + else { + val descendants = sessions_structure.build_descendants(List(session_name)).toSet + val g = sessions_structure.build_graph.restrict(descendants) + (0.0 :: g.maximals.flatMap { desc => + val ps = g.all_preds(List(desc)) + if (ps.exists(p => !timing.isDefinedAt(p))) None + else Some(ps.map(timing(_)).sum) + }).max + } + } + timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) + } + + def apply( + sessions_structure: Sessions.Structure, + store: Sessions.Store, + progress: Progress = new Progress + ): Context = { + val sessions = + Map.from( + for (session <- sessions_structure.build_graph.keys_iterator) + yield session -> Build_Process.Session_Context(session, store, progress = progress)) + + val session_timing = + make_session_timing(sessions_structure, + Map.from(for ((name, context) <- sessions.iterator) yield name -> context.old_time.seconds)) + + val ordering = + new Ordering[String] { + def compare(name1: String, name2: String): Int = + session_timing(name2) compare session_timing(name1) match { + case 0 => + sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { + case 0 => name1 compare name2 + case ord => ord + } + case ord => ord + } + } + + new Context(sessions, ordering) + } + } + + final class Context private( + sessions: Map[String, Session_Context], + val ordering: Ordering[String] + ) { + def apply(session: String): Session_Context = + sessions.getOrElse(session, Session_Context.empty(session)) + } }