src/Pure/General/ssh.scala
author wenzelm
Wed, 14 Sep 2022 15:57:47 +0200
changeset 76150 5c971c7fc807
parent 76149 ccc748255342
child 76151 21492610ae5b
permissions -rw-r--r--
more robust;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/ssh.scala
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     3
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
     4
SSH client on OpenSSH command-line tools, preferably with connection
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
     5
multiplexing, but this does not work on Windows.
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     6
*/
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     7
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     8
package isabelle
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
     9
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    10
73909
1d0d9772fff0 tuned imports;
wenzelm
parents: 73897
diff changeset
    11
import java.util.{Map => JMap}
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    12
import java.net.ServerSocket
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    13
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    14
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    15
object SSH {
64185
wenzelm
parents: 64166
diff changeset
    16
  /* target machine: user@host syntax */
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    17
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    18
  object Target {
76128
wenzelm
parents: 76125
diff changeset
    19
    def parse(s: String): (String, String) = {
wenzelm
parents: 76125
diff changeset
    20
      val i = s.indexOf('@')
wenzelm
parents: 76125
diff changeset
    21
      if (i <= 0) ("", s)
wenzelm
parents: 76125
diff changeset
    22
      else (s.substring(0, i), s.substring(i + 1))
wenzelm
parents: 76125
diff changeset
    23
    }
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    24
76128
wenzelm
parents: 76125
diff changeset
    25
    def unapplySeq(s: String): Option[List[String]] = {
wenzelm
parents: 76125
diff changeset
    26
      val (user, host) = parse(s)
wenzelm
parents: 76125
diff changeset
    27
      if (host.isEmpty) None else Some(List(user, host))
wenzelm
parents: 76125
diff changeset
    28
    }
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    29
  }
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    30
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    31
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    32
  /* OpenSSH configuration and command-line */
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    33
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    34
  // see https://linux.die.net/man/5/ssh_config
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    35
  object Config {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    36
    def entry(x: String, y: String): String = x + "=" + y
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    37
    def entry(x: String, y: Int): String = entry(x, y.toString)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    38
    def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no")
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    39
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    40
    def make(options: Options,
76131
8b695e59db3f clarified default: do not override port from ssh_config, which could be different from 22;
wenzelm
parents: 76130
diff changeset
    41
      port: Int = 0,
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    42
      user: String = "",
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    43
      control_master: Boolean = false,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    44
      control_path: String = ""
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    45
    ): List[String] = {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    46
      List("BatchMode=yes",
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    47
        entry("ConnectTimeout", options.seconds("ssh_connect_timeout").ms.toInt),
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    48
        entry("ServerAliveInterval", options.seconds("ssh_alive_interval").ms.toInt),
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    49
        entry("ServerAliveCountMax", options.int("ssh_alive_count_max")),
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    50
        entry("Compression", options.bool("ssh_compression"))) :::
76131
8b695e59db3f clarified default: do not override port from ssh_config, which could be different from 22;
wenzelm
parents: 76130
diff changeset
    51
      (if (port > 0) List(entry("Port", port)) else Nil) :::
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    52
      (if (user.nonEmpty) List(entry("User", user)) else Nil) :::
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    53
      (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) :::
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    54
      (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    55
    }
64325
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    56
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    57
    def option(entry: String): String = "-o " + Bash.string(entry)
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    58
    def option(x: String, y: String): String = option(entry(x, y))
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    59
    def option(x: String, y: Int): String = option(entry(x, y))
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    60
    def option(x: String, y: Boolean): String = option(entry(x, y))
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    61
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    62
    def command(command: String, config: List[String]): String =
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    63
      Bash.string(command) + config.map(entry => " " + option(entry)).mkString
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    64
  }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    65
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    66
  def sftp_string(str: String): String = {
76150
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    67
    val special = "[]?*\\{} \"'"
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    68
    if (str.isEmpty) "\"\""
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    69
    else if (str.exists(special.contains)) {
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    70
      val res = new StringBuilder
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    71
      for (c <- str) {
76150
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    72
        if (special.contains(c)) res += '\\'
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    73
        res += c
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    74
      }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    75
      res.toString()
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    76
    }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    77
    else str
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    78
  }
67273
c573cfb2c407 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents: 67067
diff changeset
    79
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    80
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    81
  /* open session */
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    82
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    83
  def open_session(
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    84
    options: Options,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    85
    host: String,
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    86
    port: Int = 0,
76148
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
    87
    user: String = ""
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    88
  ): Session = {
76148
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
    89
    val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    90
    val (control_master, control_path) =
76144
35a279a2d246 clarified signature;
wenzelm
parents: 76142
diff changeset
    91
      if (multiplex) (true, Isabelle_System.tmp_file("ssh_socket", initialized = false).getPath)
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    92
      else (false, "")
76131
8b695e59db3f clarified default: do not override port from ssh_config, which could be different from 22;
wenzelm
parents: 76130
diff changeset
    93
    new Session(options, host, port, user, control_master, control_path)
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
    94
  }
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
    95
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    96
  class Session private[SSH](
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    97
    val options: Options,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    98
    val host: String,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    99
    val port: Int,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   100
    val user: String,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   101
    control_master: Boolean,
76136
1bb677cceea4 let rsync re-use ssh connection via control path;
wenzelm
parents: 76133
diff changeset
   102
    val control_path: String
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   103
  ) extends System {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   104
    ssh =>
64128
wenzelm
parents: 64127
diff changeset
   105
76133
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   106
    def port_suffix: String = if (port > 0) ":" + port else ""
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   107
    def user_prefix: String = if (user.nonEmpty) user + "@" else ""
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   108
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   109
    override def toString: String = user_prefix + host + port_suffix
76132
2bb6eb6df6c2 proper port for Mercurial;
wenzelm
parents: 76131
diff changeset
   110
    override def hg_url: String = "ssh://" + toString + "/"
76133
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   111
    override def rsync_prefix: String = user_prefix + host + ":"
64191
wenzelm
parents: 64190
diff changeset
   112
wenzelm
parents: 64190
diff changeset
   113
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   114
    /* local ssh commands */
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   115
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   116
    def run_command(command: String,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   117
      master: Boolean = false,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   118
      opts: String = "",
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   119
      args: String = "",
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   120
      progress_stdout: String => Unit = (_: String) => (),
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   121
      progress_stderr: String => Unit = (_: String) => (),
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   122
      strict: Boolean = true
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   123
    ): Process_Result = {
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   124
      val config =
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   125
        Config.make(options, port = port, user = user,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   126
          control_master = master, control_path = control_path)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   127
      val cmd =
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   128
        Config.command(command, config) +
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   129
        (if (opts.nonEmpty) " " + opts else "") +
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   130
        (if (args.nonEmpty) " -- " + args else "")
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   131
      Isabelle_System.bash(cmd, progress_stdout = progress_stdout,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   132
        progress_stderr = progress_stderr, strict = strict)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   133
    }
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   134
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   135
    def run_sftp(script: String, opts: String = "", args: String = ""): Process_Result = {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   136
      Isabelle_System.with_tmp_file("sftp") { tmp_path =>
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   137
        File.write(tmp_path, script)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   138
        val opts1 = "-b " + File.bash_path(tmp_path) + (if (opts.nonEmpty) " " + opts else "")
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   139
        val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   140
        run_command("sftp", opts = opts1, args = args1)
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   141
      }
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   142
    }
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   143
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   144
    def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   145
      val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   146
      run_command("ssh", master = master, opts = opts, args = args1)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   147
    }
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   148
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   149
    def run_scp(opts: String = "", args: String = ""): Process_Result = {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   150
      val opts1 = "-s -p -q" + (if (opts.nonEmpty) " " + opts else "")
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   151
      run_command("scp", opts = opts1, args = args)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   152
    }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   153
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   154
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   155
    /* init and exit */
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   156
76149
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   157
    val user_home: String =
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   158
      run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   159
      match {
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   160
        case List(user_home, shell) =>
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   161
          if (shell.endsWith("/bash")) user_home
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   162
          else {
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   163
            error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell)
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   164
          }
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   165
        case _ => error("Malformed remote environment for " + quote(toString))
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   166
      }
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   167
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   168
    val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   169
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   170
    override def close(): Unit = {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   171
      if (control_path.nonEmpty) run_ssh(opts = "-O exit").check
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   172
    }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   173
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   174
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   175
    /* remote commands */
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   176
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   177
    override def execute(cmd_line: String,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   178
      progress_stdout: String => Unit = (_: String) => (),
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   179
      progress_stderr: String => Unit = (_: String) => (),
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   180
      settings: Boolean = true,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   181
      strict: Boolean = true
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   182
    ): Process_Result = {
76142
e8d4013c49d1 more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;
wenzelm
parents: 76136
diff changeset
   183
      val args1 =
e8d4013c49d1 more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;
wenzelm
parents: 76136
diff changeset
   184
        Bash.string(host) + " export " + Bash.string("USER_HOME=\"$HOME\"") + "\n" + cmd_line
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   185
      run_command("ssh", args = args1, progress_stdout = progress_stdout,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   186
        progress_stderr = progress_stderr, strict = strict)
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   187
    }
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   188
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   189
    override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   190
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   191
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   192
    /* remote file-system */
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   193
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   194
    override def expand_path(path: Path): Path = path.expand_env(settings)
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   195
    def remote_path(path: Path): String = expand_path(path).implode
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   196
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   197
    override def bash_path(path: Path): String = Bash.string(remote_path(path))
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   198
    def sftp_path(path: Path): String = sftp_string(remote_path(path))
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   199
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   200
    def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path)).check
69300
8b6ab9989bcd is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents: 67771
diff changeset
   201
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   202
    override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   203
    override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok
69300
8b6ab9989bcd is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents: 67771
diff changeset
   204
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   205
    override def make_directory(path: Path): Path = {
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   206
      if (!execute("mkdir -p " + bash_path(path)).ok) {
76118
e8e3b60d8ecd clarified operation: avoid perl;
wenzelm
parents: 76117
diff changeset
   207
        error("Failed to create directory: " + quote(remote_path(path)))
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   208
      }
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   209
      path
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   210
    }
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   211
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   212
    def read_dir(path: Path): List[String] =
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   213
      run_sftp("ls -1 -a " + sftp_path(path)).check.out_lines.flatMap(s =>
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   214
        if (s == "." || s == ".." || s.endsWith("/.") || s.endsWith("/..")) None
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   215
        else Some(Library.perhaps_unprefix("./", s)))
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   216
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   217
    override def read_file(path: Path, local_path: Path): Unit =
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   218
      run_scp(args = Bash.string(host + ":" + remote_path(path)) + " " +
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   219
        File.bash_platform_path(local_path)).check
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   220
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   221
    override def read_bytes(path: Path): Bytes =
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   222
      Isabelle_System.with_tmp_file("scp") { local_path =>
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   223
        read_file(path, local_path)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   224
        Bytes.read(local_path)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   225
      }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   226
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   227
    override def read(path: Path): String = read_bytes(path).text
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   228
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   229
    override def write_file(path: Path, local_path: Path): Unit =
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   230
      run_scp(args = File.bash_platform_path(local_path) + " " +
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   231
        Bash.string(host + ":" + remote_path(path))).check
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   232
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   233
    def write_bytes(path: Path, bytes: Bytes): Unit =
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   234
      Isabelle_System.with_tmp_file("scp") { local_path =>
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   235
        Bytes.write(local_path, bytes)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   236
        write_file(path, local_path)
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   237
      }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   238
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   239
    def write(path: Path, text: String): Unit = write_bytes(path, Bytes(text))
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents: 71780
diff changeset
   240
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   241
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   242
    /* tmp dirs */
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   243
64306
7b6dc1b36f20 tuned signature, in accordance to Isabelle_System;
wenzelm
parents: 64304
diff changeset
   244
    def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))
7b6dc1b36f20 tuned signature, in accordance to Isabelle_System;
wenzelm
parents: 64304
diff changeset
   245
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   246
    def rm_tree(remote_dir: String): Unit =
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64258
diff changeset
   247
      execute("rm -r -f " + Bash.string(remote_dir)).check
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   248
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   249
    def tmp_dir(): String =
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   250
      execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   251
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   252
    override def with_tmp_dir[A](body: Path => A): A = {
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   253
      val remote_dir = tmp_dir()
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   254
      try { body(Path.explode(remote_dir)) }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   255
      finally { rm_tree(remote_dir) }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   256
    }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   257
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   258
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   259
    /* port forwarding */
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   260
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   261
    def port_forwarding(
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   262
      remote_port: Int,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   263
      remote_host: String = "localhost",
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   264
      local_port: Int = 0,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   265
      local_host: String = "localhost",
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   266
      ssh_close: Boolean = false
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   267
    ): Port_Forwarding = {
76145
a6bdf4b889ca clarified signature;
wenzelm
parents: 76144
diff changeset
   268
      val port = if (local_port > 0) local_port else Isabelle_System.local_port()
a6bdf4b889ca clarified signature;
wenzelm
parents: 76144
diff changeset
   269
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   270
      val forward = List(local_host, port, remote_host, remote_port).mkString(":")
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   271
      val forward_option = "-L " + Bash.string(forward)
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   272
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   273
      val cancel: () => Unit =
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   274
        if (control_path.nonEmpty) {
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   275
          run_ssh(opts = forward_option + " -O forward").check
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   276
          () => run_ssh(opts = forward_option + " -O cancel")  // permissive
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   277
        }
76148
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   278
        else {
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   279
          val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false))
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   280
          val thread = Isabelle_Thread.fork("port_forwarding") {
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   281
            val opts =
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   282
              forward_option +
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   283
                " " + Config.option("SessionType", "none") +
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   284
                " " + Config.option("PermitLocalCommand", true) +
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   285
                " " + Config.option("LocalCommand", "pwd")
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   286
            try {
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   287
              run_command("ssh", opts = opts, args = Bash.string(host),
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   288
                progress_stdout = _ => result.change(_ => Exn.Res(true))).check
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   289
            }
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   290
            catch { case exn: Throwable => result.change(_ => Exn.Exn(exn)) }
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   291
          }
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   292
          result.guarded_access {
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   293
            case res@Exn.Res(ok) => if (ok) Some((), res) else None
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   294
            case Exn.Exn(exn) => throw exn
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   295
          }
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   296
          () => thread.interrupt()
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   297
        }
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   298
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   299
      val shutdown_hook =
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   300
        Isabelle_System.create_shutdown_hook { cancel() }
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   301
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   302
      new Port_Forwarding(host, port, remote_host, remote_port) {
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   303
        override def toString: String = forward
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   304
        override def close(): Unit = {
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   305
          cancel()
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   306
          Isabelle_System.remove_shutdown_hook(shutdown_hook)
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   307
          if (ssh_close) ssh.close()
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   308
        }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   309
      }
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   310
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   311
  }
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   312
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   313
  abstract class Port_Forwarding private[SSH](
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   314
    val host: String,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   315
    val port: Int,
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   316
    val remote_host: String,
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   317
    val remote_port: Int
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   318
  ) extends AutoCloseable
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   319
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   320
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   321
  /* system operations */
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   322
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   323
  trait System extends AutoCloseable {
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   324
    def close(): Unit = ()
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   325
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   326
    def hg_url: String = ""
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   327
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   328
    def rsync_prefix: String = ""
75517
292d7a9dc8a3 proper operation on String, not Path;
wenzelm
parents: 75513
diff changeset
   329
    def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   330
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   331
    def expand_path(path: Path): Path = path.expand
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   332
    def bash_path(path: Path): String = File.bash_path(path)
69300
8b6ab9989bcd is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
wenzelm
parents: 67771
diff changeset
   333
    def is_dir(path: Path): Boolean = path.is_dir
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   334
    def is_file(path: Path): Boolean = path.is_file
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   335
    def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   336
    def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   337
    def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   338
    def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
75513
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   339
    def read_bytes(path: Path): Bytes = Bytes.read(path)
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   340
    def read(path: Path): String = File.read(path)
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   341
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   342
    def execute(command: String,
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   343
        progress_stdout: String => Unit = (_: String) => (),
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   344
        progress_stderr: String => Unit = (_: String) => (),
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   345
        settings: Boolean = true,
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   346
        strict: Boolean = true): Process_Result =
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   347
      Isabelle_System.bash(command,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   348
        progress_stdout = progress_stdout,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   349
        progress_stderr = progress_stderr,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   350
        env = if (settings) Isabelle_System.settings() else null,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   351
        strict = strict)
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents: 71780
diff changeset
   352
72340
676066aa4798 clarified signature;
wenzelm
parents: 72338
diff changeset
   353
    def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   354
  }
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   355
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   356
  object Local extends System
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   357
}