diff -r 5f6f567a2661 -r f376aebca9c1 src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Thu Mar 02 14:41:21 2023 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-/*  Title:      Pure/System/numa.scala
-    Author:     Makarius
-
-Support for Non-Uniform Memory Access of separate CPU nodes.
-*/
-
-package isabelle
-
-
-object NUMA {
-  /* information about nodes */
-
-  private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online")
-
-  private val Info_Single = """^(\d+)$""".r
-  private val Info_Multiple = """^(\d+)-(\d+)$""".r
-
-  private def parse_nodes(s: String): List[Int] =
-    s match {
-      case Info_Single(Value.Int(i)) => List(i)
-      case Info_Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
-      case _ => error("Cannot parse CPU node specification: " + quote(s))
-    }
-
-  def nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = {
-    val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None
-    for {
-      path <- numa_info.toList
-      if enabled && ssh.is_file(path)
-      s <- space_explode(',', ssh.read(path).trim)
-      n <- parse_nodes(s)
-    } yield n
-  }
-
-
-  /* CPU policy via numactl tool */
-
-  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_ok(node)) numactl(node) else ""
-
-  def policy_options(options: Options, numa_node: Option[Int]): Options =
-    numa_node match {
-      case None => options
-      case Some(n) => options.string("ML_process_policy") = policy(n)
-    }
-
-  def perhaps_policy_options(options: Options): Options = {
-    val numa_node =
-      try {
-        nodes() match {
-          case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
-          case _ => None
-        }
-      }
-      catch { case ERROR(_) => None }
-    policy_options(options, numa_node)
-  }
-
-
-  /* shuffling of CPU nodes */
-
-  def check(progress: Progress, enabled: Boolean): Boolean = {
-    def warning =
-      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 {
-        case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false
-        case _ => true
-      })
-  }
-}