# HG changeset patch # User wenzelm # Date 1717186771 -7200 # Node ID 18a36de467bcf5c0c345895e1cdcee7da54e5cdb # Parent 0604d3051eee82271a16ca7ada8983f19afef3df# Parent 0d89f0a398541392b5ae5b47ab30f0e9efcd7606 merged diff -r 0604d3051eee -r 18a36de467bc lib/scripts/download_file --- a/lib/scripts/download_file Wed May 29 18:13:05 2024 +0200 +++ b/lib/scripts/download_file Fri May 31 22:19:31 2024 +0200 @@ -16,20 +16,10 @@ return 2 } - local CURL_OPTIONS="--fail --silent --location" - if [ "$(uname -s)" = "Darwin" ] - then - case $(sw_vers -productVersion) in - 10.*) - CURL_OPTIONS="$CURL_OPTIONS --insecure" - ;; - esac - fi - echo "Getting \"$REMOTE\"" mkdir -p "$(dirname "$LOCAL")" - if curl $CURL_OPTIONS "$REMOTE" > "${LOCAL}.part" + if curl --fail --silent --location "$REMOTE" > "${LOCAL}.part" then mv -f "${LOCAL}.part" "$LOCAL" else diff -r 0604d3051eee -r 18a36de467bc src/Pure/Admin/component_bash_process.scala --- a/src/Pure/Admin/component_bash_process.scala Wed May 29 18:13:05 2024 +0200 +++ b/src/Pure/Admin/component_bash_process.scala Fri May 31 22:19:31 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 0604d3051eee -r 18a36de467bc src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Wed May 29 18:13:05 2024 +0200 +++ b/src/Pure/General/ssh.scala Fri May 31 22:19:31 2024 +0200 @@ -1,7 +1,7 @@ /* Title: Pure/General/ssh.scala Author: Makarius -SSH client on OpenSSH command-line tools, preferably with connection +SSH client on top of OpenSSH command-line tools, preferably with connection multiplexing, but this does not work on Windows. */ @@ -123,7 +123,7 @@ override def ssh_session: Option[Session] = Some(ssh) def port_suffix: String = if (port > 0) ":" + port else "" - def user_prefix: String = if (user.nonEmpty) user + "@" else "" + def user_prefix: String = if_proper(user, user + "@") override def toString: String = user_prefix + host + port_suffix override def print: String = " (ssh " + toString + ")" @@ -135,28 +135,20 @@ /* local ssh commands */ - def run_command(command: String, + def make_command( + command: String = "ssh", master: Boolean = false, opts: String = "", - args: String = "", - cwd: JFile = null, - redirect: Boolean = false, - progress_stdout: String => Unit = (_: String) => (), - progress_stderr: String => Unit = (_: String) => (), - strict: Boolean = true - ): Process_Result = { + args_host: Boolean = false, + args: String = "" + ): String = { val config = Config.make(options, port = port, user = user, control_master = master, control_path = control_path) - val cmd = - Config.command(command, config) + + val args1 = if_proper(args_host, Bash.string(host) + if_proper(args, " ")) + args + Config.command(command, config) + if_proper(opts, " " + opts) + - if_proper(args, " -- " + args) - Isabelle_System.bash(cmd, cwd = cwd, - redirect = redirect, - progress_stdout = progress_stdout, - progress_stderr = progress_stderr, - strict = strict) + if_proper(args1, " -- " + args1) } def run_sftp( @@ -164,20 +156,19 @@ init: Path => Unit = _ => (), exit: Path => Unit = _ => () ): Process_Result = { - Isabelle_System.with_tmp_dir("ssh") { dir => + Isabelle_System.with_tmp_dir("sftp") { dir => init(dir) File.write(dir + Path.explode("script"), script) val result = - run_command("sftp", opts = "-b script", args = Bash.string(host), cwd = dir.file).check + Isabelle_System.bash( + make_command("sftp", opts = "-b script", args_host = true), cwd = dir.file).check exit(dir) result } } - def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = { - val args1 = Bash.string(host) + if_proper(args, " " + args) - run_command("ssh", master = master, opts = opts, args = args1) - } + def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = + Isabelle_System.bash(make_command(master = master, opts = opts, args_host = true, args = args)) /* init and exit */ @@ -217,16 +208,22 @@ /* remote commands */ - override def execute(cmd_line: String, + 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) => (), redirect: Boolean = false, 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(script), + val remote_script1 = Isabelle_System.export_env(user_home = user_home) + remote_script + Isabelle_System.bash(make_command(args_host = true, args = Bash.string(remote_script1)), progress_stdout = progress_stdout, progress_stderr = progress_stderr, redirect = redirect, @@ -268,10 +265,14 @@ override def eq_file(path1: Path, path2: Path): Boolean = path1 == path2 || execute("test " + bash_path(path1) + " -ef " + bash_path(path2)).ok - override def delete(path: Path): Unit = { - val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else "" - if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path)) - } + override def delete(paths: Path*): Unit = + if (paths.nonEmpty) { + val script = + "set -e\n" + + "for X in " + paths.iterator.map(bash_path).mkString(" ") + "\n" + + """do if test -d "$X"; then rmdir "$X"; else rm -f "$X"; fi; done""" + execute(script).check + } override def restrict(path: Path): Unit = if (!execute("chmod g-rwx,o-rwx " + bash_path(path)).ok) { @@ -331,20 +332,32 @@ put_file(path, File.write(_, text)) - /* tmp dirs */ + /* tmp dirs and files */ - override def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) + override def rm_tree(dir: Path): Unit = + execute("rm -r -f " + bash_path(dir)).check + + override def tmp_dir(): Path = + Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out) - def rm_tree(remote_dir: String): Unit = - execute("rm -r -f " + Bash.string(remote_dir)).check + override def tmp_file(name: String, ext: String = ""): Path = { + val file_name = name + "-XXXXXXXXXXXX" + if_proper(ext, "." + ext) + Path.explode(execute("mktemp /tmp/" + Bash.string(file_name)).check.out) + } - def tmp_dir(): String = - execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out + override def tmp_files(names: List[String]): List[Path] = { + val script = names.map(name => "mktemp /tmp/" + Bash.string(name) + "-XXXXXXXXXXXX") + Library.trim_split_lines(execute(script.mkString(" && ")).check.out).map(Path.explode) + } override def with_tmp_dir[A](body: Path => A): A = { - val remote_dir = tmp_dir() - try { body(Path.explode(remote_dir)) } - finally { rm_tree(remote_dir) } + val path = tmp_dir() + try { body(path) } finally { rm_tree(path) } + } + + override def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { + val path = tmp_file(name, ext = ext) + try { body(path) } finally { delete(path) } } @@ -376,7 +389,7 @@ " " + Config.option("PermitLocalCommand", true) + " " + Config.option("LocalCommand", "pwd") try { - run_command("ssh", opts = opts, args = Bash.string(host), + Isabelle_System.bash(make_command(opts = opts, args_host = true), progress_stdout = _ => result.change(_ => Exn.Res(true))).check } catch { case exn: Throwable => result.change(_ => Exn.Exn(exn)) } @@ -497,13 +510,19 @@ def is_dir(path: Path): Boolean = path.is_dir def is_file(path: Path): Boolean = path.is_file def eq_file(path1: Path, path2: Path): Boolean = File.eq(path1, path2) - def delete(path: Path): Unit = path.file.delete + def delete(paths: Path*): Unit = paths.foreach(path => path.file.delete) def restrict(path: Path): Unit = File.restrict(path) def set_executable(path: Path, reset: Boolean = false): Unit = File.set_executable(path, reset = reset) def make_directory(path: Path): Path = Isabelle_System.make_directory(path) def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir) + def tmp_dir(): Path = File.path(Isabelle_System.tmp_dir("tmp")) def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body) + def tmp_file(name: String, ext: String = ""): Path = + File.path(Isabelle_System.tmp_file(name, ext = ext)) + def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = + Isabelle_System.with_tmp_file(name, ext = ext)(body) + def tmp_files(names: List[String]): List[Path] = names.map(tmp_file(_)) def read_dir(path: Path): List[String] = File.read_dir(path) def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) @@ -513,6 +532,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 0604d3051eee -r 18a36de467bc src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Wed May 29 18:13:05 2024 +0200 +++ b/src/Pure/System/bash.scala Fri May 31 22:19:31 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,49 @@ ) { 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 List(timing_file, script_file) = + ssh.tmp_files(List("bash_timing", "bash_script")) + 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 + 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 +144,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 +177,7 @@ } def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { - isabelle.setup.Environment.kill_process(group_pid, "INT") + ssh.kill_process(group_pid, "INT") } @@ -154,25 +189,26 @@ private def do_cleanup(): Unit = { Isabelle_System.remove_shutdown_hook(shutdown_hook) - script_file.delete() winpid_file.foreach(_.delete()) + ssh_file.foreach(_.delete()) timing.change { case None => - if (timing_file.isFile) { - val t = - Word.explode(File.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 - Some(t) - } - else Some(Timing.zero) + val timing_text = + try { ssh.read(timing_file) } + catch { case ERROR(_) => "" } + val t = + Word.explode(timing_text) match { + case List(Value.Long(elapsed), Value.Long(cpu)) => + Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) + case _ => Timing.zero + } + Some(t) case some => some } + ssh.delete(timing_file, script_file) + cleanup() } diff -r 0604d3051eee -r 18a36de467bc src/Pure/System/components.scala --- a/src/Pure/System/components.scala Wed May 29 18:13:05 2024 +0200 +++ b/src/Pure/System/components.scala Fri May 31 22:19:31 2024 +0200 @@ -153,7 +153,8 @@ val base_name = local_dir.expand.base val local_directory = Directory(local_dir).check val remote_directory = Directory(base_dir + base_name, ssh = ssh) - if (!remote_directory.ok) { + if (remote_directory.ok) remote_directory + else { progress.echo("Providing " + base_name + ssh.print) Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar => ssh.with_tmp_dir { remote_tmp_dir => @@ -166,8 +167,8 @@ "tar -C " + ssh.bash_path(remote_dir) + " -xf " + ssh.bash_path(remote_tmp_tar)).check } } + remote_directory.check } - remote_directory.check } @@ -253,12 +254,12 @@ ssh.is_file(settings) || ssh.is_file(components) || Sessions.is_session_dir(path, ssh = ssh) def check: Directory = - if (!ssh.is_dir(path)) error("Bad component directory: " + toString) - else if (!ok) { + if (ok) this + else if (!ssh.is_dir(path)) error("Bad component directory: " + toString) + else { error("Malformed component directory: " + toString + "\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")") } - else this def read_components(): List[String] = split_lines(ssh.read(components)).filter(_.nonEmpty) diff -r 0604d3051eee -r 18a36de467bc src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Wed May 29 18:13:05 2024 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri May 31 22:19:31 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) }