# HG changeset patch
# User wenzelm
# Date 1707918078 -3600
# Node ID 0e8ac7db1f4daa3651eb21a3483d782741ef36cb
# Parent  9f002cdb6b8dcf5ccc4add991919fbc1ff9b0c24
clarified num_processors: follow Poly/ML (with its inaccuracies);

diff -r 9f002cdb6b8d -r 0e8ac7db1f4d src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Wed Feb 14 14:16:56 2024 +0100
+++ b/src/Pure/Concurrent/multithreading.ML	Wed Feb 14 14:41:18 2024 +0100
@@ -8,6 +8,7 @@
 
 signature MULTITHREADING =
 sig
+  val num_processors: unit -> int
   val max_threads: unit -> int
   val max_threads_update: int -> unit
   val parallel_proofs: int ref
@@ -22,15 +23,18 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* max_threads *)
-
-local
+(* physical processors *)
 
 fun num_processors () =
   (case Thread.Thread.numPhysicalProcessors () of
     SOME n => n
   | NONE => Thread.Thread.numProcessors ());
 
+
+(* max_threads *)
+
+local
+
 fun max_threads_result m =
   if Thread_Data.is_virtual then 1
   else if m > 0 then m
diff -r 9f002cdb6b8d -r 0e8ac7db1f4d src/Pure/Concurrent/multithreading.scala
--- a/src/Pure/Concurrent/multithreading.scala	Wed Feb 14 14:16:56 2024 +0100
+++ b/src/Pure/Concurrent/multithreading.scala	Wed Feb 14 14:41:18 2024 +0100
@@ -8,10 +8,27 @@
 
 
 object Multithreading {
+  /* physical processors */
+
+  def num_processors(ssh: SSH.System = SSH.Local): Int =
+    if (ssh.isabelle_platform.is_macos) {
+      val result = ssh.execute("sysctl -n hw.physicalcpu").check
+      Library.trim_line(result.out) match {
+        case Value.Int(n) => n
+        case _ => 1
+      }
+    }
+    else {
+      val Core_Id = """^\s*core id\s*:\s*(\d+)\s*$""".r
+      val cpuinfo = ssh.read(Path.explode("/proc/cpuinfo"))
+      (for (case Core_Id(Value.Int(i)) <- Library.trim_split_lines(cpuinfo)) yield i).toSet.size
+    }
+
+
   /* max_threads */
 
   def max_threads(): Int = {
     val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
-    if (m > 0) m else (Host.num_cpus() max 1) min 8
+    if (m > 0) m else (num_processors() max 1) min 8
   }
 }