# HG changeset patch # User wenzelm # Date 1663331202 -7200 # Node ID a3c694039fd67ca1dca292d778b30ffdfe0630a3 # Parent aab9bb081f01a0aac23fdee9bd44624ec740a440 discontinued pointless SSH.Target: OpenSSH client can handle user@host directly; diff -r aab9bb081f01 -r a3c694039fd6 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Fri Sep 16 14:02:02 2022 +0200 +++ b/src/Pure/Admin/build_release.scala Fri Sep 16 14:26:42 2022 +0200 @@ -231,14 +231,10 @@ " (" + server_option + " = " + quote(server) + ") ...") val ssh = - server match { - case "" => - if (Platform.family == platform) SSH.Local - else error("Undefined option " + server_option + ": cannot build heaps") - case SSH.Target(user, host) => - SSH.open_session(options, host = host, user = user) - case _ => error("Malformed option " + server_option + ": " + quote(server)) - } + if (server.nonEmpty) SSH.open_session(options, server) + else if (Platform.family == platform) SSH.Local + else error("Undefined option " + server_option + ": cannot build heaps") + try { Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar => execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") diff -r aab9bb081f01 -r a3c694039fd6 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Fri Sep 16 14:02:02 2022 +0200 +++ b/src/Pure/General/mercurial.scala Fri Sep 16 14:26:42 2022 +0200 @@ -467,40 +467,38 @@ /* remote repository */ - val remote_url = - remote match { - case _ if remote.startsWith("ssh://") => - val ssh_url = remote + "/" + repos_name + val remote_url = { + if (remote.startsWith("ssh://")) { + val ssh_url = remote + "/" + repos_name + + if (!remote_exists) { + try { local_hg.command("init", ssh_url, repository = false).check } + catch { case ERROR(msg) => progress.echo_warning(msg) } + } - if (!remote_exists) { - try { local_hg.command("init", ssh_url, repository = false).check } - catch { case ERROR(msg) => progress.echo_warning(msg) } + ssh_url + } + else { + val phabricator = Phabricator.API(remote) + + var repos = + phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { + if (remote_exists) { + error("Remote repository " + + quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") + } + else phabricator.create_repository(repos_name, short_name = repos_name) } - ssh_url - - case SSH.Target(user, host) => - val phabricator = Phabricator.API(user, host) + while (repos.importing) { + progress.echo("Awaiting remote repository ...") + Time.seconds(0.5).sleep() + repos = phabricator.the_repository(repos.phid) + } - var repos = - phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { - if (remote_exists) { - error("Remote repository " + - quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") - } - else phabricator.create_repository(repos_name, short_name = repos_name) - } - - while (repos.importing) { - progress.echo("Awaiting remote repository ...") - Time.seconds(0.5).sleep() - repos = phabricator.the_repository(repos.phid) - } - - repos.ssh_url - - case _ => error("Malformed remote specification " + quote(remote)) + repos.ssh_url } + } progress.echo("Remote repository " + quote(remote_url)) diff -r aab9bb081f01 -r a3c694039fd6 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Fri Sep 16 14:02:02 2022 +0200 +++ b/src/Pure/General/ssh.scala Fri Sep 16 14:26:42 2022 +0200 @@ -13,22 +13,6 @@ object SSH { - /* target machine: user@host syntax */ - - object Target { - def parse(s: String): (String, String) = { - val i = s.indexOf('@') - if (i <= 0) ("", s) - else (s.substring(0, i), s.substring(i + 1)) - } - - def unapplySeq(s: String): Option[List[String]] = { - val (user, host) = parse(s) - if (host.isEmpty) None else Some(List(user, host)) - } - } - - /* OpenSSH configuration and command-line */ // see https://linux.die.net/man/5/ssh_config diff -r aab9bb081f01 -r a3c694039fd6 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Fri Sep 16 14:02:02 2022 +0200 +++ b/src/Pure/System/components.scala Fri Sep 16 14:26:42 2022 +0200 @@ -221,68 +221,67 @@ } if ((publish && archives.nonEmpty) || update_components_sha1) { - options.string("isabelle_components_server") match { - case SSH.Target(user, host) => - using(SSH.open_session(options, host = host, user = user)) { ssh => - val components_dir = Path.explode(options.string("isabelle_components_dir")) - val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) + val server = options.string("isabelle_components_server") + if (server.isEmpty) error("Undefined option isabelle_components_server") - for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { - error("Bad remote directory: " + dir) - } + using(SSH.open_session(options, server)) { ssh => + val components_dir = Path.explode(options.string("isabelle_components_dir")) + val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) - if (publish) { - for (archive <- archives) { - val archive_name = archive.file_name - val name = Archive.get_name(archive_name) - val remote_component = components_dir + archive.base - val remote_contrib = contrib_dir + Path.explode(name) + for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { + error("Bad remote directory: " + dir) + } - // component archive - if (ssh.is_file(remote_component) && !force) { - error("Remote component archive already exists: " + remote_component) - } - progress.echo("Uploading " + archive_name) - ssh.write_file(remote_component, archive) + if (publish) { + for (archive <- archives) { + val archive_name = archive.file_name + val name = Archive.get_name(archive_name) + val remote_component = components_dir + archive.base + val remote_contrib = contrib_dir + Path.explode(name) - // contrib directory - val is_standard_component = - Isabelle_System.with_tmp_dir("component") { tmp_dir => - Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check - check_dir(tmp_dir + Path.explode(name)) - } - if (is_standard_component) { - if (ssh.is_dir(remote_contrib)) { - if (force) ssh.rm_tree(remote_contrib) - else error("Remote component directory already exists: " + remote_contrib) - } - progress.echo("Unpacking remote " + archive_name) - ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + - ssh.bash_path(remote_component)).check - } - else { - progress.echo_warning("No unpacking of non-standard component: " + archive_name) - } + // component archive + if (ssh.is_file(remote_component) && !force) { + error("Remote component archive already exists: " + remote_component) + } + progress.echo("Uploading " + archive_name) + ssh.write_file(remote_component, archive) + + // contrib directory + val is_standard_component = + Isabelle_System.with_tmp_dir("component") { tmp_dir => + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check + check_dir(tmp_dir + Path.explode(name)) } + if (is_standard_component) { + if (ssh.is_dir(remote_contrib)) { + if (force) ssh.rm_tree(remote_contrib) + else error("Remote component directory already exists: " + remote_contrib) + } + progress.echo("Unpacking remote " + archive_name) + ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + + ssh.bash_path(remote_component)).check } - - // remote SHA1 digests - if (update_components_sha1) { - val lines = - for { - entry <- ssh.read_dir(components_dir) - if ssh.is_file(components_dir + Path.basic(entry)) && - entry.endsWith(Archive.suffix) - } - yield { - progress.echo("Digesting remote " + entry) - ssh.execute("cd " + ssh.bash_path(components_dir) + - "; sha1sum " + Bash.string(entry)).check.out - } - write_components_sha1(read_components_sha1(lines)) + else { + progress.echo_warning("No unpacking of non-standard component: " + archive_name) } } - case s => error("Bad isabelle_components_server: " + quote(s)) + } + + // remote SHA1 digests + if (update_components_sha1) { + val lines = + for { + entry <- ssh.read_dir(components_dir) + if ssh.is_file(components_dir + Path.basic(entry)) && + entry.endsWith(Archive.suffix) + } + yield { + progress.echo("Digesting remote " + entry) + ssh.execute("cd " + ssh.bash_path(components_dir) + + "; sha1sum " + Bash.string(entry)).check.out + } + write_components_sha1(read_components_sha1(lines)) + } } } diff -r aab9bb081f01 -r a3c694039fd6 src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Fri Sep 16 14:02:02 2022 +0200 +++ b/src/Pure/Tools/phabricator.scala Fri Sep 16 14:26:42 2022 +0200 @@ -889,23 +889,20 @@ /* context for operations */ - def apply(user: String, host: String, port: Int = default_system_port): API = - new API(user, host, port) + def apply(ssh_target: String, ssh_port: Int = default_system_port): API = + new API(ssh_target, ssh_port) } - final class API private(ssh_user: String, ssh_host: String, ssh_port: Int) { + final class API private(ssh_target: String, ssh_port: Int) { /* connection */ - require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port") - - private def ssh_user_prefix: String = - if (ssh_user.nonEmpty) ssh_user + "@" else "" + require(ssh_target.nonEmpty && ssh_port >= 0, "bad ssh host or port") private def ssh_port_suffix: String = if (ssh_port != default_system_port) ":" + ssh_port else "" - override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix - def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix + override def toString: String = ssh_target + ssh_port_suffix + def hg_url: String = "ssh://" + ssh_target + ssh_port_suffix /* execute methods */ @@ -915,7 +912,7 @@ File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params)))) val result = Isabelle_System.bash( - "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) + + "ssh -p " + ssh_port + " " + Bash.string(ssh_target) + " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check JSON.parse(result.out, strict = false) }