# HG changeset patch
# User wenzelm
# Date 1676925652 -3600
# Node ID 87698fe320bbf56e1904aca169c1eb8b038071fa
# Parent  7a03477bf3d50b8a6c0b5fde6c9caad0158428be
clarified signature: more robust operations, without assumption about node 0;

diff -r 7a03477bf3d5 -r 87698fe320bb src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Mon Feb 20 21:04:49 2023 +0100
+++ b/src/Pure/System/numa.scala	Mon Feb 20 21:40:52 2023 +0100
@@ -32,10 +32,10 @@
 
   /* CPU policy via numactl tool */
 
-  lazy val numactl_available: Boolean = Isabelle_System.bash("numactl -m0 -N0 true").ok
+  def numactl(node: Int): String = "numactl -m" + node + " -N" + node
+  def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok
 
-  def policy(node: Int): String =
-    if (numactl_available) "numactl -m" + node + " -N" + node else ""
+  def policy(node: Int): String = if (numactl_ok(node)) numactl(node) else ""
 
   def policy_options(options: Options, numa_node: Option[Int]): Options =
     numa_node match {
@@ -47,7 +47,7 @@
     val numa_node =
       try {
         nodes() match {
-          case ns if ns.length >= 2 && numactl_available => ns.headOption
+          case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
           case _ => None
         }
       }
@@ -60,9 +60,11 @@
 
   def enabled_warning(progress: Progress, enabled: Boolean): Boolean = {
     def warning =
-      if (nodes().length < 2) Some("no NUMA nodes available")
-      else if (!numactl_available) Some("bad numactl tool")
-      else None
+      nodes() match {
+        case ns if ns.length < 2 => Some("no NUMA nodes available")
+        case ns if !numactl_ok(ns.head) => Some("bad numactl tool")
+        case _ => None
+      }
 
     enabled &&
       (warning match {