# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700841992 -3600
# Node ID cd7c1acc9cf28684417261b34a03bbb5c96e833a
# Parent  1b3a6cc4a2bf3d3394a890f42100311c7de21e59
better estimation for unknown jobs;

diff -r 1b3a6cc4a2bf -r cd7c1acc9cf2 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:05:49 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 24 17:06:32 2023 +0100
@@ -156,7 +156,16 @@
 
     def estimate(job_name: String, hostname: String, threads: Int): Time =
       data.by_job.get(job_name) match {
-        case None => data.mean_time
+        case None =>
+          // no data for job, take average of other jobs for given threads
+          val job_estimates = data.by_job.keys.flatMap(estimate_threads(_, hostname, threads))
+          if (job_estimates.nonEmpty) Timing_Data.mean_time(job_estimates)
+          else {
+            // no other job to estimate from, use global curve to approximate any other job
+            val (threads1, data1) = data.by_threads.head
+            data1.mean_time.scale(global_threads_factor(threads1, threads))
+          }
+
         case Some(data) =>
           data.by_threads.get(threads) match {
             case None => // interpolate threads