--- a/src/Pure/System/host.scala Mon Mar 06 18:58:48 2023 +0100
+++ b/src/Pure/System/host.scala Mon Mar 06 19:09:17 2023 +0100
@@ -46,6 +46,16 @@
} yield n
}
+ def numa_node0(): Option[Int] =
+ try {
+ numa_nodes() match {
+ case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
+ case _ => None
+ }
+ }
+ catch { case ERROR(_) => None }
+
+
/* process policy via numactl tool */
@@ -59,18 +69,6 @@
options.string("process_policy") = if (numactl_ok(node)) numactl(node) else ""
}
- def perhaps_process_policy(options: Options): Options = {
- val numa_node =
- try {
- numa_nodes() match {
- case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
- case _ => None
- }
- }
- catch { case ERROR(_) => None }
- process_policy(options, numa_node)
- }
-
/* shuffling of NUMA nodes */
--- a/src/Pure/Tools/dump.scala Mon Mar 06 18:58:48 2023 +0100
+++ b/src/Pure/Tools/dump.scala Mon Mar 06 19:09:17 2023 +0100
@@ -98,7 +98,7 @@
): Context = {
val session_options: Options = {
val options1 =
- Host.perhaps_process_policy(options) +
+ Host.process_policy(options, Host.numa_node0()) +
"parallel_proofs=0" +
"completion_limit=0" +
"editor_tracing_messages=0"