src/Pure/General/ssh.scala

misc tuning and clarification;
proper shutdown_hook;

/*  Title:      Pure/General/ssh.scala
    Author:     Makarius

SSH client on OpenSSH command-line tools, preferably with connection
multiplexing, but this does not work on Windows.
*/

package isabelle


import java.util.{Map => JMap}
import java.net.ServerSocket


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
  object Config {
    def entry(x: String, y: String): String = x + "=" + y
    def entry(x: String, y: Int): String = entry(x, y.toString)
    def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no")

    def make(options: Options,
      port: Int = 0,
      user: String = "",
      control_master: Boolean = false,
      control_path: String = ""
    ): List[String] = {
      List("BatchMode=yes",
        entry("ConnectTimeout", options.seconds("ssh_connect_timeout").ms.toInt),
        entry("ServerAliveInterval", options.seconds("ssh_alive_interval").ms.toInt),
        entry("ServerAliveCountMax", options.int("ssh_alive_count_max")),
        entry("Compression", options.bool("ssh_compression"))) :::
      (if (port > 0) List(entry("Port", port)) else Nil) :::
      (if (user.nonEmpty) List(entry("User", user)) else Nil) :::
      (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) :::
      (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil)
    }

    def option(entry: String): String = "-o " + Bash.string(entry)
    def option(x: String, y: String): String = option(entry(x, y))
    def option(x: String, y: Int): String = option(entry(x, y))
    def option(x: String, y: Boolean): String = option(entry(x, y))

    def command(command: String, config: List[String]): String =
      Bash.string(command) + config.map(entry => " " + option(entry)).mkString
  }

  def sftp_string(str: String): String = {
    val special = Set(' ', '*', '?', '{', '}')
    if (str.exists(special)) {
      val res = new StringBuilder
      for (c <- str) {
        if (special(c)) res += '\\'
        res += c
      }
      res.toString()
    }
    else str
  }


  /* open session */

  def open_session(
    options: Options,
    host: String,
    port: Int = 0,
    user: String = "",
    multiplex: Boolean = !Platform.is_windows
  ): Session = {
    val (control_master, control_path) =
      if (multiplex) (true, Isabelle_System.tmp_file("ssh_socket", initialized = false).getPath)
      else (false, "")
    new Session(options, host, port, user, control_master, control_path)
  }

  class Session private[SSH](
    val options: Options,
    val host: String,
    val port: Int,
    val user: String,
    control_master: Boolean,
    val control_path: String
  ) extends System {
    ssh =>

    def port_suffix: String = if (port > 0) ":" + port else ""
    def user_prefix: String = if (user.nonEmpty) user + "@" else ""

    override def toString: String = user_prefix + host + port_suffix
    override def hg_url: String = "ssh://" + toString + "/"
    override def rsync_prefix: String = user_prefix + host + ":"


    /* local ssh commands */

    def run_command(command: String,
      master: Boolean = false,
      opts: String = "",
      args: String = "",
      progress_stdout: String => Unit = (_: String) => (),
      progress_stderr: String => Unit = (_: String) => (),
      strict: Boolean = true
    ): Process_Result = {
      val config =
        Config.make(options, port = port, user = user,
          control_master = master, control_path = control_path)
      val cmd =
        Config.command(command, config) +
        (if (opts.nonEmpty) " " + opts else "") +
        (if (args.nonEmpty) " -- " + args else "")
      Isabelle_System.bash(cmd, progress_stdout = progress_stdout,
        progress_stderr = progress_stderr, strict = strict)
    }

    def run_sftp(script: String, opts: String = "", args: String = ""): Process_Result = {
      Isabelle_System.with_tmp_file("sftp") { tmp_path =>
        File.write(tmp_path, script)
        val opts1 = "-b " + File.bash_path(tmp_path) + (if (opts.nonEmpty) " " + opts else "")
        val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
        run_command("sftp", opts = opts1, args = args1)
      }
    }

    def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
      val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
      run_command("ssh", master = master, opts = opts, args = args1)
    }

    def run_scp(opts: String = "", args: String = ""): Process_Result = {
      val opts1 = "-s -p -q" + (if (opts.nonEmpty) " " + opts else "")
      run_command("scp", opts = opts1, args = args)
    }


    /* init and exit */

    val user_home: String = run_ssh(master = control_master, args = "printenv HOME").check.out

    val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)

    override def close(): Unit = {
      if (control_path.nonEmpty) run_ssh(opts = "-O exit").check
    }


    /* remote commands */

    override def execute(cmd_line: String,
      progress_stdout: String => Unit = (_: String) => (),
      progress_stderr: String => Unit = (_: String) => (),
      settings: Boolean = true,
      strict: Boolean = true
    ): Process_Result = {
      val args1 =
        Bash.string(host) + " export " + Bash.string("USER_HOME=\"$HOME\"") + "\n" + cmd_line
      run_command("ssh", args = args1, progress_stdout = progress_stdout,
        progress_stderr = progress_stderr, strict = strict)
    }

    override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))


    /* remote file-system */

    override def expand_path(path: Path): Path = path.expand_env(settings)
    def remote_path(path: Path): String = expand_path(path).implode

    override def bash_path(path: Path): String = Bash.string(remote_path(path))
    def sftp_path(path: Path): String = sftp_string(remote_path(path))

    def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path)).check

    override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok
    override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok

    override def make_directory(path: Path): Path = {
      if (!execute("mkdir -p " + bash_path(path)).ok) {
        error("Failed to create directory: " + quote(remote_path(path)))
      }
      path
    }

    def read_dir(path: Path): List[String] =
      run_sftp("ls -1 -a " + sftp_path(path)).check.out_lines.flatMap(s =>
        if (s == "." || s == ".." || s.endsWith("/.") || s.endsWith("/..")) None
        else Some(Library.perhaps_unprefix("./", s)))

    override def read_file(path: Path, local_path: Path): Unit =
      run_scp(args = Bash.string(host + ":" + remote_path(path)) + " " +
        File.bash_platform_path(local_path)).check

    override def read_bytes(path: Path): Bytes =
      Isabelle_System.with_tmp_file("scp") { local_path =>
        read_file(path, local_path)
        Bytes.read(local_path)
      }

    override def read(path: Path): String = read_bytes(path).text

    override def write_file(path: Path, local_path: Path): Unit =
      run_scp(args = File.bash_platform_path(local_path) + " " +
        Bash.string(host + ":" + remote_path(path))).check

    def write_bytes(path: Path, bytes: Bytes): Unit =
      Isabelle_System.with_tmp_file("scp") { local_path =>
        Bytes.write(local_path, bytes)
        write_file(path, local_path)
      }

    def write(path: Path, text: String): Unit = write_bytes(path, Bytes(text))


    /* tmp dirs */

    def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))

    def rm_tree(remote_dir: String): Unit =
      execute("rm -r -f " + Bash.string(remote_dir)).check

    def tmp_dir(): String =
      execute("mktemp -d -t tmp.XXXXXXXXXX").check.out

    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) }
    }


    /* port forwarding */

    def port_forwarding(
      remote_port: Int,
      remote_host: String = "localhost",
      local_port: Int = 0,
      local_host: String = "localhost",
      ssh_close: Boolean = false
    ): Port_Forwarding = {
      val port = if (local_port > 0) local_port else Isabelle_System.local_port()

      val forward = List(local_host, port, remote_host, remote_port).mkString(":")
      val forward_option = "-L " + Bash.string(forward)

      val cancel: () => Unit =
        if (control_path.nonEmpty) {
          run_ssh(opts = forward_option + " -O forward").check
          () => run_ssh(opts = forward_option + " -O cancel")  // permissive
        }
        else error("SSH port forwarding requires multiplexing")

      val shutdown_hook =
        Isabelle_System.create_shutdown_hook { cancel() }

      new Port_Forwarding(host, port, remote_host, remote_port) {
        override def toString: String = forward
        override def close(): Unit = {
          cancel()
          Isabelle_System.remove_shutdown_hook(shutdown_hook)
          if (ssh_close) ssh.close()
        }
      }
    }
  }

  abstract class Port_Forwarding private[SSH](
    val host: String,
    val port: Int,
    val remote_host: String,
    val remote_port: Int
  ) extends AutoCloseable


  /* system operations */

  trait System extends AutoCloseable {
    def close(): Unit = ()

    def hg_url: String = ""

    def rsync_prefix: String = ""
    def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode

    def expand_path(path: Path): Path = path.expand
    def bash_path(path: Path): String = File.bash_path(path)
    def is_dir(path: Path): Boolean = path.is_dir
    def is_file(path: Path): Boolean = path.is_file
    def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
    def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
    def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
    def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
    def read_bytes(path: Path): Bytes = Bytes.read(path)
    def read(path: Path): String = File.read(path)

    def execute(command: String,
        progress_stdout: String => Unit = (_: String) => (),
        progress_stderr: String => Unit = (_: String) => (),
        settings: Boolean = true,
        strict: Boolean = true): Process_Result =
      Isabelle_System.bash(command,
        progress_stdout = progress_stdout,
        progress_stderr = progress_stderr,
        env = if (settings) Isabelle_System.settings() else null,
        strict = strict)

    def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
  }

  object Local extends System
}