# HG changeset patch
# User wenzelm
# Date 1708111101 -3600
# Node ID 432217a1e990d6438bafc1ba26c4e089c36fd449
# Parent  c59231722f10d6d4ce37dbb9abf6849fa005a37c
support for alternative user home, e.g. to avoid slow NFS shares;

diff -r c59231722f10 -r 432217a1e990 src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Fri Feb 16 17:46:43 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Fri Feb 16 20:18:21 2024 +0100
@@ -24,6 +24,7 @@
     private val JOBS = "jobs"
     private val NUMA = "numa"
     private val DIRS = "dirs"
+    private val HOME = "home"
     private val SHARED = "shared"
 
     val parameters: Options =
@@ -34,7 +35,8 @@
         option jobs : int = 1         -- "maximum number of parallel jobs"
         option numa : bool = false    -- "cyclic shuffling of NUMA CPU nodes"
         option dirs : string = ""     -- "additional session directories (separated by colon)"
-        option shared : bool = false  -- "shared directory: omit sync + init"
+        option home : string = ""     -- "alternative user home (via $USER_HOME)"
+        option shared : bool = false  -- "shared home directory: omit sync + init"
       """)
 
     def is_parameter(spec: Options.Spec): Boolean = parameters.defined(spec.name)
@@ -49,11 +51,12 @@
       jobs: Int = parameters.int(JOBS),
       numa: Boolean = parameters.bool(NUMA),
       dirs: String = parameters.string(DIRS),
+      home: String = parameters.string(HOME),
       shared: Boolean = parameters.bool(SHARED),
       options: List[Options.Spec] = Nil
     ): Host = {
       Path.split(dirs)  // check
-      new Host(name, hostname, user, port, jobs, numa, dirs, shared, options)
+      new Host(name, hostname, user, port, jobs, numa, dirs, home, shared, options)
     }
 
     def parse(registry: Registry, str: String): List[Host] = {
@@ -95,6 +98,7 @@
           jobs = params.int(JOBS),
           numa = params.bool(NUMA),
           dirs = params.string(DIRS),
+          home = params.string(HOME),
           shared = params.bool(SHARED),
           options = options)
       }
@@ -112,6 +116,7 @@
     val jobs: Int,
     val numa: Boolean,
     val dirs: String,
+    val home: String,
     val shared: Boolean,
     val options: List[Options.Spec]
   ) {
@@ -132,6 +137,7 @@
           if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString),
           if_proper(host.numa, Host.NUMA),
           if_proper(host.dirs, Options.Spec.print(Host.DIRS, host.dirs)),
+          if_proper(host.home, Options.Spec.print(Host.HOME, host.home)),
           if_proper(host.shared, Host.SHARED)
         ).filter(_.nonEmpty)
       val rest = (params ::: host.options.map(_.print)).mkString(",")
@@ -142,7 +148,8 @@
     def message(msg: String): String = "Host " + quote(host.name) + if_proper(msg, ": " + msg)
 
     def open_ssh(options: Options): SSH.System =
-      SSH.open_system(options ++ host.options, ssh_host, port = host.port, user = host.user)
+      SSH.open_system(options ++ host.options, ssh_host, port = host.port,
+        user = host.user, user_home = home)
 
     def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = {
       val ssh_options = build_context.build_options ++ host.options