--- a/src/Pure/System/host.scala Mon Mar 06 17:29:00 2023 +0100
+++ b/src/Pure/System/host.scala Mon Mar 06 18:58:48 2023 +0100
@@ -52,15 +52,14 @@
def numactl(node: Int): String = "numactl -m" + node + " -N" + node
def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok
- def process_policy(node: Int): String = if (numactl_ok(node)) numactl(node) else ""
-
- def process_policy_options(options: Options, numa_node: Option[Int]): Options =
+ def process_policy(options: Options, numa_node: Option[Int]): Options =
numa_node match {
case None => options
- case Some(n) => options.string("process_policy") = process_policy(n)
+ case Some(node) =>
+ options.string("process_policy") = if (numactl_ok(node)) numactl(node) else ""
}
- def perhaps_process_policy_options(options: Options): Options = {
+ def perhaps_process_policy(options: Options): Options = {
val numa_node =
try {
numa_nodes() match {
@@ -69,7 +68,7 @@
}
}
catch { case ERROR(_) => None }
- process_policy_options(options, numa_node)
+ process_policy(options, numa_node)
}
--- a/src/Pure/Tools/build_job.scala Mon Mar 06 17:29:00 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Mar 06 18:58:48 2023 +0100
@@ -119,7 +119,7 @@
def job_name: String = session_name
private val info: Sessions.Info = session_background.sessions_structure(session_name)
- private val options: Options = Host.process_policy_options(info.options, node_info.numa_node)
+ private val options: Options = Host.process_policy(info.options, node_info.numa_node)
private val session_sources =
Sessions.Sources.load(session_background.base, cache = store.cache.compress)
--- a/src/Pure/Tools/dump.scala Mon Mar 06 17:29:00 2023 +0100
+++ b/src/Pure/Tools/dump.scala Mon Mar 06 18:58:48 2023 +0100
@@ -98,7 +98,7 @@
): Context = {
val session_options: Options = {
val options1 =
- Host.perhaps_process_policy_options(options) +
+ Host.perhaps_process_policy(options) +
"parallel_proofs=0" +
"completion_limit=0" +
"editor_tracing_messages=0"