diff --git a/src/Pure/General/ssh.scala b/src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala +++ b/src/Pure/General/ssh.scala @@ -1,378 +1,387 @@ /* Title: Pure/General/ssh.scala Author: Makarius SSH client on OpenSSH command-line tools, preferably with connection multiplexing, but this does not work on Windows. */ package isabelle import java.util.{Map => JMap} import java.io.{File => JFile} object SSH { /* client command */ def client_command(port: Int = 0, control_path: String = ""): String = if (control_path.isEmpty || control_path == Bash.string(control_path)) { "ssh" + (if (port > 0) " -p " + port else "") + (if (control_path.nonEmpty) " -o ControlPath=" + control_path else "") } else error ("Malformed SSH control socket: " + quote(control_path)) /* 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: Long): String = entry(x, y.toString) def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no") def make(options: Options, port: Int = 0, user: String = "", control_master: Boolean = false, control_path: String = "" ): List[String] = { val ssh_batch_mode = options.bool("ssh_batch_mode") val ssh_compression = options.bool("ssh_compression") val ssh_alive_interval = options.real("ssh_alive_interval").round val ssh_alive_count_max = options.int("ssh_alive_count_max") List( entry("BatchMode", ssh_batch_mode), entry("Compression", ssh_compression)) ::: (if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) ::: (if (ssh_alive_count_max >= 0) List(entry("ServerAliveCountMax", ssh_alive_count_max)) else Nil) ::: (if (port > 0) List(entry("Port", port)) else Nil) ::: (if (user.nonEmpty) List(entry("User", user)) else Nil) ::: (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) ::: (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil) } def option(entry: String): String = "-o " + Bash.string(entry) def option(x: String, y: String): String = option(entry(x, y)) def option(x: String, y: Int): String = option(entry(x, y)) def option(x: String, y: Long): String = option(entry(x, y)) def option(x: String, y: Boolean): String = option(entry(x, y)) def command(command: String, config: List[String]): String = Bash.string(command) + config.map(entry => " " + option(entry)).mkString } def sftp_string(str: String): String = { val special = "[]?*\\{} \"'" if (str.isEmpty) "\"\"" else if (str.exists(special.contains)) { val res = new StringBuilder for (c <- str) { if (special.contains(c)) res += '\\' res += c } res.toString() } else str } /* open session */ def open_session( options: Options, host: String, port: Int = 0, user: String = "" ): Session = { val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows val (control_master, control_path) = if (multiplex) (true, Isabelle_System.tmp_file("ssh", initialized = false).getPath) else (false, "") new Session(options, host, port, user, control_master, control_path) } class Session private[SSH]( val options: Options, val host: String, val port: Int, val user: String, control_master: Boolean, val control_path: String ) extends System { ssh => def port_suffix: String = if (port > 0) ":" + port else "" def user_prefix: String = if (user.nonEmpty) user + "@" else "" override def toString: String = user_prefix + host + port_suffix override def hg_url: String = "ssh://" + toString + "/" override def rsync_prefix: String = user_prefix + host + ":" /* local ssh commands */ def run_command(command: String, master: Boolean = false, opts: String = "", args: String = "", cwd: JFile = null, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true ): Process_Result = { val config = Config.make(options, port = port, user = user, control_master = master, control_path = control_path) val cmd = Config.command(command, config) + (if (opts.nonEmpty) " " + opts else "") + (if (args.nonEmpty) " -- " + args else "") Isabelle_System.bash(cmd, cwd = cwd, progress_stdout = progress_stdout, progress_stderr = progress_stderr, strict = strict) } def run_sftp( script: String, init: Path => Unit = _ => (), exit: Path => Unit = _ => () ): Process_Result = { Isabelle_System.with_tmp_dir("ssh") { dir => init(dir) File.write(dir + Path.explode("script"), script) val result = run_command("sftp", opts = "-b script", args = Bash.string(host), cwd = dir.file).check exit(dir) result } } 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) } /* init and exit */ val user_home: String = { run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines match { case List(user_home, shell) => if (shell.endsWith("/bash")) user_home else { error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell) } case _ => error("Malformed remote environment for " + quote(toString)) } } val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home) override def close(): Unit = { if (control_path.nonEmpty) run_ssh(opts = "-O exit").check } /* remote commands */ override def execute(cmd_line: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), settings: Boolean = true, strict: Boolean = true ): Process_Result = { val args1 = Bash.string(host) + " " + Bash.string("export USER_HOME=\"$HOME\"\n" + cmd_line) run_command("ssh", args = args1, progress_stdout = progress_stdout, progress_stderr = progress_stderr, strict = strict) } override def download_file( url_name: String, file: Path, progress: Progress = new Progress ): Unit = { val cmd_line = File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" + "download_file " + Bash.string(url_name) + " " + bash_path(file) execute(cmd_line, progress_stdout = progress.echo, progress_stderr = progress.echo).check } override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh)) /* remote file-system */ override def expand_path(path: Path): Path = path.expand_env(settings) def remote_path(path: Path): String = expand_path(path).implode override def bash_path(path: Path): String = Bash.string(remote_path(path)) def sftp_path(path: Path): String = sftp_string(remote_path(path)) def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path)) override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok override def make_directory(path: Path): Path = { if (!execute("mkdir -p " + bash_path(path)).ok) { error("Failed to create directory: " + quote(remote_path(path))) } path } + override def copy_file(src: Path, dst: Path): Unit = { + val direct = if (is_dir(dst)) "/." else "" + if (!execute("cp -a " + bash_path(src) + " " + bash_path(dst) + direct).ok) { + error("Failed to copy file " + expand_path(src) + " to " + + expand_path(dst) + " (ssh " + toString + ")") + } + } + def read_dir(path: Path): List[String] = run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s => if (s == "." || s == "..") None else Some(Library.perhaps_unprefix("./", s))) private def get_file[A](path: Path, f: Path => A): A = { var result: Option[A] = None run_sftp("get -p " + sftp_path(path) + " local", exit = dir => result = Some(f(dir + Path.explode("local")))) result.get } private def put_file(path: Path, f: Path => Unit): Unit = run_sftp("put -p local " + sftp_path(path), init = dir => f(dir + Path.explode("local"))) override def read_file(path: Path, local_path: Path): Unit = get_file(path, Isabelle_System.copy_file(_, local_path)) override def read_bytes(path: Path): Bytes = get_file(path, Bytes.read) override def read(path: Path): String = get_file(path, File.read) override def write_file(path: Path, local_path: Path): Unit = put_file(path, Isabelle_System.copy_file(local_path, _)) def write_bytes(path: Path, bytes: Bytes): Unit = put_file(path, Bytes.write(_, bytes)) def write(path: Path, text: String): Unit = put_file(path, File.write(_, text)) /* tmp dirs */ def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) def rm_tree(remote_dir: String): Unit = execute("rm -r -f " + Bash.string(remote_dir)).check def tmp_dir(): String = execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out override def with_tmp_dir[A](body: Path => A): A = { val remote_dir = tmp_dir() try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } } /* port forwarding */ def port_forwarding( remote_port: Int, remote_host: String = "localhost", local_port: Int = 0, local_host: String = "localhost", ssh_close: Boolean = false ): Port_Forwarding = { val port = if (local_port > 0) local_port else Isabelle_System.local_port() val forward = List(local_host, port, remote_host, remote_port).mkString(":") val forward_option = "-L " + Bash.string(forward) val cancel: () => Unit = if (control_path.nonEmpty) { run_ssh(opts = forward_option + " -O forward").check () => run_ssh(opts = forward_option + " -O cancel") // permissive } else { val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false)) val thread = Isabelle_Thread.fork("port_forwarding") { val opts = forward_option + " " + Config.option("SessionType", "none") + " " + Config.option("PermitLocalCommand", true) + " " + Config.option("LocalCommand", "pwd") try { run_command("ssh", opts = opts, args = Bash.string(host), progress_stdout = _ => result.change(_ => Exn.Res(true))).check } catch { case exn: Throwable => result.change(_ => Exn.Exn(exn)) } } result.guarded_access { case res@Exn.Res(ok) => if (ok) Some((), res) else None case Exn.Exn(exn) => throw exn } () => thread.interrupt() } val shutdown_hook = Isabelle_System.create_shutdown_hook { cancel() } new Port_Forwarding(host, port, remote_host, remote_port) { override def toString: String = forward override def close(): Unit = { cancel() Isabelle_System.remove_shutdown_hook(shutdown_hook) if (ssh_close) ssh.close() } } } } abstract class Port_Forwarding private[SSH]( val host: String, val port: Int, val remote_host: String, val remote_port: Int ) extends AutoCloseable /* system operations */ trait System extends AutoCloseable { def close(): Unit = () def hg_url: String = "" def rsync_prefix: String = "" def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode def expand_path(path: Path): Path = path.expand def bash_path(path: Path): String = File.bash_path(path) def is_dir(path: Path): Boolean = path.is_dir def is_file(path: Path): Boolean = path.is_file def make_directory(path: Path): Path = Isabelle_System.make_directory(path) def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body) + def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) def read_bytes(path: Path): Bytes = Bytes.read(path) def read(path: Path): String = File.read(path) def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), settings: Boolean = true, strict: Boolean = true): Process_Result = Isabelle_System.bash(command, progress_stdout = progress_stdout, progress_stderr = progress_stderr, env = if (settings) Isabelle_System.settings() else null, strict = strict) def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Isabelle_System.download_file(url_name, file, progress = progress) def isabelle_platform: Isabelle_Platform = Isabelle_Platform() } object Local extends System } diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala --- a/src/Pure/System/components.scala +++ b/src/Pure/System/components.scala @@ -1,378 +1,388 @@ /* Title: Pure/System/components.scala Author: Makarius Isabelle system components. */ package isabelle import java.io.{File => JFile} object Components { /* archive name */ object Archive { val suffix: String = ".tar.gz" def apply(name: String): String = if (name == "") error("Bad component name: " + quote(name)) else name + suffix def unapply(archive: String): Option[String] = { for { name0 <- Library.try_unsuffix(suffix, archive) name <- proper_string(name0) } yield name } def get_name(archive: String): String = unapply(archive) getOrElse error("Bad component archive name (expecting .tar.gz): " + quote(archive)) } /* component collections */ def default_component_repository: String = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") val default_catalogs: List[String] = List("main") val optional_catalogs: List[String] = List("main", "optional") def admin(dir: Path): Path = dir + Path.explode("Admin/components") def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) - def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = { + def unpack( + dir: Path, + archive: Path, + ssh: SSH.System = SSH.Local, + progress: Progress = new Progress + ): String = { val name = Archive.get_name(archive.file_name) progress.echo("Unpacking " + name) - Isabelle_System.bash( - "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive)).check + ssh.execute( + "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive), + progress_stdout = progress.echo, + progress_stderr = progress.echo).check name } - def resolve(base_dir: Path, names: List[String], + def resolve( + base_dir: Path, + names: List[String], target_dir: Option[Path] = None, copy_dir: Option[Path] = None, component_repository: String = Components.default_component_repository, + ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { - Isabelle_System.make_directory(base_dir) + ssh.make_directory(base_dir) for (name <- names) { val archive_name = Archive(name) val archive = base_dir + Path.explode(archive_name) - if (!archive.is_file) { + if (!ssh.is_file(archive)) { val remote = Url.append_path(component_repository, archive_name) - Isabelle_System.download_file(remote, archive, progress = progress) + ssh.download_file(remote, archive, progress = progress) } for (dir <- copy_dir) { - Isabelle_System.make_directory(dir) - Isabelle_System.copy_file(archive, dir) + ssh.make_directory(dir) + ssh.copy_file(archive, dir) } - unpack(target_dir getOrElse base_dir, archive, progress = progress) + unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress) } } private val platforms_family: Map[Platform.Family.Value, Set[String]] = Map( Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"), Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"), Platform.Family.macos -> Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), Platform.Family.windows -> Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) private val platforms_all: Set[String] = Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2) def purge(dir: Path, platform: Platform.Family.Value): Unit = { val purge_set = platforms_all -- platforms_family(platform) File.find_files(dir.file, (file: JFile) => file.isDirectory && purge_set(file.getName), include_dirs = true).foreach(Isabelle_System.rm_tree) } /* component directories */ def directories(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) /* component directory content */ object Directory { def apply(path: Path): Directory = new Directory(path.absolute) } class Directory private(val path: Path) { override def toString: String = path.toString def etc: Path = path + Path.basic("etc") def src: Path = path + Path.basic("src") def lib: Path = path + Path.basic("lib") def settings: Path = etc + Path.basic("settings") def components: Path = etc + Path.basic("components") def build_props: Path = etc + Path.basic("build.props") def README: Path = path + Path.basic("README") def LICENSE: Path = path + Path.basic("LICENSE") def create(progress: Progress = new Progress): Directory = { progress.echo("Creating component directory " + path) Isabelle_System.new_directory(path) Isabelle_System.make_directory(etc) this } def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path) def check: Directory = if (!path.is_dir) error("Bad component directory: " + path) else if (!ok) { error("Malformed component directory: " + path + "\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")") } else this def read_components(): List[String] = split_lines(File.read(components)).filter(_.nonEmpty) def write_components(lines: List[String]): Unit = File.write(components, terminate_lines(lines)) def write_settings(text: String): Unit = File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) } /* component repository content */ val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) { override def toString: String = digest.shasum(name) } def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => Word.explode(line) match { case Nil => None case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name)) case _ => error("Bad components.sha1 entry: " + quote(line)) }) def write_components_sha1(entries: List[SHA1_Digest]): Unit = File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n")) /** manage user components **/ val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components") def read_components(): List[String] = if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) else Nil def write_components(lines: List[String]): Unit = { Isabelle_System.make_directory(components_path.dir) File.write(components_path, Library.terminate_lines(lines)) } def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { val path = path0.expand.absolute if (add) Directory(path).check val lines1 = read_components() val lines2 = lines1.filter(line => line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) val lines3 = if (add) lines2 ::: List(path.implode) else lines2 if (lines1 != lines3) write_components(lines3) val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" progress.echo(prefix + " component " + path) } /* main entry point */ def main(args: Array[String]): Unit = { Command_Line.tool { for (arg <- args) { val add = if (arg.startsWith("+")) true else if (arg.startsWith("-")) false else error("Bad argument: " + quote(arg)) val path = Path.explode(arg.substring(1)) update_components(add, path, progress = new Console_Progress) } } } /** build and publish components **/ def build_components( options: Options, components: List[Path], progress: Progress = new Progress, publish: Boolean = false, force: Boolean = false, update_components_sha1: Boolean = false ): Unit = { val archives: List[Path] = for (path <- components) yield { path.file_name match { case Archive(_) => path case name => Directory(path).check val component_path = path.expand val archive_dir = component_path.dir val archive_name = Archive(name) val archive = archive_dir + Path.explode(archive_name) if (archive.is_file && !force) { error("Component archive already exists: " + archive) } progress.echo("Packaging " + archive_name) Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), dir = archive_dir).check archive } } if ((publish && archives.nonEmpty) || update_components_sha1) { val server = options.string("isabelle_components_server") if (server.isEmpty) error("Undefined option isabelle_components_server") using(SSH.open_session(options, server)) { ssh => val components_dir = Path.explode(options.string("isabelle_components_dir")) val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { error("Bad remote directory: " + dir) } if (publish) { for (archive <- archives) { val archive_name = archive.file_name val name = Archive.get_name(archive_name) val remote_component = components_dir + archive.base val remote_contrib = contrib_dir + Path.explode(name) // component archive if (ssh.is_file(remote_component) && !force) { error("Remote component archive already exists: " + remote_component) } progress.echo("Uploading " + archive_name) ssh.write_file(remote_component, archive) // contrib directory val is_standard_component = Isabelle_System.with_tmp_dir("component") { tmp_dir => Isabelle_System.extract(archive, tmp_dir) Directory(tmp_dir + Path.explode(name)).ok } if (is_standard_component) { if (ssh.is_dir(remote_contrib)) { if (force) ssh.rm_tree(remote_contrib) else error("Remote component directory already exists: " + remote_contrib) } progress.echo("Unpacking remote " + archive_name) ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + ssh.bash_path(remote_component)).check } else { progress.echo_warning("No unpacking of non-standard component: " + archive_name) } } } // remote SHA1 digests if (update_components_sha1) { val lines = for { entry <- ssh.read_dir(components_dir) if ssh.is_file(components_dir + Path.basic(entry)) && entry.endsWith(Archive.suffix) } yield { progress.echo("Digesting remote " + entry) ssh.execute("cd " + ssh.bash_path(components_dir) + "; sha1sum " + Bash.string(entry)).check.out } write_components_sha1(read_components_sha1(lines)) } } } // local SHA1 digests { val new_entries = for (archive <- archives) yield { val name = archive.file_name progress.echo("Digesting local " + name) SHA1_Digest(SHA1.digest(archive), name) } val new_names = new_entries.map(_.name).toSet write_components_sha1( new_entries ::: read_components_sha1().filterNot(entry => new_names.contains(entry.name))) } } /* Isabelle tool wrapper */ private val relevant_options = List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") val isabelle_tool = Isabelle_Tool("build_components", "build and publish Isabelle components", Scala_Project.here, { args => var publish = false var update_components_sha1 = false var force = false var options = Options.init() def show_options: String = cat_lines(relevant_options.flatMap(options.get).map(_.print)) val getopts = Getopts(""" Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... Options are: -P publish on SSH server (see options below) -f force: overwrite existing component archives and directories -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u update all SHA1 keys in Isabelle repository Admin/components Build and publish Isabelle components as .tar.gz archives on SSH server, depending on system options: """ + Library.indent_lines(2, show_options) + "\n", "P" -> (_ => publish = true), "f" -> (_ => force = true), "o:" -> (arg => options = options + arg), "u" -> (_ => update_components_sha1 = true)) val more_args = getopts(args) if (more_args.isEmpty && !update_components_sha1) getopts.usage() val progress = new Console_Progress build_components(options, more_args.map(Path.explode), progress = progress, publish = publish, force = force, update_components_sha1 = update_components_sha1) }) }