--- 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
--- 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
--- 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"))
--- 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,