--- 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
--- 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(
--- 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) => (),
--- 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()
}
--- 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)
--- 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)
}