# HG changeset patch # User Fabian Huch # Date 1700767603 -3600 # Node ID 6585acdd6505ea8ab2595eba48337591e4b9ca1e # Parent f78ee2d48bf55bb453716792370488ef33aed513 clarified time estimation: does not use config; diff -r f78ee2d48bf5 -r 6585acdd6505 src/Pure/Tools/build_schedule.scala --- a/src/Pure/Tools/build_schedule.scala Thu Nov 23 19:56:27 2023 +0100 +++ b/src/Pure/Tools/build_schedule.scala Thu Nov 23 20:26:43 2023 +0100 @@ -50,7 +50,7 @@ def best_time(job_name: String): Time = by_job.get(job_name).map(_.best_entry.elapsed).getOrElse( - estimate_config(Config(job_name, Node_Info(best_entry.hostname, None, Nil)))) + estimate(job_name, best_entry.hostname, best_entry.threads)) private def hostname_factor(from: String, to: String): Double = host_infos.host_factor(host_infos.the_host(from), host_infos.the_host(to)) @@ -132,12 +132,10 @@ case _ => divided.toDouble / divisor } - def estimate_config(config: Config): Time = - by_job.get(config.job_name) match { + def estimate(job_name: String, hostname: String, threads: Int): Time = + by_job.get(job_name) match { case None => mean_time case Some(data) => - val hostname = config.node_info.hostname - val threads = host_infos.num_threads(config.node_info) data.by_threads.get(threads) match { case None => // interpolate threads data.by_hostname.get(hostname).flatMap( @@ -350,7 +348,8 @@ val remaining = build_state.running.values.toList.map { job => val elapsed = current_time - job.start_date.time - val predicted = timing_data.estimate_config(Config.from_job(job)) + val threads = timing_data.host_infos.num_threads(job.node_info) + val predicted = timing_data.estimate(job.name, job.node_info.hostname, threads) val remaining = if (elapsed > predicted) Time.zero else predicted - elapsed job -> remaining }