# HG changeset patch
# User wenzelm
# Date 1692705066 -7200
# Node ID db99a70f8531728e1aadc8cdc4c1e97bf4798556
# Parent  a04277e3b313956cb50ab40378f3413db740e57f
support hosts with shared directory (e.g. NFS);

diff -r a04277e3b313 -r db99a70f8531 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Tue Aug 22 13:27:53 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Tue Aug 22 13:51:06 2023 +0200
@@ -22,13 +22,15 @@
     private val PORT = "port"
     private val JOBS = "jobs"
     private val NUMA = "numa"
+    private val SHARED = "shared"
 
     val parameters: Options =
       Options.inline("""
-        option user : string = ""   -- "explicit SSH user"
-        option port : int = 0       -- "explicit SSH port"
-        option jobs : int = 1       -- "maximum number of parallel jobs"
-        option numa : bool = false  -- "cyclic shuffling of NUMA CPU nodes"
+        option user : string = ""    -- "explicit SSH user"
+        option port : int = 0        -- "explicit SSH port"
+        option jobs : int = 1        -- "maximum number of parallel jobs"
+        option numa : bool = false   -- "cyclic shuffling of NUMA CPU nodes"
+        option shared : bool = false -- "shared directory: omit sync + init"
       """)
 
     def is_parameter(spec: Options.Spec): Boolean = parameters.defined(spec.name)
@@ -41,8 +43,9 @@
       port: Int = parameters.int(PORT),
       jobs: Int = parameters.int(JOBS),
       numa: Boolean = parameters.bool(NUMA),
+      shared: Boolean = parameters.bool(SHARED),
       options: List[Options.Spec] = Nil
-    ): Host = new Host(name, user, port, jobs, numa, options)
+    ): Host = new Host(name, user, port, jobs, numa, shared, options)
 
     def parse(str: String): Host = {
       val name = str.takeWhile(c => !rfc822_specials.contains(c))
@@ -69,6 +72,7 @@
         port = params.int(PORT),
         jobs = params.int(JOBS),
         numa = params.bool(NUMA),
+        shared = params.bool(SHARED),
         options = options)
     }
   }
@@ -79,6 +83,7 @@
     val port: Int,
     val jobs: Int,
     val numa: Boolean,
+    val shared: Boolean,
     val options: List[Options.Spec]
   ) {
     host =>
@@ -93,7 +98,8 @@
           if (host.user.isEmpty) "" else Options.Spec.print(Host.USER, host.user),
           if (host.port == 0) "" else Options.Spec.print(Host.PORT, host.port.toString),
           if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString),
-          if_proper(host.numa, Host.NUMA)
+          if_proper(host.numa, Host.NUMA),
+          if_proper(host.shared, Host.SHARED)
         ).filter(_.nonEmpty)
       val rest = (params ::: host.options.map(_.print)).mkString(",")
 
@@ -254,7 +260,7 @@
 
     if (_init.isEmpty) {
       _init =
-        for (session <- _sessions) yield {
+        for (session <- _sessions if !session.host.shared) yield {
           Future.thread(session.host.message("session")) {
             capture(session.host, "sync") { session.sync() }
             capture(session.host, "init") { session.init() }