--- a/src/Pure/System/benchmark.scala Tue Feb 13 21:28:08 2024 +0100
+++ b/src/Pure/System/benchmark.scala Wed Feb 14 11:08:05 2024 +0100
@@ -98,7 +98,7 @@
progress.echo(
"Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score))
- Host.write_info(db, Host.Info.gather(hostname, score = Some(score)))
+ Host.write_info(db, Host.Info.init(hostname = hostname, score = Some(score)))
}
}
}
--- a/src/Pure/System/host.scala Tue Feb 13 21:28:08 2024 +0100
+++ b/src/Pure/System/host.scala Wed Feb 14 11:08:05 2024 +0100
@@ -135,15 +135,21 @@
}
object Info {
- def gather(hostname: String, ssh: SSH.System = SSH.Local, score: Option[Double] = None): Info =
- Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score)
+ def init(
+ hostname: String = SSH.LOCAL,
+ ssh: SSH.System = SSH.Local,
+ score: Option[Double] = None
+ ): Info = Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score)
}
sealed case class Info(
hostname: String,
numa_nodes: List[Int],
num_cpus: Int,
- benchmark_score: Option[Double])
+ benchmark_score: Option[Double]
+ ) {
+ override def toString: String = hostname
+ }
/* shuffling of NUMA nodes */