# HG changeset patch
# User wenzelm
# Date 1698316579 -7200
# Node ID 26a43785590b3154ee558aaf4ed15d33ed82af16
# Parent  3958180eaa7253536802ccfdb585d95fff3c5a77
proper support for SSH;

diff -r 3958180eaa72 -r 26a43785590b src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Thu Oct 26 12:27:10 2023 +0200
+++ b/src/Pure/System/host.scala	Thu Oct 26 12:36:19 2023 +0200
@@ -122,11 +122,21 @@
     }
     catch { case ERROR(_) => None }
 
-  def num_cpus(): Int = Runtime.getRuntime.availableProcessors
+  def num_cpus(ssh: SSH.System = SSH.Local): Int =
+    if (ssh.is_local) Runtime.getRuntime.availableProcessors
+    else {
+      val command =
+        if (ssh.isabelle_platform.is_macos) "sysctl -n hw.ncpu" else "nproc"
+      val result = ssh.execute(command).check
+      Library.trim_line(result.out) match {
+        case Value.Int(n) => n
+        case _ => 1
+      }
+    }
 
   object Info {
     def gather(hostname: String, ssh: SSH.System = SSH.Local, score: Option[Double] = None): Info =
-      Info(hostname, numa_nodes(ssh = ssh), num_cpus(), score)
+      Info(hostname, numa_nodes(ssh = ssh), num_cpus(ssh = ssh), score)
   }
 
   sealed case class Info(