# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700818450 -3600
# Node ID 8f6c8a573716431efeac0a62de44f59e2fd7dbae
# Parent  4596a14d9a95f411edceb6a4babe859f95aef8eb
tuned;

diff -r 4596a14d9a95 -r 8f6c8a573716 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 23 16:49:39 2023 +0000
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 24 10:34:10 2023 +0100
@@ -80,28 +80,28 @@
             Time.ms((a.scale(threads) + b).ms max 0)
           }
 
-          val monotone_prefix = sorted_prefix(entries, e => -e._2.ms)
+          val mono_prefix = sorted_prefix(entries, e => -e._2.ms)
 
-          val is_mono = entries == monotone_prefix
-          val in_prefix = monotone_prefix.length > 1 && threads <= monotone_prefix.last._1
-          val in_inflection = !is_mono && threads < entries.drop(monotone_prefix.length).head._1
+          val is_mono = entries == mono_prefix
+          val in_prefix = mono_prefix.length > 1 && threads <= mono_prefix.last._1
+          val in_inflection = !is_mono && threads < entries.drop(mono_prefix.length).head._1
           if (is_mono || in_prefix || in_inflection) {
             // Model with Amdahl's law
             val t_p =
               Timing_Data.median_time(for {
-                (n, t0) <- monotone_prefix
-                (m, t1) <- monotone_prefix
+                (n, t0) <- mono_prefix
+                (m, t1) <- mono_prefix
                 if m != n
               } yield (t0 - t1).scale(n.toDouble * m / (m - n)))
             val t_c =
-              Timing_Data.median_time(for ((n, t) <- monotone_prefix) yield t - t_p.scale(1.0 / n))
+              Timing_Data.median_time(for ((n, t) <- mono_prefix) yield t - t_p.scale(1.0 / n))
 
             def model(threads: Int): Time = t_c + t_p.scale(1.0 / threads)
 
             if (is_mono || in_prefix) model(threads)
             else {
-              val post_inflection = entries.drop(monotone_prefix.length).head
-              val inflection_threads = inflection_point(monotone_prefix.last._1, post_inflection._1)
+              val post_inflection = entries.drop(mono_prefix.length).head
+              val inflection_threads = inflection_point(mono_prefix.last._1, post_inflection._1)
 
               if (threads <= inflection_threads) model(threads)
               else linear((inflection_threads, model(inflection_threads)), post_inflection)