# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701352081 -3600
# Node ID 3620010c410a631b9a78bf95bb0cdc74d6a12a38
# Parent  59d5d1e2639380ff816550b3d5140ed8a0027950
use cpu time for approximation;

diff -r 59d5d1e26393 -r 3620010c410a src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 30 14:08:21 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 30 14:48:01 2023 +0100
@@ -18,6 +18,7 @@
 
   case class Timing_Entry(job_name: String, hostname: String, threads: Int, timing: Timing) {
     def elapsed: Time = timing.elapsed
+    def proper_cpu: Option[Time] = timing.cpu.proper_ms.map(Time.ms)
   }
   case class Timing_Entries(entries: List[Timing_Entry]) {
     require(entries.nonEmpty)
@@ -121,12 +122,20 @@
     }
 
     def estimate_threads(job_name: String, hostname: String, threads: Int): Option[Time] = {
+      def try_approximate(data: Timing_Entries): Option[Time] = {
+        val entries =
+          data.by_threads.toList match {
+            case List((i, Timing_Entries(List(entry)))) if i != 1 =>
+              (i, data.mean_time) :: entry.proper_cpu.map(1 -> _).toList
+            case entries => entries.map((threads, data) => threads -> data.mean_time)
+          }
+        if (entries.size < 2) None else Some(approximate_threads(entries, threads))
+      }
+
       for {
         data <- data.by_job.get(job_name)
         data <- data.by_hostname.get(hostname)
-        entries = data.by_threads.toList.map((threads, data) => threads -> data.mean_time)
-        time <- data.by_threads.get(threads).map(_.mean_time).orElse(
-          if (data.by_threads.size < 2) None else Some(approximate_threads(entries, threads)))
+        time <- data.by_threads.get(threads).map(_.mean_time).orElse(try_approximate(data))
       } yield time
     }