diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala +++ b/src/Pure/Admin/build_history.scala @@ -1,592 +1,592 @@ /* Title: Pure/Admin/build_history.scala Author: Makarius Build other history versions. */ package isabelle object Build_History { /* log files */ val engine = "build_history" val log_prefix = engine + "_" /* augment settings */ def augment_settings( other_isabelle: Other_Isabelle, threads: Int, arch_64: Boolean, heap: Int, max_heap: Option[Int], more_settings: List[String] ): String = { val (ml_platform, ml_settings) = { val cygwin_32 = "x86-cygwin" val windows_32 = "x86-windows" val windows_64 = "x86_64-windows" val windows_64_32 = "x86_64_32-windows" val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32") val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64") val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-") val polyml_home = try { Path.explode(other_isabelle.getenv("ML_HOME")).dir } catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) } def ml_home(platform: String): Path = polyml_home + Path.explode(platform) def err(platform: String): Nothing = error("Platform " + platform + " unavailable on this machine") def check_dir(platform: String): Boolean = platform != "" && ml_home(platform).is_dir val ml_platform = if (Platform.is_windows && arch_64) { if (check_dir(windows_64)) windows_64 else err(windows_64) } else if (Platform.is_windows && !arch_64) { if (check_dir(windows_64_32)) windows_64_32 else if (check_dir(cygwin_32)) cygwin_32 else if (check_dir(windows_32)) windows_32 else err(windows_32) } else if (arch_64) { if (check_dir(platform_64)) platform_64 else err(platform_64) } else if (check_dir(platform_64_32)) platform_64_32 else platform_32 val ml_options = "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + " --gcthreads " + threads + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") (ml_platform, List( "ML_HOME=" + File.bash_path(ml_home(ml_platform)), "ML_PLATFORM=" + quote(ml_platform), "ML_OPTIONS=" + quote(ml_options))) } val thread_settings = List( "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") val settings = List(ml_settings, thread_settings) ::: (if (more_settings.isEmpty) Nil else List(more_settings)) File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) ml_platform } /** local build **/ private val default_multicore = (1, 1) private val default_heap = 1500 private val default_isabelle_identifier = "build_history" def local_build( options: Options, root: Path, progress: Progress = new Progress, afp: Boolean = false, afp_partition: Int = 0, isabelle_identifier: String = default_isabelle_identifier, ml_statistics_step: Int = 1, component_repository: String = Components.default_component_repository, components_base: String = Components.standard_components_base, fresh: Boolean = false, hostname: String = "", multicore_base: Boolean = false, multicore_list: List[(Int, Int)] = List(default_multicore), arch_64: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, init_settings: List[String] = Nil, more_settings: List[String] = Nil, more_preferences: List[String] = Nil, verbose: Boolean = false, build_tags: List[String] = Nil, build_args: List[String] = Nil ): List[(Process_Result, Path)] = { /* sanity checks */ if (File.eq(Path.ISABELLE_HOME, root)) { error("Repository coincides with ISABELLE_HOME=" + Path.ISABELLE_HOME.expand) } for ((threads, _) <- multicore_list if threads < 1) { error("Bad threads value < 1: " + threads) } for ((_, processes) <- multicore_list if processes < 1) { error("Bad processes value < 1: " + processes) } if (heap < 100) error("Bad heap value < 100: " + heap) if (max_heap.isDefined && max_heap.get < heap) { error("Bad max_heap value < heap: " + max_heap.get) } System.getenv("ISABELLE_SETTINGS_PRESENT") match { case null | "" => case _ => error("Cannot run Admin/build_other within existing Isabelle settings environment") } /* Isabelle + AFP directory */ def directory(dir: Path): Mercurial.Hg_Sync.Directory = { val directory = Mercurial.Hg_Sync.directory(dir) if (verbose) progress.echo(directory.log) directory } val isabelle_directory = directory(root) val afp_directory = if (afp) Some(directory(root + Path.explode("AFP"))) else None val (afp_build_args, afp_sessions) = if (afp_directory.isEmpty) (Nil, Nil) else { val (opt, sessions) = { if (afp_partition == 0) ("-d", Nil) else { try { val afp_info = AFP.init(options, base_dir = afp_directory.get.root) ("-d", afp_info.partition(afp_partition)) } catch { case ERROR(_) => ("-D", Nil) } } } (List(opt, "~~/AFP/thys"), sessions) } /* main */ val other_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = progress) val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname() val build_history_date = Date.now() val build_group_id = build_host + ":" + build_history_date.time.ms var first_build = true for ((threads, processes) <- multicore_list) yield { /* init settings */ val component_settings = other_isabelle.init_components( component_repository = component_repository, components_base = components_base, catalogs = Components.optional_catalogs) other_isabelle.init_settings(component_settings ::: init_settings) other_isabelle.resolve_components(echo = verbose) val ml_platform = augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) File.write(other_isabelle.etc_preferences, cat_lines(more_preferences)) val isabelle_output = other_isabelle.expand_path( Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")) val isabelle_output_log = isabelle_output + Path.explode("log") val isabelle_base_log = isabelle_output + Path.explode("../base_log") if (first_build) { other_isabelle.resolve_components(echo = verbose) other_isabelle.scala_build(fresh = fresh, echo = verbose) for { tool <- List("ghc_setup", "ocaml_setup") if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" && (other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file } other_isabelle.bash("bin/isabelle " + tool, echo = verbose) Isabelle_System.rm_tree(isabelle_base_log) } Isabelle_System.rm_tree(isabelle_output) Isabelle_System.make_directory(isabelle_output) other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/mash_state")).file.delete val log_path = other_isabelle.isabelle_home_user + Build_Log.log_subdir(build_history_date) + Build_Log.log_filename(Build_History.engine, build_history_date, List(build_host, ml_platform, "M" + threads) ::: build_tags) Isabelle_System.make_directory(log_path.dir) val build_out = other_isabelle.expand_path(Path.explode("$ISABELLE_HOME_USER/log/build.out")) val build_out_progress = new File_Progress(build_out) build_out.file.delete /* build */ if (multicore_base && !first_build && isabelle_base_log.is_dir) { Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log) } val build_start = Date.now() val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args val build_result = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, progress = build_out_progress) .bash("bin/isabelle build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true, strict = false) val build_end = Date.now() val build_info: Build_Log.Build_Info = Build_Log.Log_File(log_path.file_name, build_result.out_lines). parse_build_info(ml_statistics = true) /* output log */ val store = Sessions.store(options + "build_database_server=false") val meta_info = Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) ::: Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) ::: List( Build_Log.Prop.build_group_id.name -> build_group_id, Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms), Build_Log.Prop.build_engine.name -> Build_History.engine, Build_Log.Prop.build_host.name -> build_host, Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start), Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end), Build_Log.Prop.isabelle_version.name -> isabelle_directory.id) ::: afp_directory.map(dir => Build_Log.Prop.afp_version.name -> dir.id).toList build_out_progress.echo("Reading session build info ...") val session_build_info = build_info.finished_sessions.flatMap { session_name => val database = isabelle_output + store.database(session_name) if (database.is_file) { using(SQLite.open_database(database)) { db => val theory_timings = try { store.read_theory_timings(db, session_name).map(ps => Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps)) } catch { case ERROR(_) => Nil } val session_sources = store.read_build(db, session_name).map(_.sources) match { case Some(sources) if sources.length == SHA1.digest_length => List("Sources " + session_name + " " + sources) case _ => Nil } theory_timings ::: session_sources } } else Nil } build_out_progress.echo("Reading ML statistics ...") val ml_statistics = build_info.finished_sessions.flatMap { session_name => val database = isabelle_output + store.database(session_name) val log_gz = isabelle_output + store.log_gz(session_name) val properties = if (database.is_file) { using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name)) } else if (log_gz.is_file) { Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics } else Nil val trimmed_properties = if (ml_statistics_step <= 0) Nil else if (ml_statistics_step == 1) properties else { (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 } yield ps).toList } trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps) } build_out_progress.echo("Reading error messages ...") val session_errors = build_info.failed_sessions.flatMap { session_name => val database = isabelle_output + store.database(session_name) val errors = if (database.is_file) { try { using(SQLite.open_database(database))(db => store.read_errors(db, session_name)) } // column "errors" could be missing catch { case _: java.sql.SQLException => Nil } } else Nil errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg)) } build_out_progress.echo("Reading heap sizes ...") val heap_sizes = build_info.finished_sessions.flatMap { session_name => val heap = isabelle_output + Path.explode(session_name) if (heap.is_file) { Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)") } else None } build_out_progress.echo("Writing log file " + log_path.xz + " ...") File.write_xz(log_path.xz, terminate_lines( Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: session_build_info ::: ml_statistics.map(Protocol.ML_Statistics_Marker.apply) ::: session_errors.map(Protocol.Error_Message_Marker.apply) ::: heap_sizes), Compress.Options_XZ(6)) /* next build */ if (multicore_base && first_build && isabelle_output_log.is_dir) { Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) } Isabelle_System.rm_tree(isabelle_output) first_build = false (build_result, log_path.xz) } } /* command line entry point */ private object Multicore { private val Pat1 = """^(\d+)$""".r private val Pat2 = """^(\d+)x(\d+)$""".r def parse(s: String): (Int, Int) = s match { case Pat1(Value.Int(x)) => (x, 1) case Pat2(Value.Int(x), Value.Int(y)) => (x, y) case _ => error("Bad multicore configuration: " + quote(s)) } } def main(args: Array[String]): Unit = { Command_Line.tool { var afp = false var multicore_base = false var components_base = Components.standard_components_base var heap: Option[Int] = None var max_heap: Option[Int] = None var multicore_list = List(default_multicore) var isabelle_identifier = default_isabelle_identifier var afp_partition = 0 var component_repository = Components.default_component_repository var more_settings: List[String] = Nil var more_preferences: List[String] = Nil var fresh = false var hostname = "" var init_settings: List[String] = Nil var arch_64 = false var output_file = "" var ml_statistics_step = 1 var build_tags = List.empty[String] var verbose = false var exit_code = false val getopts = Getopts(""" Usage: Admin/build_other [OPTIONS] ISABELLE_HOME [ARGS ...] Options are: -A include $ISABELLE_HOME/AFP directory -B first multicore build serves as base for scheduling information -C DIR base directory for Isabelle components (default: """ + quote(Components.standard_components_base) + """) -H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64) -M MULTICORE multicore configurations (see below) -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """) -P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted) -R URL remote repository for Isabelle components (default: """ + Components.default_component_repository + """) -U SIZE maximal ML heap in MB (default: unbounded) -e TEXT additional text for generated etc/settings -f fresh build of Isabelle/Scala components (recommended) -h NAME override local hostname -i TEXT initial text for generated etc/settings -m ARCH processor architecture (32=x86, 64=x86_64, default: x86) -n no build: sync only -o FILE output file for log names (default: stdout) -p TEXT additional text for generated etc/preferences -s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1) -t TAG free-form build tag (multiple occurrences possible) -v verbose -x return overall exit code from build processes Build Isabelle sessions from the history of another REPOSITORY clone, passing ARGS directly to its isabelle build tool. Each MULTICORE configuration consists of one or two numbers (default 1): THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4. """, "A" -> (_ => afp = true), "B" -> (_ => multicore_base = true), "C:" -> (arg => components_base = arg), "H:" -> (arg => heap = Some(Value.Int.parse(arg))), "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)), "N:" -> (arg => isabelle_identifier = arg), "P:" -> (arg => afp_partition = Value.Int.parse(arg)), "R:" -> (arg => component_repository = arg), "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), "h:" -> (arg => hostname = arg), "i:" -> (arg => init_settings = init_settings ::: List(arg)), "m:" -> { case "32" | "x86" => arch_64 = false case "64" | "x86_64" => arch_64 = true case bad => error("Bad processor architecture: " + quote(bad)) }, "o:" -> (arg => output_file = arg), "p:" -> (arg => more_preferences = more_preferences ::: List(arg)), "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)), "t:" -> (arg => build_tags = build_tags ::: List(arg)), "v" -> (_ => verbose = true), "x" -> (_ => exit_code = true)) val more_args = getopts(args) val (root, build_args) = more_args match { case root :: build_args => (Path.explode(root), build_args) case _ => getopts.usage() } val progress = new Console_Progress(stderr = true) val results = local_build(Options.init(), root, progress = progress, afp = afp, afp_partition = afp_partition, isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, component_repository = component_repository, components_base = components_base, fresh = fresh, hostname = hostname, multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, init_settings = init_settings, more_settings = more_settings, more_preferences = more_preferences, verbose = verbose, build_tags = build_tags, build_args = build_args) if (output_file.isEmpty) { for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true) } else { File.write(Path.explode(output_file), cat_lines(for ((_, log_path) <- results) yield log_path.implode)) } val rc = results.foldLeft(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc } if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc) } } /** remote build -- via rsync and ssh **/ def remote_build( ssh: SSH.Session, isabelle_self: Path, isabelle_other: Path, isabelle_identifier: String = "remote_build_history", progress: Progress = new Progress, protect_args: Boolean = false, rev: String = "", afp_repos: Option[Path] = None, afp_rev: String = "", options: String = "", args: String = "", no_build: Boolean = false ): List[(String, Bytes)] = { /* synchronize Isabelle + AFP repositories */ def sync(target: Path, accurate: Boolean = false, rev: String = "", afp_rev: String = "", afp: Boolean = false ): Unit = { val context = Rsync.Context(progress, ssh_port = ssh.port, ssh_control_path = ssh.control_path, protect_args = protect_args) Sync.sync(ssh.options, context, ssh.rsync_path(target), thorough = accurate, preserve_jars = !accurate, rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None) } def execute(command: String, args: String, echo: Boolean = false, strict: Boolean = true ): Unit = ssh.execute( Isabelle_System.export_isabelle_identifier(isabelle_identifier) + ssh.bash_path(isabelle_self + Path.explode(command)) + " " + args, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), strict = strict).check sync(isabelle_self) execute("bin/isabelle", "components -I") execute("bin/isabelle", "components -a", echo = true) execute("bin/isabelle", "jedit -bf") sync(isabelle_other, accurate = true, rev = proper_string(rev) getOrElse "tip", afp_rev = proper_string(afp_rev) getOrElse "tip", afp = true) /* build */ if (no_build) Nil else { ssh.with_tmp_dir { tmp_dir => val output_file = tmp_dir + Path.explode("output") val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options try { execute("Admin/build_other", "-o " + ssh.bash_path(output_file) + build_options + " " + ssh.bash_path(isabelle_other) + " " + args, echo = true, strict = false) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for Admin/build_other " + build_options) } for (line <- split_lines(ssh.read(output_file))) yield { val log = Path.explode(line) val bytes = ssh.read_bytes(log) - ssh.rm(log) + ssh.delete(log) (log.file_name, bytes) } } } } } 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,396 +1,417 @@ /* 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, + redirect: Boolean = false, 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) + Isabelle_System.bash(cmd, cwd = cwd, + redirect = redirect, + 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: Isabelle_System.Settings = (name: String) => if (name == "HOME" || name == "USER_HOME") user_home else "" 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) => (), + redirect: Boolean = false, settings: Boolean = true, strict: Boolean = true ): Process_Result = { run_command("ssh", args = Bash.string(host) + " " + Bash.string(cmd_line), progress_stdout = progress_stdout, progress_stderr = progress_stderr, + redirect = redirect, 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) override def absolute_path(path: Path): Path = { val path1 = expand_path(path) if (path1.is_absolute) path1 else Path.explode(user_home) + path1 } 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 delete(path: Path): Unit = { + val cmd = if (is_dir(path)) "rmdir" else if (is_file(path)) "rm" else "" + if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path)) + } + + override def set_executable(path: Path, flag: Boolean): Unit = + if (!execute("chmod a" + (if (flag) "+" else "-") + "x " + bash_path(path)).ok) { + error("Failed to change executable status of " + quote(remote_path(path))) + } + 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 = + override def write_bytes(path: Path, bytes: Bytes): Unit = put_file(path, Bytes.write(_, bytes)) - def write(path: Path, text: String): Unit = + override 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)) + override 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 absolute_path(path: Path): Path = path.absolute 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 delete(path: Path): Unit = path.file.delete + def set_executable(path: Path, flag: Boolean): Unit = File.set_executable(path, flag) def make_directory(path: Path): Path = Isabelle_System.make_directory(path) + def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir) 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 write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) + def write_bytes(path: Path, bytes: Bytes): Unit = Bytes.write(path, bytes) + def write(path: Path, text: String): Unit = File.write(path, text) def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), + redirect: Boolean = false, settings: Boolean = true, strict: Boolean = true): Process_Result = Isabelle_System.bash(command, progress_stdout = progress_stdout, progress_stderr = progress_stderr, + redirect = redirect, 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 }