implicit use of NUMA policy, absorbing potential errors;

--- a/src/Pure/System/numa.scala	Sat Sep 08 22:09:52 2018 +0200
+++ b/src/Pure/System/numa.scala	Sat Sep 08 22:21:19 2018 +0200
@@ -39,7 +39,7 @@
   def policy(node: Int): String =
     if (numactl_available) "numactl -m" + node + " -N" + node else ""
 
-  def policy_options(options: Options, numa_node: Option[Int]): Options =
+  def policy_options(options: Options, numa_node: Option[Int] = Some(0)): Options =
     numa_node match {
       case None => options
       case Some(n) => options.string("ML_process_policy") = policy(n)
@@ -48,6 +48,10 @@
 
   /* shuffling of CPU nodes */
 
+  def enabled: Boolean =
+    try { nodes().length >= 2 && numactl_available }
+    catch { case ERROR(_) => false }
+
   def enabled_warning(progress: Progress, enabled: Boolean): Boolean =
   {
     def warning =

--- a/src/Pure/Tools/dump.scala	Sat Sep 08 22:09:52 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Sep 08 22:21:19 2018 +0200
@@ -79,7 +79,8 @@
 
   def make_options(options: Options, aspects: List[Aspect]): Options =
   {
-    val options1 = options + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0"
+    val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
+    val options1 = options0 + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0"
     (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
   }