# HG changeset patch
# User wenzelm
# Date 1708113261 -3600
# Node ID 7eaf1931f408b2f92dc3cb75e87d5b5f46f6a65e
# Parent  5bedeb0dc827b299ccfa10ddf343efd9567fc9a7# Parent  a14497801192def2528f052c2b8a23196b1ef50a
merged

diff -r 5bedeb0dc827 -r 7eaf1931f408 src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Fri Feb 16 15:55:06 2024 +0000
+++ b/src/Pure/Build/build_cluster.scala	Fri Feb 16 20:54: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,11 @@
       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 +97,7 @@
           jobs = params.int(JOBS),
           numa = params.bool(NUMA),
           dirs = params.string(DIRS),
+          home = params.string(HOME),
           shared = params.bool(SHARED),
           options = options)
       }
@@ -112,12 +115,15 @@
     val jobs: Int,
     val numa: Boolean,
     val dirs: String,
+    val home: String,
     val shared: Boolean,
     val options: List[Options.Spec]
   ) {
     host =>
 
-    def ssh_host: String = proper_string(hostname) getOrElse name
+    Path.split(host.dirs)  // check
+
+    def ssh_host: String = proper_string(host.hostname) getOrElse host.name
     def is_local: Boolean = SSH.is_local(ssh_host)
     def is_remote: Boolean = !is_local
 
@@ -131,7 +137,8 @@
           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(dirs, Options.Spec.print(Host.DIRS, host.dirs)),
+          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 +149,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 = host.home)
 
     def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = {
       val ssh_options = build_context.build_options ++ host.options
diff -r 5bedeb0dc827 -r 7eaf1931f408 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Feb 16 15:55:06 2024 +0000
+++ b/src/Pure/General/ssh.scala	Fri Feb 16 20:54:21 2024 +0100
@@ -95,7 +95,8 @@
     options: Options,
     host: String,
     port: Int = 0,
-    user: String = ""
+    user: String = "",
+    user_home: String = ""
   ): Session = {
     if (is_local(host)) error("Illegal SSH host name " + quote(host))
 
@@ -103,7 +104,7 @@
     val (control_master, control_path) =
       if (multiplex) (true, Isabelle_System.tmp_file("ssh", initialized = false).getPath)
       else (false, "")
-    new Session(options, host, port, user, control_master, control_path)
+    new Session(options, host, port, user, user_home, control_master, control_path)
   }
 
   class Session private[SSH](
@@ -111,6 +112,7 @@
     val host: String,
     val port: Int,
     val user: String,
+    user_home0: String,
     control_master: Boolean,
     val control_path: String
   ) extends System {
@@ -178,11 +180,11 @@
 
     /* init and exit */
 
-    val user_home: String = {
+    override val home: String = {
       run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines
       match {
-        case List(user_home, shell) =>
-          if (shell.endsWith("/bash")) user_home
+        case List(home, shell) =>
+          if (shell.endsWith("/bash")) home
           else {
             error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell)
           }
@@ -190,8 +192,21 @@
       }
     }
 
-    val settings: Isabelle_System.Settings =
-      (name: String) => if (name == "HOME" || name == "USER_HOME") user_home else ""
+    override val user_home: String = {
+      val path1 =
+        try { Path.explode(home).expand_env(Isabelle_System.No_Env) }
+        catch { case ERROR(msg) => error(msg + " -- in SSH HOME") }
+      val path2 =
+        try { Path.explode(user_home0).expand_env(Isabelle_System.No_Env) }
+        catch { case ERROR(msg) => error(msg + "-- in SSH USER_HOME") }
+      (path1 + path2).implode
+    }
+
+    val settings: Isabelle_System.Settings = {
+      case "HOME" => home
+      case "USER_HOME" => user_home
+      case _ => ""
+    }
 
     override def close(): Unit = {
       if (control_path.nonEmpty) run_ssh(opts = "-O exit").check
@@ -207,8 +222,9 @@
       settings: Boolean = true,
       strict: Boolean = true
     ): Process_Result = {
+      val script = Isabelle_System.export_env(user_home = user_home) + cmd_line
       run_command("ssh",
-        args = Bash.string(host) + " " + Bash.string(cmd_line),
+        args = Bash.string(host) + " " + Bash.string(script),
         progress_stdout = progress_stdout,
         progress_stderr = progress_stderr,
         redirect = redirect,
@@ -236,7 +252,7 @@
     override def expand_path(path: Path): Path = path.expand_env(settings)
     override def absolute_path(path: Path): Path = {
       val path1 = expand_path(path)
-      if (path1.is_absolute) path1 else Path.explode(user_home) + path1
+      if (path1.is_absolute) path1 else Path.explode(home) + path1
     }
 
     def remote_path(path: Path): String = expand_path(path).implode
@@ -387,12 +403,13 @@
     host: String,
     port: Int = 0,
     user: String = "",
+    user_home: String = "",
     remote_port: Int = 0,
     remote_host: String = "localhost",
     local_port: Int = 0,
     local_host: String = "localhost"
   ): Server = {
-    val ssh = open_session(options, host, port = port, user = user)
+    val ssh = open_session(options, host, port = port, user = user, user_home = user_home)
     try {
       ssh.open_server(remote_port = remote_port, remote_host = remote_host,
         local_port = local_port, local_host = local_host, ssh_close = true)
@@ -430,16 +447,23 @@
     options: Options,
     host: String,
     port: Int = 0,
-    user: String = ""
+    user: String = "",
+    user_home: String = ""
   ): System = {
-    if (is_local(host)) Local
-    else open_session(options, host = host, port = port, user = user)
+    if (is_local(host)) {
+      if (user_home.isEmpty) Local
+      else error("Illegal user home for local host")
+    }
+    else open_session(options, host = host, port = port, user = user, user_home = user_home)
   }
 
   trait System extends AutoCloseable {
     def ssh_session: Option[Session]
     def is_local: Boolean = ssh_session.isEmpty
 
+    def home: String = ""
+    def user_home: String = ""
+
     def close(): Unit = ()
 
     override def toString: String = LOCAL
diff -r 5bedeb0dc827 -r 7eaf1931f408 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Feb 16 15:55:06 2024 +0000
+++ b/src/Pure/System/isabelle_system.scala	Fri Feb 16 20:54:21 2024 +0100
@@ -28,6 +28,8 @@
     override def get(name: String): String = Option(env.get(name)).getOrElse("")
   }
 
+  object No_Env extends Env(JMap.of())
+
   def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = {
     val env0 = isabelle.setup.Environment.settings()
     if (putenv.isEmpty) env0
@@ -115,7 +117,8 @@
       else ""
     }
 
-  def export_isabelle_identifier(isabelle_identifier: String): String =
+  def export_env(user_home: String = "", isabelle_identifier: String = ""): String =
+    "export USER_HOME=" + Bash.string(user_home) + "\n" +
     "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
 
   def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
diff -r 5bedeb0dc827 -r 7eaf1931f408 src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Fri Feb 16 15:55:06 2024 +0000
+++ b/src/Pure/System/other_isabelle.scala	Fri Feb 16 20:54:21 2024 +0100
@@ -47,9 +47,11 @@
     echo: Boolean = false,
     strict: Boolean = true
   ): Process_Result = {
-    ssh.execute(
-      Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
-        "cd " + ssh.bash_path(isabelle_home) + "\n" + script,
+    val env =
+      Isabelle_System.export_env(
+        user_home = ssh.user_home,
+        isabelle_identifier = isabelle_identifier)
+    ssh.execute(env + "cd " + ssh.bash_path(isabelle_home) + "\n" + script,
       progress_stdout = progress.echo_if(echo, _),
       progress_stderr = progress.echo_if(echo, _),
       redirect = redirect,