src/Pure/General/ssh.scala
author wenzelm
Fri, 31 May 2024 20:46:51 +0200
changeset 80218 875968a3b2f9
parent 80217 e0606fb415d2
child 80220 928e02d0cab7
permissions -rw-r--r--
suport Isabelle_System.bash via SSH.System;
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
80209
f2fa6753c3e2 tuned comments;
wenzelm
parents: 80189
diff changeset
     4
SSH client on top of OpenSSH command-line tools, preferably with connection
76122
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}
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
    12
import java.io.{File => JFile}
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    13
80189
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
    14
import scala.annotation.tailrec
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
    15
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    16
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
    17
object SSH {
76170
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    18
  /* client command */
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    19
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    20
  def client_command(port: Int = 0, control_path: String = ""): String =
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    21
    if (control_path.isEmpty || control_path == Bash.string(control_path)) {
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    22
      "ssh" +
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    23
        (if (port > 0) " -p " + port else "") +
77369
wenzelm
parents: 77130
diff changeset
    24
        if_proper(control_path, " -o ControlPath=" + control_path)
76170
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    25
    }
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    26
    else error ("Malformed SSH control socket: " + quote(control_path))
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    27
5912209b4fb6 clarified modules;
wenzelm
parents: 76169
diff changeset
    28
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    29
  /* 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
    30
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    31
  // 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
    32
  object Config {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    33
    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
    34
    def entry(x: String, y: Int): String = entry(x, y.toString)
76165
cf469736000c proper time values in seconds;
wenzelm
parents: 76164
diff changeset
    35
    def entry(x: String, y: Long): String = entry(x, y.toString)
76122
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: Boolean): String = entry(x, if (y) "yes" else "no")
64141
79cd4be708fb support user@host syntax;
wenzelm
parents: 64137
diff changeset
    37
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    38
    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
    39
      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
    40
      user: String = "",
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    41
      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
    42
      control_path: String = ""
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    43
    ): List[String] = {
76168
aab9bb081f01 clarified options;
wenzelm
parents: 76167
diff changeset
    44
      val ssh_batch_mode = options.bool("ssh_batch_mode")
76167
e517a38dc0e6 clarified options;
wenzelm
parents: 76166
diff changeset
    45
      val ssh_compression = options.bool("ssh_compression")
e517a38dc0e6 clarified options;
wenzelm
parents: 76166
diff changeset
    46
      val ssh_alive_interval = options.real("ssh_alive_interval").round
e517a38dc0e6 clarified options;
wenzelm
parents: 76166
diff changeset
    47
      val ssh_alive_count_max = options.int("ssh_alive_count_max")
e517a38dc0e6 clarified options;
wenzelm
parents: 76166
diff changeset
    48
76168
aab9bb081f01 clarified options;
wenzelm
parents: 76167
diff changeset
    49
      List(
aab9bb081f01 clarified options;
wenzelm
parents: 76167
diff changeset
    50
        entry("BatchMode", ssh_batch_mode),
aab9bb081f01 clarified options;
wenzelm
parents: 76167
diff changeset
    51
        entry("Compression", ssh_compression)) :::
76167
e517a38dc0e6 clarified options;
wenzelm
parents: 76166
diff changeset
    52
      (if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) :::
e517a38dc0e6 clarified options;
wenzelm
parents: 76166
diff changeset
    53
      (if (ssh_alive_count_max >= 0) List(entry("ServerAliveCountMax", ssh_alive_count_max)) else Nil) :::
76131
8b695e59db3f clarified default: do not override port from ssh_config, which could be different from 22;
wenzelm
parents: 76130
diff changeset
    54
      (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
    55
      (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
    56
      (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
    57
      (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
    58
    }
64325
47e03cb99274 prevent sporadic disconnection;
wenzelm
parents: 64306
diff changeset
    59
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    60
    def option(entry: String): String = "-o " + Bash.string(entry)
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    61
    def option(x: String, y: String): String = option(entry(x, y))
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    62
    def option(x: String, y: Int): String = option(entry(x, y))
76165
cf469736000c proper time values in seconds;
wenzelm
parents: 76164
diff changeset
    63
    def option(x: String, y: Long): String = option(entry(x, y))
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    64
    def option(x: String, y: Boolean): String = option(entry(x, y))
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    65
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    66
    def command(command: String, config: List[String]): String =
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
    67
      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
    68
  }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    69
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    70
  def sftp_string(str: String): String = {
76150
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    71
    val special = "[]?*\\{} \"'"
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    72
    if (str.isEmpty) "\"\""
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    73
    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
    74
      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
    75
      for (c <- str) {
76150
5c971c7fc807 more robust;
wenzelm
parents: 76149
diff changeset
    76
        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
    77
        res += c
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    78
      }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    79
      res.toString()
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    80
    }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    81
    else str
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    82
  }
67273
c573cfb2c407 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents: 67067
diff changeset
    83
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
    84
78425
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    85
  /* local host (not "localhost") */
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    86
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    87
  val LOCAL = "local"
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    88
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    89
  def is_local(host: String): Boolean = host.isEmpty || host == LOCAL
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    90
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    91
  def print_local(host: String): String = if (is_local(host)) LOCAL else host
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    92
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
    93
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    94
  /* open session */
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    95
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    96
  def open_session(
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    97
    options: Options,
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
    98
    host: String,
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
    99
    port: Int = 0,
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   100
    user: String = "",
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   101
    user_home: String = ""
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76100
diff changeset
   102
  ): Session = {
78583
8f11794211ef tuned error;
wenzelm
parents: 78425
diff changeset
   103
    if (is_local(host)) error("Illegal SSH host name " + quote(host))
78425
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
   104
76148
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   105
    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
   106
    val (control_master, control_path) =
76161
d556db0b7256 tuned names;
wenzelm
parents: 76159
diff changeset
   107
      if (multiplex) (true, Isabelle_System.tmp_file("ssh", 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
   108
      else (false, "")
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   109
    new Session(options, host, port, user, user_home, control_master, control_path)
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64256
diff changeset
   110
  }
64130
e17c211a0bb6 clarified treatment of options;
wenzelm
parents: 64129
diff changeset
   111
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   112
  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
   113
    val options: Options,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   114
    val host: String,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   115
    val port: Int,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   116
    val user: String,
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   117
    user_home0: String,
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   118
    control_master: Boolean,
76136
1bb677cceea4 let rsync re-use ssh connection via control path;
wenzelm
parents: 76133
diff changeset
   119
    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
   120
  ) extends System {
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   121
    ssh =>
64128
wenzelm
parents: 64127
diff changeset
   122
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   123
    override def ssh_session: Option[Session] = Some(ssh)
77782
127d077cccfe clarified signature: avoid object-oriented "dispatch";
wenzelm
parents: 77761
diff changeset
   124
76133
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   125
    def port_suffix: String = if (port > 0) ":" + port else ""
80210
wenzelm
parents: 80209
diff changeset
   126
    def user_prefix: String = if_proper(user, user + "@")
76133
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   127
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   128
    override def toString: String = user_prefix + host + port_suffix
77761
04a250facd44 tuned output;
wenzelm
parents: 77760
diff changeset
   129
    override def print: String = " (ssh " + toString + ")"
76132
2bb6eb6df6c2 proper port for Mercurial;
wenzelm
parents: 76131
diff changeset
   130
    override def hg_url: String = "ssh://" + toString + "/"
77783
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   131
    override def client_command: String =
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   132
      SSH.client_command(port = port, control_path = control_path)
76133
c5fd7947f585 tuned signature;
wenzelm
parents: 76132
diff changeset
   133
    override def rsync_prefix: String = user_prefix + host + ":"
64191
wenzelm
parents: 64190
diff changeset
   134
wenzelm
parents: 64190
diff changeset
   135
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   136
    /* 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
   137
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   138
    def make_command(
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   139
      command: String = "ssh",
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   140
      master: Boolean = false,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   141
      opts: String = "",
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   142
      args_host: Boolean = false,
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   143
      args: String = ""
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   144
    ): String = {
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   145
      val config =
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   146
        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
   147
          control_master = master, control_path = control_path)
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   148
      val args1 = if_proper(args_host, Bash.string(host) + if_proper(args, " ")) + args
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   149
      Config.command(command, config) +
77369
wenzelm
parents: 77130
diff changeset
   150
        if_proper(opts, " " + opts) +
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   151
        if_proper(args1, " -- " + args1)
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   152
    }
64134
57581e4026fe proper support for exec channel (see also bash.scala);
wenzelm
parents: 64133
diff changeset
   153
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   154
    def run_sftp(
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   155
      script: String,
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   156
      init: Path => Unit = _ => (),
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   157
      exit: Path => Unit = _ => ()
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   158
    ): Process_Result = {
80212
67b5e8b88728 tuned tmp name;
wenzelm
parents: 80211
diff changeset
   159
      Isabelle_System.with_tmp_dir("sftp") { dir =>
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   160
        init(dir)
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   161
        File.write(dir + Path.explode("script"), script)
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   162
        val result =
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   163
          Isabelle_System.bash(
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   164
            make_command("sftp", opts = "-b script", args_host = true), cwd = dir.file).check
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   165
        exit(dir)
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   166
        result
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   167
      }
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   168
    }
65009
eda9366bbfac remote database access via ssh port forwarding;
wenzelm
parents: 64347
diff changeset
   169
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   170
    def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result =
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   171
      Isabelle_System.bash(make_command(master = master, opts = opts, args_host = true, args = args))
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   172
76122
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
    /* init and exit */
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   175
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   176
    override val home: String = {
76154
dfddb80fc515 more robust: do not assume Bash syntax while testing for it;
wenzelm
parents: 76151
diff changeset
   177
      run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines
dfddb80fc515 more robust: do not assume Bash syntax while testing for it;
wenzelm
parents: 76151
diff changeset
   178
      match {
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   179
        case List(home, shell) =>
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   180
          if (shell.endsWith("/bash")) home
76149
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   181
          else {
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   182
            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
   183
          }
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   184
        case _ => error("Malformed remote environment for " + quote(toString))
ccc748255342 more robust: Bash.string operations require remote bash;
wenzelm
parents: 76148
diff changeset
   185
      }
76151
21492610ae5b proper treatment of complex multi-line script;
wenzelm
parents: 76150
diff changeset
   186
    }
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   187
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   188
    override val user_home: String = {
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   189
      val path1 =
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   190
        try { Path.explode(home).expand_env(Isabelle_System.No_Env) }
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   191
        catch { case ERROR(msg) => error(msg + " -- in SSH HOME") }
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   192
      val path2 =
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   193
        try { Path.explode(user_home0).expand_env(Isabelle_System.No_Env) }
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   194
        catch { case ERROR(msg) => error(msg + "-- in SSH USER_HOME") }
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   195
      (path1 + path2).implode
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   196
    }
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   197
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   198
    val settings: Isabelle_System.Settings = {
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   199
      case "HOME" => home
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   200
      case "USER_HOME" => user_home
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   201
      case _ => ""
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   202
    }
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   203
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   204
    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
   205
      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
   206
    }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   207
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   208
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   209
    /* 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
   210
80218
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   211
    override def kill_process(group_pid: String, signal: String): Boolean = {
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   212
      val script =
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   213
        make_command(args_host = true,
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   214
          args = "kill -" + Bash.string(signal) + " -" + Bash.string(group_pid))
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   215
      Isabelle_System.bash(script).ok
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   216
    }
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   217
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   218
    override def execute(remote_script: String,
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   219
      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
   220
      progress_stderr: String => Unit = (_: String) => (),
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   221
      redirect: Boolean = false,
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   222
      settings: Boolean = true,
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   223
      strict: Boolean = true
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   224
    ): Process_Result = {
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   225
      val remote_script1 = Isabelle_System.export_env(user_home = user_home) + remote_script
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   226
      Isabelle_System.bash(make_command(args_host = true, args = Bash.string(remote_script1)),
77077
c2e8ba15a10a discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
wenzelm
parents: 77076
diff changeset
   227
        progress_stdout = progress_stdout,
c2e8ba15a10a discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
wenzelm
parents: 77076
diff changeset
   228
        progress_stderr = progress_stderr,
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   229
        redirect = redirect,
77077
c2e8ba15a10a discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
wenzelm
parents: 77076
diff changeset
   230
        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
   231
    }
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   232
77054
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   233
    override def download_file(
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   234
      url_name: String,
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   235
      file: Path,
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   236
      progress: Progress = new Progress
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   237
    ): Unit = {
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   238
      val cmd_line =
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   239
        File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" +
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   240
          "download_file " + Bash.string(url_name) + " " + bash_path(file)
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   241
      execute(cmd_line,
77509
3bc49507bae5 clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents: 77369
diff changeset
   242
        progress_stdout = progress.echo(_),
3bc49507bae5 clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents: 77369
diff changeset
   243
        progress_stderr = progress.echo(_)).check
77054
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   244
    }
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   245
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   246
    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
   247
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   248
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   249
    /* remote file-system */
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   250
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   251
    override def expand_path(path: Path): Path = path.expand_env(settings)
77076
4471dbb3b7a0 more operations;
wenzelm
parents: 77059
diff changeset
   252
    override def absolute_path(path: Path): Path = {
4471dbb3b7a0 more operations;
wenzelm
parents: 77059
diff changeset
   253
      val path1 = expand_path(path)
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   254
      if (path1.is_absolute) path1 else Path.explode(home) + path1
77076
4471dbb3b7a0 more operations;
wenzelm
parents: 77059
diff changeset
   255
    }
4471dbb3b7a0 more operations;
wenzelm
parents: 77059
diff changeset
   256
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   257
    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
   258
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   259
    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
   260
    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
   261
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   262
    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
   263
    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
   264
80187
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   265
    override def eq_file(path1: Path, path2: Path): Boolean =
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   266
      path1 == path2 || execute("test " + bash_path(path1) + " -ef " + bash_path(path2)).ok
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   267
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   268
    override def delete(path: Path): Unit = {
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   269
      val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else ""
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   270
      if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path))
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   271
    }
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   272
78161
4b1b7cbb3e9a clarified signature;
wenzelm
parents: 78158
diff changeset
   273
    override def restrict(path: Path): Unit =
4b1b7cbb3e9a clarified signature;
wenzelm
parents: 78158
diff changeset
   274
      if (!execute("chmod g-rwx,o-rwx " + bash_path(path)).ok) {
4b1b7cbb3e9a clarified signature;
wenzelm
parents: 78158
diff changeset
   275
        error("Failed to change permissions of " + quote(remote_path(path)))
4b1b7cbb3e9a clarified signature;
wenzelm
parents: 78158
diff changeset
   276
      }
4b1b7cbb3e9a clarified signature;
wenzelm
parents: 78158
diff changeset
   277
78298
3b0f8f1010f2 clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
wenzelm
parents: 78161
diff changeset
   278
    override def set_executable(path: Path, reset: Boolean = false): Unit =
3b0f8f1010f2 clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
wenzelm
parents: 78161
diff changeset
   279
      if (!execute("chmod a" + (if (reset) "-" else "+") + "x " + bash_path(path)).ok) {
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   280
        error("Failed to change executable status of " + quote(remote_path(path)))
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   281
      }
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   282
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   283
    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
   284
      if (!execute("mkdir -p " + bash_path(path)).ok) {
76118
e8e3b60d8ecd clarified operation: avoid perl;
wenzelm
parents: 76117
diff changeset
   285
        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
   286
      }
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   287
      path
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   288
    }
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   289
77059
422c57b75b17 support remote operations;
wenzelm
parents: 77054
diff changeset
   290
    override def copy_file(src: Path, dst: Path): Unit = {
80187
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   291
      val target = if (is_dir(dst)) dst + expand_path(src).base else dst
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   292
      if (!eq_file(src, target)) {
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   293
        if (!execute("cp -a " + bash_path(src) + " " + bash_path(target)).ok) {
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   294
          error("Failed to copy file " +
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   295
            absolute_path(src) + " to " + absolute_path(target) + " (ssh " + toString + ")")
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   296
        }
77059
422c57b75b17 support remote operations;
wenzelm
parents: 77054
diff changeset
   297
      }
422c57b75b17 support remote operations;
wenzelm
parents: 77054
diff changeset
   298
    }
422c57b75b17 support remote operations;
wenzelm
parents: 77054
diff changeset
   299
77096
940a6cb734fd more operations for SSH.System;
wenzelm
parents: 77092
diff changeset
   300
    override def read_dir(path: Path): List[String] =
76241
aa6ce2e51e6c proper base names;
wenzelm
parents: 76240
diff changeset
   301
      run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s =>
aa6ce2e51e6c proper base names;
wenzelm
parents: 76240
diff changeset
   302
        if (s == "." || s == "..") None
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   303
        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
   304
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   305
    private def get_file[A](path: Path, f: Path => A): A = {
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   306
      var result: Option[A] = None
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   307
      run_sftp("get -p " + sftp_path(path) + " local",
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   308
        exit = dir => result = Some(f(dir + Path.explode("local"))))
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   309
      result.get
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   310
    }
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   311
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   312
    private def put_file(path: Path, f: Path => Unit): Unit =
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   313
      run_sftp("put -p local " + sftp_path(path),
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   314
        init = dir => f(dir + Path.explode("local")))
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   315
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   316
    override def read_file(path: Path, local_path: Path): Unit =
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   317
      get_file(path, Isabelle_System.copy_file(_, local_path))
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   318
    override def read_bytes(path: Path): Bytes =
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   319
      get_file(path, Bytes.read)
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   320
    override def read(path: Path): String =
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   321
      get_file(path, File.read)
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64254
diff changeset
   322
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   323
    override def write_file(path: Path, local_path: Path): Unit =
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   324
      put_file(path, Isabelle_System.copy_file(local_path, _))
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   325
    override def write_bytes(path: Path, bytes: Bytes): Unit =
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   326
      put_file(path, Bytes.write(_, bytes))
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   327
    override def write(path: Path, text: String): Unit =
76164
5e8bc80df6b3 clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh;
wenzelm
parents: 76163
diff changeset
   328
      put_file(path, File.write(_, text))
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents: 71780
diff changeset
   329
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   330
80217
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   331
    /* tmp dirs and files */
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   332
80215
c6d18c836509 clarified signature;
wenzelm
parents: 80214
diff changeset
   333
    override def rm_tree(dir: Path): Unit =
c6d18c836509 clarified signature;
wenzelm
parents: 80214
diff changeset
   334
      execute("rm -r -f " + bash_path(dir)).check
64306
7b6dc1b36f20 tuned signature, in accordance to Isabelle_System;
wenzelm
parents: 64304
diff changeset
   335
80215
c6d18c836509 clarified signature;
wenzelm
parents: 80214
diff changeset
   336
    override def tmp_dir(): Path =
c6d18c836509 clarified signature;
wenzelm
parents: 80214
diff changeset
   337
      Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out)
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   338
80217
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   339
    override def tmp_file(name: String, ext: String = ""): Path = {
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   340
      val file_name = name + "-XXXXXXXXXXXX" + if_proper(ext, "." + ext)
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   341
      Path.explode(execute("mktemp /tmp/" + Bash.string(file_name)).check.out)
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   342
    }
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   343
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   344
    override def with_tmp_dir[A](body: Path => A): A = {
80216
wenzelm
parents: 80215
diff changeset
   345
      val path = tmp_dir()
wenzelm
parents: 80215
diff changeset
   346
      try { body(path) } finally { rm_tree(path) }
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   347
    }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   348
80217
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   349
    override def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = {
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   350
      val path = tmp_file(name, ext = ext)
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   351
      try { body(path) } finally { delete(path) }
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   352
    }
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   353
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   354
78345
545da61f5989 clarified signature;
wenzelm
parents: 78341
diff changeset
   355
    /* open server on remote host */
76122
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   356
78345
545da61f5989 clarified signature;
wenzelm
parents: 78341
diff changeset
   357
    def open_server(
78339
f8a553a21423 tuned signature;
wenzelm
parents: 78298
diff changeset
   358
      remote_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
   359
      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
   360
      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
   361
      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
   362
      ssh_close: Boolean = false
78345
545da61f5989 clarified signature;
wenzelm
parents: 78341
diff changeset
   363
    ): Server = {
78340
5790e48f7573 clarified signature: more uniform SSH.Port_Forwarding;
wenzelm
parents: 78339
diff changeset
   364
      val forward_host = local_host
5790e48f7573 clarified signature: more uniform SSH.Port_Forwarding;
wenzelm
parents: 78339
diff changeset
   365
      val forward_port = if (local_port > 0) local_port else Isabelle_System.local_port()
5790e48f7573 clarified signature: more uniform SSH.Port_Forwarding;
wenzelm
parents: 78339
diff changeset
   366
      val forward = List(forward_host, forward_port, remote_host, remote_port).mkString(":")
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   367
      val forward_option = "-L " + Bash.string(forward)
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   368
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   369
      val cancel: () => Unit =
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   370
        if (control_path.nonEmpty) {
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   371
          run_ssh(opts = forward_option + " -O forward").check
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   372
          () => run_ssh(opts = forward_option + " -O cancel")  // permissive
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   373
        }
76148
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   374
        else {
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   375
          val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false))
78345
545da61f5989 clarified signature;
wenzelm
parents: 78341
diff changeset
   376
          val thread = Isabelle_Thread.fork("ssh_server") {
76148
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   377
            val opts =
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   378
              forward_option +
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   379
                " " + Config.option("SessionType", "none") +
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   380
                " " + Config.option("PermitLocalCommand", true) +
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   381
                " " + Config.option("LocalCommand", "pwd")
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   382
            try {
80214
d78446e2b613 clarified signature;
wenzelm
parents: 80212
diff changeset
   383
              Isabelle_System.bash(make_command(opts = opts, args_host = true),
76148
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   384
                progress_stdout = _ => result.change(_ => Exn.Res(true))).check
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   385
            }
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   386
            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
   387
          }
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   388
          result.guarded_access {
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   389
            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
   390
            case Exn.Exn(exn) => throw exn
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   391
          }
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   392
          () => thread.interrupt()
769ebb139a32 support port forwarding without multiplexing (for the sake of Windows);
wenzelm
parents: 76147
diff changeset
   393
        }
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   394
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   395
      val shutdown_hook =
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   396
        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
   397
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   398
      new Server(forward_host, forward_port, ssh) {
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   399
        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
   400
        override def close(): Unit = {
76147
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   401
          cancel()
75f0fc965539 misc tuning and clarification;
wenzelm
parents: 76145
diff changeset
   402
          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
   403
          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
   404
        }
b8f26c20d3b1 ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration);
wenzelm
parents: 76119
diff changeset
   405
      }
64137
e9b3d9c1bc5a support for remote tmp dirs;
wenzelm
parents: 64136
diff changeset
   406
    }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   407
  }
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   408
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   409
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   410
  /* server port forwarding */
78340
5790e48f7573 clarified signature: more uniform SSH.Port_Forwarding;
wenzelm
parents: 78339
diff changeset
   411
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   412
  def open_server(
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   413
    options: Options,
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   414
    host: String,
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   415
    port: Int = 0,
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   416
    user: String = "",
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   417
    user_home: String = "",
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   418
    remote_port: Int = 0,
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   419
    remote_host: String = "localhost",
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   420
    local_port: Int = 0,
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   421
    local_host: String = "localhost"
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   422
  ): Server = {
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   423
    val ssh = open_session(options, host, port = port, user = user, user_home = user_home)
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   424
    try {
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   425
      ssh.open_server(remote_port = remote_port, remote_host = remote_host,
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   426
        local_port = local_port, local_host = local_host, ssh_close = true)
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   427
    }
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   428
    catch { case exn: Throwable => ssh.close(); throw exn }
78341
5f14f1290a88 clarified signature;
wenzelm
parents: 78340
diff changeset
   429
  }
5f14f1290a88 clarified signature;
wenzelm
parents: 78340
diff changeset
   430
78345
545da61f5989 clarified signature;
wenzelm
parents: 78341
diff changeset
   431
  def local_server(port: Int = 0, host: String = "localhost"): Server =
545da61f5989 clarified signature;
wenzelm
parents: 78341
diff changeset
   432
    new Local_Server(host, port)
78341
5f14f1290a88 clarified signature;
wenzelm
parents: 78340
diff changeset
   433
78345
545da61f5989 clarified signature;
wenzelm
parents: 78341
diff changeset
   434
  val no_server: Server = new No_Server
76116
c4dc343fdbcb clarified signature: avoid exposure of JSch types;
wenzelm
parents: 76115
diff changeset
   435
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   436
  class Server private[SSH](
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   437
    val host: String,
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   438
    val port: Int,
78347
72fc2ff08e07 clarified signature: more operations;
wenzelm
parents: 78346
diff changeset
   439
    val ssh_system: System
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   440
  ) extends AutoCloseable {
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   441
    def defined: Boolean = host.nonEmpty && port > 0
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   442
    override def close(): Unit = ()
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   443
  }
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   444
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   445
  class Local_Server private[SSH](host: String, port: Int)
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   446
  extends Server(host, port, Local) {
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   447
    override def toString: String = if_proper(host, host + ":") + port
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   448
  }
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   449
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   450
  class No_Server extends Server("", 0, Local) {
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   451
    override def toString: String = "0"
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   452
  }
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   453
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   454
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   455
  /* system operations */
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   456
77783
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   457
  def open_system(
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   458
    options: Options,
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   459
    host: String,
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   460
    port: Int = 0,
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   461
    user: String = "",
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   462
    user_home: String = ""
77783
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   463
  ): System = {
79635
8d2539a13502 more robust;
wenzelm
parents: 79633
diff changeset
   464
    if (is_local(host)) {
8d2539a13502 more robust;
wenzelm
parents: 79633
diff changeset
   465
      if (user_home.isEmpty) Local
8d2539a13502 more robust;
wenzelm
parents: 79633
diff changeset
   466
      else error("Illegal user home for local host")
8d2539a13502 more robust;
wenzelm
parents: 79633
diff changeset
   467
    }
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   468
    else open_session(options, host = host, port = port, user = user, user_home = user_home)
77783
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   469
  }
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   470
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74306
diff changeset
   471
  trait System extends AutoCloseable {
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   472
    def ssh_session: Option[Session]
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   473
    def is_local: Boolean = ssh_session.isEmpty
77782
127d077cccfe clarified signature: avoid object-oriented "dispatch";
wenzelm
parents: 77761
diff changeset
   474
79633
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   475
    def home: String = ""
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   476
    def user_home: String = ""
c59231722f10 support explicit USER_HOME within SSH session;
wenzelm
parents: 78924
diff changeset
   477
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   478
    def close(): Unit = ()
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   479
78425
62d7ef1da441 clarified signature;
wenzelm
parents: 78347
diff changeset
   480
    override def toString: String = LOCAL
77761
04a250facd44 tuned output;
wenzelm
parents: 77760
diff changeset
   481
    def print: String = ""
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   482
    def hg_url: String = ""
77783
fb61887c069a clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents: 77782
diff changeset
   483
    def client_command: String = ""
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   484
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   485
    def rsync_prefix: String = ""
75517
292d7a9dc8a3 proper operation on String, not Path;
wenzelm
parents: 75513
diff changeset
   486
    def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
75500
57e292106d71 more operations;
wenzelm
parents: 75480
diff changeset
   487
80189
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   488
    def find_path[A](start: Path, detect: Path => Option[A]): Option[A] = {
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   489
      @tailrec def find(root: Path): Option[A] =
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   490
        detect(root) match {
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   491
          case None => if (root.is_root) None else find(root + Path.parent)
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   492
          case some => some
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   493
        }
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   494
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   495
      find(expand_path(start))
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   496
    }
e8d4ac2f21ea clarified modules;
wenzelm
parents: 80187
diff changeset
   497
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   498
    def expand_path(path: Path): Path = path.expand
77076
4471dbb3b7a0 more operations;
wenzelm
parents: 77059
diff changeset
   499
    def absolute_path(path: Path): Path = path.absolute
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 66923
diff changeset
   500
    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
   501
    def is_dir(path: Path): Boolean = path.is_dir
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   502
    def is_file(path: Path): Boolean = path.is_file
80187
b8918a5a669e more uniform local/remote operations;
wenzelm
parents: 79635
diff changeset
   503
    def eq_file(path1: Path, path2: Path): Boolean = File.eq(path1, path2)
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   504
    def delete(path: Path): Unit = path.file.delete
78161
4b1b7cbb3e9a clarified signature;
wenzelm
parents: 78158
diff changeset
   505
    def restrict(path: Path): Unit = File.restrict(path)
78298
3b0f8f1010f2 clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
wenzelm
parents: 78161
diff changeset
   506
    def set_executable(path: Path, reset: Boolean = false): Unit =
3b0f8f1010f2 clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
wenzelm
parents: 78161
diff changeset
   507
      File.set_executable(path, reset = reset)
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   508
    def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   509
    def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir)
80215
c6d18c836509 clarified signature;
wenzelm
parents: 80214
diff changeset
   510
    def tmp_dir(): Path = File.path(Isabelle_System.tmp_dir("tmp"))
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   511
    def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
80217
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   512
    def tmp_file(name: String, ext: String = ""): Path =
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   513
      File.path(Isabelle_System.tmp_file(name, ext = ext))
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   514
    def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
e0606fb415d2 more operations;
wenzelm
parents: 80216
diff changeset
   515
      Isabelle_System.with_tmp_file(name, ext = ext)(body)
77096
940a6cb734fd more operations for SSH.System;
wenzelm
parents: 77092
diff changeset
   516
    def read_dir(path: Path): List[String] = File.read_dir(path)
77059
422c57b75b17 support remote operations;
wenzelm
parents: 77054
diff changeset
   517
    def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   518
    def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
75513
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   519
    def read_bytes(path: Path): Bytes = Bytes.read(path)
36316c6a3fc2 clarified signature: more operations;
wenzelm
parents: 75500
diff changeset
   520
    def read(path: Path): String = File.read(path)
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   521
    def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   522
    def write_bytes(path: Path, bytes: Bytes): Unit = Bytes.write(path, bytes)
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   523
    def write(path: Path, text: String): Unit = File.write(path, text)
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   524
80218
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   525
    def kill_process(group_pid: String, signal: String): Boolean =
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   526
      isabelle.setup.Environment.kill_process(Bash.string(group_pid), Bash.string(signal))
875968a3b2f9 suport Isabelle_System.bash via SSH.System;
wenzelm
parents: 80217
diff changeset
   527
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   528
    def execute(command: String,
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   529
        progress_stdout: String => Unit = (_: String) => (),
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   530
        progress_stderr: String => Unit = (_: String) => (),
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   531
        redirect: Boolean = false,
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   532
        settings: Boolean = true,
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   533
        strict: Boolean = true): Process_Result =
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   534
      Isabelle_System.bash(command,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   535
        progress_stdout = progress_stdout,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   536
        progress_stderr = progress_stderr,
77092
4d9f3d1e1749 more operations for SSH.System;
wenzelm
parents: 77079
diff changeset
   537
        redirect = redirect,
73634
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   538
        env = if (settings) Isabelle_System.settings() else null,
c88faa1e09e1 support local build_heaps;
wenzelm
parents: 73367
diff changeset
   539
        strict = strict)
72338
54871a086193 formal platform information, notably for ssh;
wenzelm
parents: 71780
diff changeset
   540
77760
34178d26a360 more SSH operations;
wenzelm
parents: 77509
diff changeset
   541
    def new_directory(path: Path): Path =
34178d26a360 more SSH operations;
wenzelm
parents: 77509
diff changeset
   542
      if (is_dir(path)) error("Directory already exists: " + absolute_path(path))
34178d26a360 more SSH operations;
wenzelm
parents: 77509
diff changeset
   543
      else make_directory(path)
34178d26a360 more SSH operations;
wenzelm
parents: 77509
diff changeset
   544
77054
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   545
    def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   546
      Isabelle_System.download_file(url_name, file, progress = progress)
3bb374ac31b3 support remote download_file;
wenzelm
parents: 76241
diff changeset
   547
72340
676066aa4798 clarified signature;
wenzelm
parents: 72338
diff changeset
   548
    def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
77130
2b8cf3b94cde more operations;
wenzelm
parents: 77096
diff changeset
   549
78610
fd1fec53665b clarified signature: prefer enum types;
wenzelm
parents: 78583
diff changeset
   550
    def isabelle_platform_family: Platform.Family =
77130
2b8cf3b94cde more operations;
wenzelm
parents: 77096
diff changeset
   551
      Platform.Family.parse(isabelle_platform.ISABELLE_PLATFORM_FAMILY)
66570
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   552
  }
9af879e222cc clarified signature;
wenzelm
parents: 65717
diff changeset
   553
77782
127d077cccfe clarified signature: avoid object-oriented "dispatch";
wenzelm
parents: 77761
diff changeset
   554
  object Local extends System {
78346
9c2e273d2f0d clarified signature: more operations;
wenzelm
parents: 78345
diff changeset
   555
    override def ssh_session: Option[Session] = None
77782
127d077cccfe clarified signature: avoid object-oriented "dispatch";
wenzelm
parents: 77761
diff changeset
   556
  }
64123
a967b5a07f92 support for SSH in Isabelle/Scala;
wenzelm
parents:
diff changeset
   557
}