author | wenzelm |
Fri, 31 May 2024 20:46:51 +0200 | |
changeset 80218 | 875968a3b2f9 |
parent 80217 | e0606fb415d2 |
child 80220 | 928e02d0cab7 |
permissions | -rw-r--r-- |
64123 | 1 |
/* Title: Pure/General/ssh.scala |
2 |
Author: Makarius |
|
3 |
||
80209 | 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 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
73909 | 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 | 13 |
|
80189 | 14 |
import scala.annotation.tailrec |
15 |
||
64123 | 16 |
|
75393 | 17 |
object SSH { |
76170 | 18 |
/* client command */ |
19 |
||
20 |
def client_command(port: Int = 0, control_path: String = ""): String = |
|
21 |
if (control_path.isEmpty || control_path == Bash.string(control_path)) { |
|
22 |
"ssh" + |
|
23 |
(if (port > 0) " -p " + port else "") + |
|
77369 | 24 |
if_proper(control_path, " -o ControlPath=" + control_path) |
76170 | 25 |
} |
26 |
else error ("Malformed SSH control socket: " + quote(control_path)) |
|
27 |
||
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 | 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 | 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 | 44 |
val ssh_batch_mode = options.bool("ssh_batch_mode") |
76167 | 45 |
val ssh_compression = options.bool("ssh_compression") |
46 |
val ssh_alive_interval = options.real("ssh_alive_interval").round |
|
47 |
val ssh_alive_count_max = options.int("ssh_alive_count_max") |
|
48 |
||
76168 | 49 |
List( |
50 |
entry("BatchMode", ssh_batch_mode), |
|
51 |
entry("Compression", ssh_compression)) ::: |
|
76167 | 52 |
(if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) ::: |
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 | 59 |
|
76147 | 60 |
def option(entry: String): String = "-o " + Bash.string(entry) |
61 |
def option(x: String, y: String): String = option(entry(x, y)) |
|
62 |
def option(x: String, y: Int): String = option(entry(x, y)) |
|
76165 | 63 |
def option(x: String, y: Long): String = option(entry(x, y)) |
76147 | 64 |
def option(x: String, y: Boolean): String = option(entry(x, y)) |
65 |
||
66 |
def command(command: String, config: List[String]): String = |
|
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 | 71 |
val special = "[]?*\\{} \"'" |
72 |
if (str.isEmpty) "\"\"" |
|
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 | 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 | 84 |
|
78425 | 85 |
/* local host (not "localhost") */ |
86 |
||
87 |
val LOCAL = "local" |
|
88 |
||
89 |
def is_local(host: String): Boolean = host.isEmpty || host == LOCAL |
|
90 |
||
91 |
def print_local(host: String): String = if (is_local(host)) LOCAL else host |
|
92 |
||
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 | 100 |
user: String = "", |
101 |
user_home: String = "" |
|
76115
f17393e21388
clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents:
76100
diff
changeset
|
102 |
): Session = { |
78583 | 103 |
if (is_local(host)) error("Illegal SSH host name " + quote(host)) |
78425 | 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 | 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 | 109 |
new Session(options, host, port, user, user_home, control_master, control_path) |
64257 | 110 |
} |
64130 | 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 | 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 | 122 |
|
78346 | 123 |
override def ssh_session: Option[Session] = Some(ssh) |
77782
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
wenzelm
parents:
77761
diff
changeset
|
124 |
|
76133 | 125 |
def port_suffix: String = if (port > 0) ":" + port else "" |
80210 | 126 |
def user_prefix: String = if_proper(user, user + "@") |
76133 | 127 |
|
128 |
override def toString: String = user_prefix + host + port_suffix |
|
77761 | 129 |
override def print: String = " (ssh " + toString + ")" |
76132 | 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 | 133 |
override def rsync_prefix: String = user_prefix + host + ":" |
64191 | 134 |
|
135 |
||
76147 | 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 | 138 |
def make_command( |
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 | 142 |
args_host: Boolean = false, |
143 |
args: String = "" |
|
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 | 148 |
val args1 = if_proper(args_host, Bash.string(host) + if_proper(args, " ")) + args |
149 |
Config.command(command, config) + |
|
77369 | 150 |
if_proper(opts, " " + opts) + |
80214 | 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 | 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 | 163 |
Isabelle_System.bash( |
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 | 169 |
|
80214 | 170 |
def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = |
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 | 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 | 179 |
case List(home, shell) => |
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 | 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 | 188 |
override val user_home: String = { |
189 |
val path1 = |
|
190 |
try { Path.explode(home).expand_env(Isabelle_System.No_Env) } |
|
191 |
catch { case ERROR(msg) => error(msg + " -- in SSH HOME") } |
|
192 |
val path2 = |
|
193 |
try { Path.explode(user_home0).expand_env(Isabelle_System.No_Env) } |
|
194 |
catch { case ERROR(msg) => error(msg + "-- in SSH USER_HOME") } |
|
195 |
(path1 + path2).implode |
|
196 |
} |
|
197 |
||
198 |
val settings: Isabelle_System.Settings = { |
|
199 |
case "HOME" => home |
|
200 |
case "USER_HOME" => user_home |
|
201 |
case _ => "" |
|
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 | 211 |
override def kill_process(group_pid: String, signal: String): Boolean = { |
212 |
val script = |
|
213 |
make_command(args_host = true, |
|
214 |
args = "kill -" + Bash.string(signal) + " -" + Bash.string(group_pid)) |
|
215 |
Isabelle_System.bash(script).ok |
|
216 |
} |
|
217 |
||
80214 | 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 | 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 | 225 |
val remote_script1 = Isabelle_System.export_env(user_home = user_home) + remote_script |
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 | 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 | 233 |
override def download_file( |
234 |
url_name: String, |
|
235 |
file: Path, |
|
236 |
progress: Progress = new Progress |
|
237 |
): Unit = { |
|
238 |
val cmd_line = |
|
239 |
File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" + |
|
240 |
"download_file " + Bash.string(url_name) + " " + bash_path(file) |
|
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 | 244 |
} |
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 | 251 |
override def expand_path(path: Path): Path = path.expand_env(settings) |
77076 | 252 |
override def absolute_path(path: Path): Path = { |
253 |
val path1 = expand_path(path) |
|
79633 | 254 |
if (path1.is_absolute) path1 else Path.explode(home) + path1 |
77076 | 255 |
} |
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 | 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 | 265 |
override def eq_file(path1: Path, path2: Path): Boolean = |
266 |
path1 == path2 || execute("test " + bash_path(path1) + " -ef " + bash_path(path2)).ok |
|
267 |
||
77092 | 268 |
override def delete(path: Path): Unit = { |
269 |
val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else "" |
|
270 |
if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path)) |
|
271 |
} |
|
272 |
||
78161 | 273 |
override def restrict(path: Path): Unit = |
274 |
if (!execute("chmod g-rwx,o-rwx " + bash_path(path)).ok) { |
|
275 |
error("Failed to change permissions of " + quote(remote_path(path))) |
|
276 |
} |
|
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 | 280 |
error("Failed to change executable status of " + quote(remote_path(path))) |
281 |
} |
|
282 |
||
75393 | 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 | 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 | 287 |
path |
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 | 290 |
override def copy_file(src: Path, dst: Path): Unit = { |
80187 | 291 |
val target = if (is_dir(dst)) dst + expand_path(src).base else dst |
292 |
if (!eq_file(src, target)) { |
|
293 |
if (!execute("cp -a " + bash_path(src) + " " + bash_path(target)).ok) { |
|
294 |
error("Failed to copy file " + |
|
295 |
absolute_path(src) + " to " + absolute_path(target) + " (ssh " + toString + ")") |
|
296 |
} |
|
77059 | 297 |
} |
298 |
} |
|
299 |
||
77096 | 300 |
override def read_dir(path: Path): List[String] = |
76241 | 301 |
run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s => |
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 | 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 | 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 | 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 | 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 | 329 |
|
64137 | 330 |
|
80217 | 331 |
/* tmp dirs and files */ |
64137 | 332 |
|
80215 | 333 |
override def rm_tree(dir: Path): Unit = |
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 | 336 |
override def tmp_dir(): Path = |
337 |
Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out) |
|
64137 | 338 |
|
80217 | 339 |
override def tmp_file(name: String, ext: String = ""): Path = { |
340 |
val file_name = name + "-XXXXXXXXXXXX" + if_proper(ext, "." + ext) |
|
341 |
Path.explode(execute("mktemp /tmp/" + Bash.string(file_name)).check.out) |
|
342 |
} |
|
343 |
||
75393 | 344 |
override def with_tmp_dir[A](body: Path => A): A = { |
80216 | 345 |
val path = tmp_dir() |
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 | 349 |
override def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { |
350 |
val path = tmp_file(name, ext = ext) |
|
351 |
try { body(path) } finally { delete(path) } |
|
352 |
} |
|
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 | 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 | 357 |
def open_server( |
78339 | 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 | 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 | 367 |
val forward_option = "-L " + Bash.string(forward) |
368 |
||
369 |
val cancel: () => Unit = |
|
370 |
if (control_path.nonEmpty) { |
|
371 |
run_ssh(opts = forward_option + " -O forward").check |
|
372 |
() => run_ssh(opts = forward_option + " -O cancel") // permissive |
|
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 | 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 | 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 | 394 |
|
395 |
val shutdown_hook = |
|
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 | 398 |
new Server(forward_host, forward_port, ssh) { |
76147 | 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 | 401 |
cancel() |
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 | 406 |
} |
64123 | 407 |
} |
66570 | 408 |
|
78346 | 409 |
|
410 |
/* server port forwarding */ |
|
78340
5790e48f7573
clarified signature: more uniform SSH.Port_Forwarding;
wenzelm
parents:
78339
diff
changeset
|
411 |
|
78346 | 412 |
def open_server( |
413 |
options: Options, |
|
414 |
host: String, |
|
415 |
port: Int = 0, |
|
416 |
user: String = "", |
|
79633 | 417 |
user_home: String = "", |
78346 | 418 |
remote_port: Int = 0, |
419 |
remote_host: String = "localhost", |
|
420 |
local_port: Int = 0, |
|
421 |
local_host: String = "localhost" |
|
422 |
): Server = { |
|
79633 | 423 |
val ssh = open_session(options, host, port = port, user = user, user_home = user_home) |
78346 | 424 |
try { |
425 |
ssh.open_server(remote_port = remote_port, remote_host = remote_host, |
|
426 |
local_port = local_port, local_host = local_host, ssh_close = true) |
|
427 |
} |
|
428 |
catch { case exn: Throwable => ssh.close(); throw exn } |
|
78341 | 429 |
} |
430 |
||
78345 | 431 |
def local_server(port: Int = 0, host: String = "localhost"): Server = |
432 |
new Local_Server(host, port) |
|
78341 | 433 |
|
78345 | 434 |
val no_server: Server = new No_Server |
76116
c4dc343fdbcb
clarified signature: avoid exposure of JSch types;
wenzelm
parents:
76115
diff
changeset
|
435 |
|
78346 | 436 |
class Server private[SSH]( |
437 |
val host: String, |
|
438 |
val port: Int, |
|
78347 | 439 |
val ssh_system: System |
78346 | 440 |
) extends AutoCloseable { |
441 |
def defined: Boolean = host.nonEmpty && port > 0 |
|
442 |
override def close(): Unit = () |
|
443 |
} |
|
444 |
||
445 |
class Local_Server private[SSH](host: String, port: Int) |
|
446 |
extends Server(host, port, Local) { |
|
447 |
override def toString: String = if_proper(host, host + ":") + port |
|
448 |
} |
|
449 |
||
450 |
class No_Server extends Server("", 0, Local) { |
|
451 |
override def toString: String = "0" |
|
452 |
} |
|
453 |
||
66570 | 454 |
|
455 |
/* system operations */ |
|
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 | 461 |
user: String = "", |
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 | 464 |
if (is_local(host)) { |
465 |
if (user_home.isEmpty) Local |
|
466 |
else error("Illegal user home for local host") |
|
467 |
} |
|
79633 | 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 | 471 |
trait System extends AutoCloseable { |
78346 | 472 |
def ssh_session: Option[Session] |
473 |
def is_local: Boolean = ssh_session.isEmpty |
|
77782
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
wenzelm
parents:
77761
diff
changeset
|
474 |
|
79633 | 475 |
def home: String = "" |
476 |
def user_home: String = "" |
|
477 |
||
73634 | 478 |
def close(): Unit = () |
479 |
||
78425 | 480 |
override def toString: String = LOCAL |
77761 | 481 |
def print: String = "" |
66570 | 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 | 484 |
|
75500 | 485 |
def rsync_prefix: String = "" |
75517 | 486 |
def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode |
75500 | 487 |
|
80189 | 488 |
def find_path[A](start: Path, detect: Path => Option[A]): Option[A] = { |
489 |
@tailrec def find(root: Path): Option[A] = |
|
490 |
detect(root) match { |
|
491 |
case None => if (root.is_root) None else find(root + Path.parent) |
|
492 |
case some => some |
|
493 |
} |
|
494 |
||
495 |
find(expand_path(start)) |
|
496 |
} |
|
497 |
||
66570 | 498 |
def expand_path(path: Path): Path = path.expand |
77076 | 499 |
def absolute_path(path: Path): Path = path.absolute |
67066 | 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 | 502 |
def is_file(path: Path): Boolean = path.is_file |
80187 | 503 |
def eq_file(path1: Path, path2: Path): Boolean = File.eq(path1, path2) |
77092 | 504 |
def delete(path: Path): Unit = path.file.delete |
78161 | 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 | 508 |
def make_directory(path: Path): Path = Isabelle_System.make_directory(path) |
77092 | 509 |
def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir) |
80215 | 510 |
def tmp_dir(): Path = File.path(Isabelle_System.tmp_dir("tmp")) |
73634 | 511 |
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body) |
80217 | 512 |
def tmp_file(name: String, ext: String = ""): Path = |
513 |
File.path(Isabelle_System.tmp_file(name, ext = ext)) |
|
514 |
def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = |
|
515 |
Isabelle_System.with_tmp_file(name, ext = ext)(body) |
|
77096 | 516 |
def read_dir(path: Path): List[String] = File.read_dir(path) |
77059 | 517 |
def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) |
73634 | 518 |
def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) |
75513 | 519 |
def read_bytes(path: Path): Bytes = Bytes.read(path) |
520 |
def read(path: Path): String = File.read(path) |
|
77092 | 521 |
def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) |
522 |
def write_bytes(path: Path, bytes: Bytes): Unit = Bytes.write(path, bytes) |
|
523 |
def write(path: Path, text: String): Unit = File.write(path, text) |
|
66570 | 524 |
|
80218 | 525 |
def kill_process(group_pid: String, signal: String): Boolean = |
526 |
isabelle.setup.Environment.kill_process(Bash.string(group_pid), Bash.string(signal)) |
|
527 |
||
66570 | 528 |
def execute(command: String, |
529 |
progress_stdout: String => Unit = (_: String) => (), |
|
530 |
progress_stderr: String => Unit = (_: String) => (), |
|
77092 | 531 |
redirect: Boolean = false, |
73634 | 532 |
settings: Boolean = true, |
66570 | 533 |
strict: Boolean = true): Process_Result = |
73634 | 534 |
Isabelle_System.bash(command, |
535 |
progress_stdout = progress_stdout, |
|
536 |
progress_stderr = progress_stderr, |
|
77092 | 537 |
redirect = redirect, |
73634 | 538 |
env = if (settings) Isabelle_System.settings() else null, |
539 |
strict = strict) |
|
72338 | 540 |
|
77760 | 541 |
def new_directory(path: Path): Path = |
542 |
if (is_dir(path)) error("Directory already exists: " + absolute_path(path)) |
|
543 |
else make_directory(path) |
|
544 |
||
77054 | 545 |
def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = |
546 |
Isabelle_System.download_file(url_name, file, progress = progress) |
|
547 |
||
72340 | 548 |
def isabelle_platform: Isabelle_Platform = Isabelle_Platform() |
77130 | 549 |
|
78610 | 550 |
def isabelle_platform_family: Platform.Family = |
77130 | 551 |
Platform.Family.parse(isabelle_platform.ISABELLE_PLATFORM_FAMILY) |
66570 | 552 |
} |
553 |
||
77782
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
wenzelm
parents:
77761
diff
changeset
|
554 |
object Local extends System { |
78346 | 555 |
override def ssh_session: Option[Session] = None |
77782
127d077cccfe
clarified signature: avoid object-oriented "dispatch";
wenzelm
parents:
77761
diff
changeset
|
556 |
} |
64123 | 557 |
} |