--- a/src/Pure/Admin/isabelle_cronjob.scala Mon Sep 12 08:07:22 2022 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Sep 12 23:10:45 2022 +0200
@@ -135,12 +135,8 @@
sealed case class Remote_Build(
description: String,
host: String,
- actual_host: String = "",
user: String = "",
port: Int = 0,
- proxy_host: String = "",
- proxy_user: String = "",
- proxy_port: Int = 0,
historic: Boolean = false,
history: Int = 0,
history_base: String = "build_history_base",
@@ -154,9 +150,7 @@
active: Boolean = true
) {
def open_session(options: Options): SSH.Session =
- SSH.open_session(options, host = host, user = user, port = port, actual_host = actual_host,
- proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
- permissive = proxy_host.nonEmpty)
+ SSH.open_session(options, host = host, user = user, port = port)
def sql: PostgreSQL.Source =
Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " +
@@ -209,11 +203,9 @@
val remote_builds_old: List[Remote_Build] =
List(
Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius",
- proxy_host = "laraserver", proxy_user = "makarius",
options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("Linux A", "i21of4", user = "i21isatest",
- proxy_host = "lxbroy10", proxy_user = "i21isatest",
options = "-m32 -M1x4,2,4" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
@@ -235,7 +227,6 @@
options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("AFP old bulky", "lrzcloud1",
- proxy_host = "lxbroy10", proxy_user = "i21isatest",
options = "-m64 -M6 -U30000 -s10 -t AFP",
args = "-g large -g slow",
afp = true,
@@ -353,8 +344,7 @@
options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))),
List(
- Remote_Build("macOS 10.15 Catalina", "monterey", actual_host = "laramac01",
- user = "makarius", proxy_host = "laraserver", proxy_user = "makarius",
+ Remote_Build("macOS 10.15 Catalina", "monterey", user = "makarius",
options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
args = "-a -d '~~/src/Benchmarks'")),
List(
@@ -381,8 +371,7 @@
val remote_builds2: List[List[Remote_Build]] =
List(
List(
- Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41",
- proxy_host = "lxbroy10", proxy_user = "i21isatest",
+ Remote_Build("AFP", "lrzcloud2",
java_heap = "8g",
options = "-m32 -M1x6 -t AFP" +
" -e ISABELLE_GHC=ghc" +
@@ -392,8 +381,7 @@
args = "-a -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
- Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41",
- proxy_host = "lxbroy10", proxy_user = "i21isatest",
+ Remote_Build("AFP", "lrzcloud2",
java_heap = "8g",
options = "-m64 -M8 -U30000 -s10 -t AFP",
args = "-g large -g slow",
--- a/src/Pure/General/ssh.scala Mon Sep 12 08:07:22 2022 +0000
+++ b/src/Pure/General/ssh.scala Mon Sep 12 23:10:45 2022 +0200
@@ -1,27 +1,22 @@
/* Title: Pure/General/ssh.scala
Author: Makarius
-SSH client based on JSch (see also http://www.jcraft.com/jsch/examples).
+SSH client on OpenSSH command-line tools, preferably with connection
+multiplexing, but this does not work on Windows.
*/
package isabelle
import java.util.{Map => JMap}
-import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
-
-import scala.collection.mutable
-import scala.util.matching.Regex
-
-import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
- OpenSSHConfig, UserInfo, ChannelExec, ChannelSftp, SftpATTRS, JSchException}
+import java.net.ServerSocket
object SSH {
/* target machine: user@host syntax */
object Target {
- val User_Host: Regex = "^([^@]+)@(.+)$".r
+ private val User_Host = "^([^@]+)@(.+)$".r
def parse(s: String): (String, String) =
s match {
@@ -48,343 +43,201 @@
case Some(name) => name + "@"
}
- def connect_timeout(options: Options): Int =
- options.seconds("ssh_connect_timeout").ms.toInt
+
+ /* OpenSSH configuration and command-line */
+
+ // see https://linux.die.net/man/5/ssh_config
+ object Config {
+ def entry(x: String, y: String): String = x + "=" + y
+ def entry(x: String, y: Int): String = entry(x, y.toString)
+ def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no")
- def alive_interval(options: Options): Int =
- options.seconds("ssh_alive_interval").ms.toInt
+ def make(options: Options,
+ port: Int = default_port,
+ user: String = "",
+ control_master: Boolean = false,
+ control_path: String = ""
+ ): List[String] = {
+ List("BatchMode=yes",
+ entry("ConnectTimeout", options.seconds("ssh_connect_timeout").ms.toInt),
+ entry("ServerAliveInterval", options.seconds("ssh_alive_interval").ms.toInt),
+ entry("ServerAliveCountMax", options.int("ssh_alive_count_max")),
+ entry("Compression", options.bool("ssh_compression"))) :::
+ (if (port > 0 && port != default_port) List(entry("Port", port)) else Nil)
+ (if (user.nonEmpty) List(entry("User", user)) else Nil) :::
+ (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) :::
+ (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil)
+ }
- def alive_count_max(options: Options): Int =
- options.int("ssh_alive_count_max")
+ def make_command(command: String, config: List[String]): String =
+ Bash.string(command) + " " + config.map(entry => "-o " + Bash.string(entry)).mkString(" ")
+ }
+
+ def sftp_string(str: String): String = {
+ val special = Set(' ', '*', '?', '{', '}')
+ if (str.exists(special)) {
+ val res = new StringBuilder
+ for (c <- str) {
+ if (special(c)) res += '\\'
+ res += c
+ }
+ res.toString()
+ }
+ else str
+ }
/* open session */
- private def connect_session(
- options: Options,
- jsch: JSch,
- host: String,
- user: String = "",
- port: Int = 0,
- permissive: Boolean = false,
- nominal_host: String = "",
- nominal_user: String = "",
- nominal_port: Option[Int] = None,
- on_close: () => Unit = () => ()
- ): Session = {
- val connect_port = make_port(port)
- val session = jsch.getSession(proper_string(user).orNull, host, connect_port)
-
- session.setUserInfo(No_User_Info)
- session.setServerAliveInterval(alive_interval(options))
- session.setServerAliveCountMax(alive_count_max(options))
- session.setConfig("MaxAuthTries", "3")
- if (permissive) session.setConfig("StrictHostKeyChecking", "no")
- if (nominal_host != "") session.setHostKeyAlias(nominal_host)
-
- if (options.bool("ssh_compression")) {
- session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
- session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
- session.setConfig("compression_level", "9")
- }
- session.connect(connect_timeout(options))
- new Session(options, session, on_close,
- proper_string(nominal_host) getOrElse host,
- proper_string(nominal_user) getOrElse user,
- nominal_port getOrElse connect_port)
- }
-
def open_session(
options: Options,
host: String,
+ port: Int = 0,
user: String = "",
- port: Int = 0,
- actual_host: String = "",
- proxy_host: String = "",
- proxy_user: String = "",
- proxy_port: Int = 0,
- permissive: Boolean = false
+ multiplex: Boolean = !Platform.is_windows
): Session = {
- val config_dir = Path.explode(options.string("ssh_config_dir"))
- if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir)
-
- val jsch = new JSch
-
- val config_file = Path.explode(options.string("ssh_config_file"))
- if (config_file.is_file)
- jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file)))
-
- val known_hosts = config_dir + Path.explode("known_hosts")
- if (!known_hosts.is_file) known_hosts.file.createNewFile
- jsch.setKnownHosts(File.platform_path(known_hosts))
+ val (control_master, control_path) =
+ if (multiplex) {
+ val file = Isabelle_System.tmp_file("ssh_socket")
+ file.delete()
+ (true, file.getPath)
+ }
+ else (false, "")
- val identity_files =
- space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
- for (identity_file <- identity_files if identity_file.is_file) {
- try { jsch.addIdentity(File.platform_path(identity_file)) }
- catch {
- case exn: JSchException =>
- error("Error in ssh identity file " + identity_file + ": " + exn.getMessage)
- }
- }
-
- val connect_host = proper_string(actual_host) getOrElse host
- val connect_port = make_port(port)
- if (proxy_host == "") {
- connect_session(options, jsch, host = connect_host, user = user, port = connect_port)
- }
- else {
- val proxy =
- connect_session(options, jsch, host = proxy_host, port = proxy_port, user = proxy_user)
-
- val fw =
- try { proxy.port_forwarding(remote_host = connect_host, remote_port = connect_port) }
- catch { case exn: Throwable => proxy.close(); throw exn }
-
- try {
- connect_session(options, jsch,
- host = fw.local_host,
- port = fw.local_port,
- permissive = permissive,
- nominal_host = host,
- nominal_port = Some(connect_port),
- nominal_user = user, user = user,
- on_close = { () => fw.close(); proxy.close() })
- }
- catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
- }
+ new Session(options, host, make_port(port), user, control_master, control_path)
}
-
- /* user info */
+ class Session private[SSH](
+ val options: Options,
+ val host: String,
+ val port: Int,
+ val user: String,
+ control_master: Boolean,
+ control_path: String
+ ) extends System {
+ ssh =>
- object No_User_Info extends UserInfo {
- def getPassphrase: String = null
- def getPassword: String = null
- def promptPassword(msg: String): Boolean = false
- def promptPassphrase(msg: String): Boolean = false
- def promptYesNo(msg: String): Boolean = false
- def showMessage(msg: String): Unit = Output.writeln(msg)
- }
-
-
- /* Sftp channel */
-
- type Attrs = SftpATTRS
-
- sealed case class Dir_Entry(name: String, is_dir: Boolean) {
- def is_file: Boolean = !is_dir
- }
+ override def toString: String = user_prefix(user) + host + port_suffix(port)
+ override def hg_url: String = "ssh://" + user_prefix(user) + host + "/"
+ override def rsync_prefix: String = user_prefix(user) + host + ":"
- /* exec channel */
-
- private val exec_wait_delay = Time.seconds(0.3)
-
- class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable {
- override def toString: String = "exec " + session.toString
-
- def close(): Unit = channel.disconnect()
+ /* ssh commands */
- val exit_status: Future[Int] =
- Future.thread("ssh_wait") {
- while (!channel.isClosed) exec_wait_delay.sleep()
- channel.getExitStatus
- }
-
- val stdin: OutputStream = channel.getOutputStream
- val stdout: InputStream = channel.getInputStream
- val stderr: InputStream = channel.getErrStream
-
- // connect after preparing streams
- channel.connect(connect_timeout(session.options))
-
- def result(
+ def run_command(command: String,
+ master: Boolean = false,
+ opts: String = "",
+ args: String = "",
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
strict: Boolean = true
): Process_Result = {
- stdin.close()
-
- def read_lines(stream: InputStream, progress: String => Unit): List[String] = {
- val result = new mutable.ListBuffer[String]
- val line_buffer = new ByteArrayOutputStream(100)
- def line_flush(): Unit = {
- val line = Library.trim_line(line_buffer.toString(UTF8.charset_name))
- progress(line)
- result += line
- line_buffer.reset()
- }
-
- var c = 0
- var finished = false
- while (!finished) {
- while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c)
- if (c == 10) line_flush()
- else if (channel.isClosed) {
- if (line_buffer.size > 0) line_flush()
- finished = true
- }
- else exec_wait_delay.sleep()
- }
-
- result.toList
- }
-
- val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
- val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
-
- def terminate(): Unit = {
- close()
- out_lines.join
- err_lines.join
- exit_status.join
- }
-
- val rc =
- try { exit_status.join }
- catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
-
- close()
- if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt()
+ val config =
+ Config.make(options, port = port, user = user,
+ control_master = master, control_path = control_path)
+ val cmd =
+ Config.make_command(command, config) +
+ (if (opts.nonEmpty) " " + opts else "") +
+ (if (args.nonEmpty) " -- " + args else "")
+ Isabelle_System.bash(cmd, progress_stdout = progress_stdout,
+ progress_stderr = progress_stderr, strict = strict)
+ }
- Process_Result(rc, out_lines.join, err_lines.join)
- }
- }
-
-
- /* session */
-
- class Session private[SSH](
- val options: Options,
- session: JSch_Session,
- on_close: () => Unit,
- val nominal_host: String,
- val nominal_user: String,
- val nominal_port: Int
- ) extends System {
- ssh =>
-
- def host: String = if (session.getHost == null) "" else session.getHost
-
- override def hg_url: String =
- "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
-
- override def rsync_prefix: String =
- user_prefix(nominal_user) + nominal_host + ":"
-
- override def toString: String =
- user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
- (if (session.isConnected) "" else " (disconnected)")
-
-
- /* port forwarding */
-
- def port_forwarding(
- remote_port: Int,
- remote_host: String = "localhost",
- local_port: Int = 0,
- local_host: String = "localhost",
- ssh_close: Boolean = false
- ): Port_Forwarding = {
- val local_port1 = session.setPortForwardingL(local_host, local_port, remote_host, remote_port)
- new Port_Forwarding(local_host, local_port1, remote_host, remote_port) {
- override def close(): Unit = {
- session.delPortForwardingL(this.local_host, this.local_port)
- if (ssh_close) ssh.close()
- }
+ def run_sftp(script: String, opts: String = "", args: String = ""): Process_Result = {
+ Isabelle_System.with_tmp_file("sftp") { tmp_path =>
+ File.write(tmp_path, script)
+ val opts1 = "-b " + File.bash_path(tmp_path) + (if (opts.nonEmpty) " " + opts else "")
+ val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
+ run_command("sftp", opts = opts1, args = args1)
}
}
-
- /* sftp channel */
+ def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
+ val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
+ run_command("ssh", master = master, opts = opts, args = args1)
+ }
- private val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
- sftp.connect(connect_timeout(options))
+ def run_scp(opts: String = "", args: String = ""): Process_Result = {
+ val opts1 = "-s -p -q" + (if (opts.nonEmpty) " " + opts else "")
+ run_command("scp", opts = opts1, args = args)
+ }
+
+
+ /* init and exit */
+
+ val user_home: String = run_ssh(master = control_master, args = "printenv HOME").check.out
+
+ val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)
- override def close(): Unit = { sftp.disconnect(); session.disconnect(); on_close() }
+ override def close(): Unit = {
+ if (control_path.nonEmpty) run_ssh(opts = "-O exit").check
+ }
+
+
+ /* remote commands */
- val settings: JMap[String, String] = {
- val home = sftp.getHome
- JMap.of("HOME", home, "USER_HOME", home)
+ override def execute(cmd_line: String,
+ progress_stdout: String => Unit = (_: String) => (),
+ progress_stderr: String => Unit = (_: String) => (),
+ settings: Boolean = true,
+ strict: Boolean = true
+ ): Process_Result = {
+ val args1 = Bash.string(host) + " env " + Bash.string("USER_HOME=\"$HOME\"") + " " + cmd_line
+ run_command("ssh", args = args1, progress_stdout = progress_stdout,
+ progress_stderr = progress_stderr, strict = strict)
}
+
+ override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
+
+
+ /* remote file-system */
+
override def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
+
override def bash_path(path: Path): String = Bash.string(remote_path(path))
-
- def rm(path: Path): Unit = sftp.rm(remote_path(path))
+ def sftp_path(path: Path): String = sftp_string(remote_path(path))
- private def test_entry(path: Path, as_dir: Boolean): Boolean =
- try {
- val is_dir = sftp.stat(remote_path(path)).isDir
- if (as_dir) is_dir else !is_dir
- }
- catch { case _: SftpException => false }
+ def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path)).check
- override def is_dir(path: Path): Boolean = test_entry(path, true)
- override def is_file(path: Path): Boolean = test_entry(path, false)
+ override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok
+ override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok
override def make_directory(path: Path): Path = {
- if (!execute("mkdir -p " + remote_path(path)).ok) {
+ if (!execute("mkdir -p " + bash_path(path)).ok) {
error("Failed to create directory: " + quote(remote_path(path)))
}
path
}
- def read_dir(path: Path): List[Dir_Entry] = {
- if (!is_dir(path)) error("No such directory: " + path.toString)
-
- val dir_name = remote_path(path)
- val dir = sftp.ls(dir_name)
- (for {
- i <- (0 until dir.size).iterator
- a = dir.get(i).asInstanceOf[AnyRef]
- name = Untyped.get[String](a, "filename")
- attrs = Untyped.get[Attrs](a, "attrs")
- if name != "." && name != ".."
- }
- yield {
- Dir_Entry(name,
- if (attrs.isLink) {
- try { sftp.stat(dir_name + "/" + name).isDir }
- catch { case _: SftpException => false }
- }
- else attrs.isDir)
- }).toList.sortBy(_.name)
- }
-
- def open_input(path: Path): InputStream = sftp.get(remote_path(path))
- def open_output(path: Path): OutputStream = sftp.put(remote_path(path))
+ def read_dir(path: Path): List[String] =
+ run_sftp("ls -1 -a " + sftp_path(path)).check.out_lines.flatMap(s =>
+ if (s == "." || s == ".." || s.endsWith("/.") || s.endsWith("/..")) None
+ else Some(Library.perhaps_unprefix("./", s)))
override def read_file(path: Path, local_path: Path): Unit =
- sftp.get(remote_path(path), File.platform_path(local_path))
- override def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
- override def read(path: Path): String = using(open_input(path))(File.read_stream)
+ run_scp(args = Bash.string(host + ":" + remote_path(path)) + " " +
+ File.bash_platform_path(local_path)).check
+
+ override def read_bytes(path: Path): Bytes =
+ Isabelle_System.with_tmp_file("scp") { local_path =>
+ read_file(path, local_path)
+ Bytes.read(local_path)
+ }
+
+ override def read(path: Path): String = read_bytes(path).text
override def write_file(path: Path, local_path: Path): Unit =
- sftp.put(File.platform_path(local_path), remote_path(path))
- def write_bytes(path: Path, bytes: Bytes): Unit =
- using(open_output(path))(bytes.write_stream)
- def write(path: Path, text: String): Unit =
- using(open_output(path))(stream => Bytes(text).write_stream(stream))
-
-
- /* exec channel */
+ run_scp(args = File.bash_platform_path(local_path) + " " +
+ Bash.string(host + ":" + remote_path(path))).check
- def exec(command: String): Exec = {
- val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
- channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
- new Exec(this, channel)
- }
+ def write_bytes(path: Path, bytes: Bytes): Unit =
+ Isabelle_System.with_tmp_file("scp") { local_path =>
+ Bytes.write(local_path, bytes)
+ write_file(path, local_path)
+ }
- override def execute(command: String,
- progress_stdout: String => Unit = (_: String) => (),
- progress_stderr: String => Unit = (_: String) => (),
- settings: Boolean = true,
- strict: Boolean = true): Process_Result =
- exec(command).result(progress_stdout, progress_stderr, strict)
-
- override def isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(this))
+ def write(path: Path, text: String): Unit = write_bytes(path, Bytes(text))
/* tmp dirs */
@@ -399,19 +252,48 @@
override def with_tmp_dir[A](body: Path => A): A = {
val remote_dir = tmp_dir()
- try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
+ try { body(Path.explode(remote_dir)) }
+ finally { rm_tree(remote_dir) }
+ }
+
+
+ /* port forwarding */
+
+ def port_forwarding(
+ remote_port: Int,
+ remote_host: String = "localhost",
+ local_port: Int = 0,
+ local_host: String = "localhost",
+ ssh_close: Boolean = false
+ ): Port_Forwarding = {
+ val port =
+ if (local_port > 0) local_port
+ else {
+ // FIXME race condition
+ val dummy = new ServerSocket(0)
+ val port = dummy.getLocalPort
+ dummy.close()
+ port
+ }
+ val string = List(local_host, port, remote_host, remote_port).mkString(":")
+ run_ssh(opts = "-L " + Bash.string(string) + " -O forward").check
+
+ new Port_Forwarding(host, port, remote_host, remote_port) {
+ override def toString: String = string
+ override def close(): Unit = {
+ run_ssh(opts = "-L " + Bash.string(string) + " -O cancel").check
+ if (ssh_close) ssh.close()
+ }
+ }
}
}
abstract class Port_Forwarding private[SSH](
- val local_host: String,
- val local_port: Int,
+ val host: String,
+ val port: Int,
val remote_host: String,
val remote_port: Int
- ) extends AutoCloseable {
- override def toString: String =
- local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
- }
+ ) extends AutoCloseable
/* system operations */