# HG changeset patch # User wenzelm # Date 1717181211 -7200 # Node ID 875968a3b2f92acd315a61754928f873aa0e5b81 # Parent e0606fb415d2e58b75a72fc6cc58b5e6027602b6 suport Isabelle_System.bash via SSH.System; diff -r e0606fb415d2 -r 875968a3b2f9 src/Pure/Admin/component_bash_process.scala --- a/src/Pure/Admin/component_bash_process.scala Fri May 31 15:56:41 2024 +0200 +++ b/src/Pure/Admin/component_bash_process.scala Fri May 31 20:46:51 2024 +0200 @@ -8,6 +8,16 @@ object Component_Bash_Process { + /* resources */ + + def home: Path = Path.explode("$ISABELLE_BASH_PROCESS_HOME") + + def remote_program(directory: Components.Directory): Path = { + val platform = directory.ssh.isabelle_platform.ISABELLE_PLATFORM(apple = true) + directory.path + Path.basic(platform) + Path.basic("bash_process") + } + + /* build bash_process */ def build_bash_process( diff -r e0606fb415d2 -r 875968a3b2f9 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Fri May 31 15:56:41 2024 +0200 +++ b/src/Pure/General/ssh.scala Fri May 31 20:46:51 2024 +0200 @@ -208,6 +208,13 @@ /* remote commands */ + override def kill_process(group_pid: String, signal: String): Boolean = { + val script = + make_command(args_host = true, + args = "kill -" + Bash.string(signal) + " -" + Bash.string(group_pid)) + Isabelle_System.bash(script).ok + } + override def execute(remote_script: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), @@ -515,6 +522,9 @@ def write_bytes(path: Path, bytes: Bytes): Unit = Bytes.write(path, bytes) def write(path: Path, text: String): Unit = File.write(path, text) + def kill_process(group_pid: String, signal: String): Boolean = + isabelle.setup.Environment.kill_process(Bash.string(group_pid), Bash.string(signal)) + def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), diff -r e0606fb415d2 -r 875968a3b2f9 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Fri May 31 15:56:41 2024 +0200 +++ b/src/Pure/System/bash.scala Fri May 31 20:46:51 2024 +0200 @@ -8,7 +8,7 @@ package isabelle -import java.util.{List => JList, Map => JMap} +import java.util.{List => JList, Map => JMap, LinkedList} import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile, IOException} import scala.annotation.tailrec @@ -48,19 +48,34 @@ private def make_description(description: String): String = proper_string(description) getOrElse "bash_process" + def local_bash_process(): String = + File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")) + + def local_bash(): String = + if (Platform.is_unix) "bash" + else isabelle.setup.Environment.cygwin_root() + "\\bin\\bash.exe" + + def remote_bash_process(ssh: SSH.Session): String = { + val component = Components.provide(Component_Bash_Process.home, ssh = ssh) + val exe = Component_Bash_Process.remote_program(component) + ssh.make_command(args_host = true, args = ssh.bash_path(exe)) + } + type Watchdog = (Time, Process => Boolean) def process(script: String, description: String = "", + ssh: SSH.System = SSH.Local, cwd: JFile = null, env: JMap[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => ()): Process = - new Process(script, description, cwd, env, redirect, cleanup) + new Process(script, description, ssh, cwd, env, redirect, cleanup) class Process private[Bash]( script: String, description: String, + ssh: SSH.System, cwd: JFile, env: JMap[String, String], redirect: Boolean, @@ -68,28 +83,48 @@ ) { override def toString: String = make_description(description) - private val timing_file = Isabelle_System.tmp_file("bash_timing") + private val proc_command: JList[String] = new LinkedList[String] + + private val winpid_file: Option[JFile] = + if (ssh.is_local && Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) + else None + private val winpid_script = + winpid_file match { + case None => "" + case Some(file) => + "read < /proc/self/winpid > /dev/null 2> /dev/null\n" + + """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + } + + private val timing_file = ssh.tmp_file("bash_timing") private val timing = Synchronized[Option[Timing]](None) def get_timing: Timing = timing.value getOrElse Timing.zero - private val winpid_file: Option[JFile] = - if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None - private val winpid_script = - winpid_file match { - case None => script - case Some(file) => - "read < /proc/self/winpid > /dev/null 2> /dev/null\n" + - """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script + private val script_file: Path = ssh.tmp_file("bash_script") + ssh.write(script_file, winpid_script + script) + + private val ssh_file: Option[JFile] = + ssh.ssh_session match { + case None => + proc_command.add(local_bash_process()) + proc_command.add(File.platform_path(timing_file)) + proc_command.add("bash") + proc_command.add(File.platform_path(script_file)) + None + case Some(ssh_session) => + val ssh_script = + "exec " + remote_bash_process(ssh_session) + " " + + ssh.bash_path(timing_file) + " bash " + + ssh.bash_path(script_file) + val file = Isabelle_System.tmp_file("bash_ssh") + File.write(file, ssh_script) + proc_command.add(local_bash()) + proc_command.add(file.getPath) + Some(file) } - private val script_file: JFile = Isabelle_System.tmp_file("bash_script") - File.write(script_file, winpid_script) - private val proc = - isabelle.setup.Environment.process_builder( - JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), - File.standard_path(timing_file), "bash", File.standard_path(script_file)), - cwd, env, redirect).start() + isabelle.setup.Environment.process_builder(proc_command, cwd, env, redirect).start() // channels @@ -108,27 +143,26 @@ private val group_pid = stdout.readLine - private def process_alive(pid: String): Boolean = - (for { - p <- Value.Long.unapply(pid) - handle <- ProcessHandle.of(p).toScala - } yield handle.isAlive) getOrElse false + private def local_process_alive(pid: String): Boolean = + ssh.is_local && + (for { + p <- Value.Long.unapply(pid) + handle <- ProcessHandle.of(p).toScala + } yield handle.isAlive).getOrElse(false) private def root_process_alive(): Boolean = winpid_file match { - case None => process_alive(group_pid) + case None => local_process_alive(group_pid) case Some(file) => - file.exists() && process_alive(Library.trim_line(File.read(file))) + file.exists() && local_process_alive(Library.trim_line(File.read(file))) } @tailrec private def signal(s: String, count: Int = 1): Boolean = { count <= 0 || { - isabelle.setup.Environment.kill_process(group_pid, s) - val running = - root_process_alive() || - isabelle.setup.Environment.kill_process(group_pid, "0") + ssh.kill_process(group_pid, s) + val running = root_process_alive() || ssh.kill_process(group_pid, "0") if (running) { - Time.seconds(0.1).sleep() + Time.seconds(if (ssh.is_local) 0.1 else 0.25).sleep() signal(s, count - 1) } else false @@ -142,7 +176,7 @@ } def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { - isabelle.setup.Environment.kill_process(group_pid, "INT") + ssh.kill_process(group_pid, "INT") } @@ -154,19 +188,21 @@ private def do_cleanup(): Unit = { Isabelle_System.remove_shutdown_hook(shutdown_hook) - script_file.delete() winpid_file.foreach(_.delete()) + ssh_file.foreach(_.delete()) + + ssh.delete(script_file) timing.change { case None => - if (timing_file.isFile) { + if (ssh.is_file(timing_file)) { val t = - Word.explode(File.read(timing_file)) match { + Word.explode(ssh.read(timing_file)) match { case List(Value.Long(elapsed), Value.Long(cpu)) => Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) case _ => Timing.zero } - timing_file.delete + ssh.delete(timing_file) Some(t) } else Some(Timing.zero) diff -r e0606fb415d2 -r 875968a3b2f9 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Fri May 31 15:56:41 2024 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri May 31 20:46:51 2024 +0200 @@ -414,6 +414,7 @@ def bash(script: String, description: String = "", + ssh: SSH.System = SSH.Local, cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false, @@ -424,8 +425,8 @@ strict: Boolean = true, cleanup: () => Unit = () => () ): Process_Result = { - Bash.process(script, - description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). + Bash.process(script, description = description, ssh = ssh, cwd = cwd, env = env, + redirect = redirect, cleanup = cleanup). result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) }