# HG changeset patch # User wenzelm # Date 1699005315 -3600 # Node ID 88eb92a52f9bbfae5e87472722f907b58561cedf # Parent 6996a20a1b7c808890e47b7ffa57aa124c698bd8# Parent 95bbf9a576b38611d32016fe07797ab55c646bfe merged diff -r 6996a20a1b7c -r 88eb92a52f9b src/Pure/General/time.scala --- a/src/Pure/General/time.scala Fri Nov 03 10:21:21 2023 +0100 +++ b/src/Pure/General/time.scala Fri Nov 03 10:55:15 2023 +0100 @@ -47,6 +47,8 @@ def min(t: Time): Time = if (this < t) this else t def max(t: Time): Time = if (this > t) this else t + def scale(s: Double): Time = new Time((s * ms).ceil.toLong) + def is_zero: Boolean = ms == 0 def is_relevant: Boolean = ms >= 1 diff -r 6996a20a1b7c -r 88eb92a52f9b src/Pure/Tools/build_schedule.scala --- a/src/Pure/Tools/build_schedule.scala Fri Nov 03 10:21:21 2023 +0100 +++ b/src/Pure/Tools/build_schedule.scala Fri Nov 03 10:55:15 2023 +0100 @@ -29,9 +29,6 @@ class Timing_Data private(data: List[Timing_Entry], val host_infos: Host_Infos) { require(data.nonEmpty) - def speedup(time: Time, factor: Double): Time = - Time.ms((time.ms * factor).toLong) - def is_empty = data.isEmpty def size = data.length @@ -64,7 +61,7 @@ def unify_hosts(data: Timing_Data): List[Time] = data.by_hostname.toList.map((hostname, data) => - speedup(data.mean_time, hostname_factor(hostname, ref_hostname))) + data.mean_time.scale(hostname_factor(hostname, ref_hostname))) val entries = data.by_threads.toList.map((threads, data) => @@ -102,7 +99,7 @@ val approximated = data.by_hostname.toList.flatMap((hostname1, data) => data.approximate_threads(threads).map(time => - speedup(time, hostname_factor(hostname1, hostname)))) + time.scale(hostname_factor(hostname1, hostname)))) if (approximated.nonEmpty) Timing_Data.mean_time(approximated) else { @@ -110,7 +107,7 @@ data.approximate_threads(threads).getOrElse { // only single data point, use global curve to approximate val global_factor = threads_factor(data.by_threads.keys.head, threads) - speedup(data.by_threads.values.head.mean_time, global_factor) + data.by_threads.values.head.mean_time.scale(global_factor) } } } @@ -119,7 +116,7 @@ data.by_hostname.get(hostname).map(_.mean_time).getOrElse { Timing_Data.median_time( data.by_hostname.toList.map((hostname1, data) => - speedup(data.mean_time, hostname_factor(hostname1, hostname)))) + data.mean_time.scale(hostname_factor(hostname1, hostname)))) } } }