diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,381 +1,384 @@ (* :mode=isabelle-options: *) section "Document Preparation" option browser_info : bool = false -- "generate theory browser information" option document : string = "" (standard "true") -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")" option document_output : string = "" (standard "output") -- "document output directory" option document_echo : bool = false -- "inform about document file names during session presentation" option document_variants : string = "document" -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" option document_bibliography : bool = false -- "explicitly enable use of bibtex (default: according to presence of root.bib)" option document_build : string = "lualatex" (standard "build") -- "document build engine (e.g. build, lualatex, pdflatex)" option document_logo : string = "" -- "generate named instance of Isabelle logo (underscore means unnamed variant)" option document_heading_prefix : string = "isamarkup" (standard) -- "prefix for LaTeX macros generated from 'chapter', 'section' etc." option document_comment_latex : bool = false -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" option thy_output_break : bool = false -- "control line breaks in non-display material" option thy_output_cartouche : bool = false -- "indicate if the output should be delimited as cartouche" option thy_output_quotes : bool = false -- "indicate if the output should be delimited via double quotes" option thy_output_margin : int = 76 -- "right margin / page width for printing of display material" option thy_output_indent : int = 0 -- "indentation for pretty printing of display material" option thy_output_source : bool = false -- "print original source text rather than internal representation" option thy_output_source_cartouche : bool = false -- "print original source text rather than internal representation, preserve cartouches" option thy_output_modes : string = "" -- "additional print modes for document output (separated by commas)" section "Prover Output" option show_types : bool = false -- "show type constraints when printing terms" option show_sorts : bool = false -- "show sort constraints when printing types" option show_brackets : bool = false -- "show extra brackets when printing terms/types" option show_question_marks : bool = true -- "show leading question mark of schematic variables" option show_consts : bool = false -- "show constants with types when printing proof state" option show_main_goal : bool = false -- "show main goal when printing proof state" option goals_limit : int = 10 -- "maximum number of subgoals to be printed" option show_states : bool = false -- "show toplevel states even if outside of interactive mode" option names_long : bool = false -- "show fully qualified names" option names_short : bool = false -- "show base names only" option names_unique : bool = true -- "show partially qualified names, as required for unique name resolution" option eta_contract : bool = true -- "print terms in eta-contracted form" option print_mode : string = "" -- "additional print modes for prover output (separated by commas)" section "Parallel Processing and Timing" public option threads : int = 0 -- "maximum number of worker threads for prover process (0 = hardware max.)" option threads_trace : int = 0 -- "level of tracing information for multithreading" option threads_stack_limit : real = 0.25 -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" public option parallel_limit : int = 0 -- "approximative limit for parallel tasks (0 = unlimited)" public option parallel_print : bool = true -- "parallel and asynchronous printing of results" public option parallel_proofs : int = 1 -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" public option timeout_scale : real = 1.0 -- "scale factor for timeout in Isabelle/ML and session build" section "Detail of Proof Checking" option record_proofs : int = -1 -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" option quick_and_dirty : bool = false -- "if true then some tools will OMIT some proofs" option skip_proofs : bool = false -- "skip over proofs (implicit 'sorry')" option strict_facts : bool = false -- "force lazy facts when defined in context" section "Global Session Parameters" option condition : string = "" -- "required environment variables for subsequent theories (separated by commas)" option timeout : real = 0 -- "timeout for session build job (seconds > 0)" option timeout_build : bool = true -- "observe timeout for session build" option process_output_limit : int = 100 -- "build process output limit (in million characters, 0 = unlimited)" option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" option profiling : string = "" (standard "time") -- "ML profiling (possible values: time, time_thread, allocations)" option system_log : string = "" (standard "-") -- "output for system messages (log file or \"-\" for console progress)" option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" section "ML System" option ML_print_depth : int = 20 -- "ML print depth for toplevel pretty-printing" public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" public option ML_exception_debugger : bool = false -- "ML debugger exception trace for toplevel command execution" public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code" public option ML_system_64 : bool = false -- "ML system for 64bit platform is used if possible (change requires restart)" public option ML_process_policy : string = "" -- "ML process command prefix (process policy)" section "PIDE Build" option pide_reports : bool = true -- "report PIDE markup" option build_pide_reports : bool = true -- "report PIDE markup in batch build" section "Editor Session" public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" public option editor_input_delay : real = 0.2 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 -- "delay for machine-generated input that may outperform user edits" public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" public option editor_consolidate_delay : real = 2.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" option editor_prune_size : int = 0 -- "retained size of pruned history (delete old versions)" public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" public option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" public option editor_continuous_checking : bool = true -- "continuous checking of proof document (visible and required parts)" public option editor_output_state : bool = false -- "implicit output of proof state" option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" public option editor_presentation : bool = false -- "dynamic presentation while editing" section "Headless Session" option headless_consolidate_delay : real = 15 -- "delay to consolidate status of command evaluation (execution forks)" option headless_prune_delay : real = 60 -- "delay to prune history (delete old versions)" option headless_check_delay : real = 0.5 -- "delay for theory status check during PIDE processing (seconds)" option headless_check_limit : int = 0 -- "maximum number of theory status checks (0 = unlimited)" option headless_nodes_status_delay : real = -1 -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" option headless_watchdog_timeout : real = 600 -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" option headless_commit_cleanup_delay : real = 60 -- "delay for cleanup of already imported theories (seconds, 0 = disabled)" option headless_load_limit : real = 5.0 -- "limit in MB for loaded theory files (0 = unlimited)" section "Miscellaneous Tools" public option find_theorems_limit : int = 40 -- "limit of displayed results" public option find_theorems_tactic_limit : int = 5 -- "limit of tactic search for 'solves' criterion" section "Completion" public option completion_limit : int = 40 -- "limit for completion within the formal context" public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker" public option spell_checker : bool = true -- "enable spell-checker for prose words within document text, comments etc." public option spell_checker_dictionary : string = "en" -- "spell-checker dictionary name" public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" -- "included markup elements for spell-checker (separated by commas)" public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" -- "excluded markup elements for spell-checker (separated by commas)" section "Secure Shell" +option ssh_multiplexing : bool = true + -- "enable multiplexing of SSH sessions (ignored on Windows)" + option ssh_compression : bool = true -- "enable SSH compression" option ssh_connect_timeout : real = 60 -- "SSH connection timeout (seconds)" option ssh_alive_interval : real = 30 -- "time interval to keep SSH server connection alive (seconds)" option ssh_alive_count_max : int = 3 -- "maximum number of messages to keep SSH server connection alive" section "Phabricator" option phabricator_version_arcanist : string = "4f70fcffa8a5393e210d64f237ffdaa256256d6a" -- "repository version for arcanist" option phabricator_version_phabricator : string = "193798385bd3a7f72dca255e44f8112f4f8fc155" -- "repository version for phabricator" section "Theory Export" option export_theory : bool = false -- "export theory content to Isabelle/Scala" option export_standard_proofs : bool = false -- "export standardized proof terms to Isabelle/Scala (not scalable)" option export_proofs : bool = false -- "export proof terms to Isabelle/Scala" option prune_proofs : bool = false -- "prune proof terms after export (do not store in Isabelle/ML)" section "Theory update" option update_inner_syntax_cartouches : bool = false -- "update inner syntax (types, terms, etc.) to use cartouches" option update_mixfix_cartouches : bool = false -- "update mixfix templates to use cartouches instead of double quotes" option update_control_cartouches : bool = false -- "update antiquotations to use control symbol with cartouche argument" option update_path_cartouches : bool = false -- "update file-system paths to use cartouches" section "Build Database" option build_database_server : bool = false option build_database_user : string = "" option build_database_password : string = "" option build_database_name : string = "" option build_database_host : string = "" option build_database_port : int = 0 option build_database_ssh_host : string = "" option build_database_ssh_user : string = "" option build_database_ssh_port : int = 0 section "Build Log Database" option build_log_database_user : string = "" option build_log_database_password : string = "" option build_log_database_name : string = "" option build_log_database_host : string = "" option build_log_database_port : int = 0 option build_log_ssh_host : string = "" option build_log_ssh_user : string = "" option build_log_ssh_port : int = 0 option build_log_history : int = 30 -- "length of relevant history (in days)" option build_log_transaction_size : int = 1 -- "number of log files for each db update" section "Isabelle/Scala/ML system channel" option system_channel_address : string = "" option system_channel_password : string = "" section "Bash process execution server" option bash_process_debugging : bool = false option bash_process_address : string = "" option bash_process_password : string = "" 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,326 +1,357 @@ /* 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.net.ServerSocket object SSH { /* target machine: user@host syntax */ object Target { def parse(s: String): (String, String) = { val i = s.indexOf('@') if (i <= 0) ("", s) else (s.substring(0, i), s.substring(i + 1)) } def unapplySeq(s: String): Option[List[String]] = { val (user, host) = parse(s) if (host.isEmpty) None else Some(List(user, host)) } } /* 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 make(options: Options, port: Int = 0, 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) 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 make_command(command: String, config: List[String]): String = - Bash.string(command) + " " + config.map(entry => "-o " + Bash.string(entry)).mkString(" ") + 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: 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 = Set(' ', '*', '?', '{', '}') - if (str.exists(special)) { + val special = "[]?*\\{} \"'" + if (str.isEmpty) "\"\"" + else if (str.exists(special.contains)) { val res = new StringBuilder for (c <- str) { - if (special(c)) res += '\\' + 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 = "", - multiplex: Boolean = !Platform.is_windows + user: String = "" ): Session = { + val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows val (control_master, control_path) = - if (multiplex) { - val file = Isabelle_System.tmp_file("ssh_socket") - file.delete() - (true, file.getPath) - } + if (multiplex) (true, Isabelle_System.tmp_file("ssh_socket", 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 + ":" - /* ssh commands */ + /* local ssh commands */ 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 = { val config = Config.make(options, port = port, user = user, control_master = master, control_path = control_path) val cmd = - Config.make_command(command, config) + + Config.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) } 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) } } 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) } 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 user_home: String = { + val args = Bash.string("printenv HOME\nprintenv SHELL") + run_ssh(master = control_master, args = args).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) + " export " + Bash.string("USER_HOME=\"$HOME\"") + "\n" + cmd_line + 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 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)).check 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 } 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 = 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 = run_scp(args = File.bash_platform_path(local_path) + " " + Bash.string(host + ":" + remote_path(path))).check 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) } def write(path: Path, text: String): Unit = write_bytes(path, Bytes(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 -t tmp.XXXXXXXXXX").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 = { - if (control_path.isEmpty) error("SSH port forwarding requires multiplexing") + val port = if (local_port > 0) local_port else Isabelle_System.local_port() - val port = - if (local_port > 0) 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 { - // FIXME race condition - val dummy = new ServerSocket(0) - val port = dummy.getLocalPort - dummy.close() - port + 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 string = List(local_host, port, remote_host, remote_port).mkString(":") - run_ssh(opts = "-L " + Bash.string(string) + " -O forward").check + + val shutdown_hook = + Isabelle_System.create_shutdown_hook { cancel() } new Port_Forwarding(host, port, remote_host, remote_port) { - override def toString: String = string + override def toString: String = forward override def close(): Unit = { - run_ssh(opts = "-L " + Bash.string(string) + " -O cancel").check + 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 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 isabelle_platform: Isabelle_Platform = Isabelle_Platform() } object Local extends System } diff --git a/src/Pure/System/bash.scala b/src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala +++ b/src/Pure/System/bash.scala @@ -1,379 +1,373 @@ /* Title: Pure/System/bash.scala Author: Makarius Support for GNU bash: portable external processes with propagation of interrupts. */ package isabelle import java.util.{List => JList, Map => JMap} import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile, IOException} import scala.annotation.tailrec import scala.jdk.OptionConverters._ object Bash { /* concrete syntax */ private def bash_chr(c: Byte): String = { val ch = c.toChar ch match { case '\t' => "$'\\t'" case '\n' => "$'\\n'" case '\f' => "$'\\f'" case '\r' => "$'\\r'" case _ => if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch)) Symbol.ascii(ch) else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" else "\\" + ch } } def string(s: String): String = if (s == "") "\"\"" else UTF8.bytes(s).iterator.map(bash_chr).mkString def strings(ss: List[String]): String = ss.iterator.map(Bash.string).mkString(" ") /* process and result */ private def make_description(description: String): String = proper_string(description) getOrElse "bash_process" type Watchdog = (Time, Process => Boolean) def process(script: String, description: String = "", cwd: JFile = null, env: JMap[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => ()): Process = new Process(script, description, cwd, env, redirect, cleanup) class Process private[Bash]( script: String, description: String, cwd: JFile, env: JMap[String, String], redirect: Boolean, cleanup: () => Unit ) { override def toString: String = make_description(description) private val timing_file = Isabelle_System.tmp_file("bash_timing") private val timing = Synchronized[Option[Timing]](None) def get_timing: Timing = timing.value getOrElse Timing.zero private val winpid_file: Option[JFile] = if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None private val winpid_script = winpid_file match { case None => script case Some(file) => "read < /proc/self/winpid > /dev/null 2> /dev/null\n" + """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script } private val script_file: JFile = Isabelle_System.tmp_file("bash_script") File.write(script_file, winpid_script) private val proc = isabelle.setup.Environment.process_builder( JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), File.standard_path(timing_file), "bash", File.standard_path(script_file)), cwd, env, redirect).start() // channels val stdin: BufferedWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) val stdout: BufferedReader = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) val stderr: BufferedReader = new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) // signals private val group_pid = stdout.readLine private def process_alive(pid: String): Boolean = (for { p <- Value.Long.unapply(pid) handle <- ProcessHandle.of(p).toScala } yield handle.isAlive) getOrElse false private def root_process_alive(): Boolean = winpid_file match { case None => process_alive(group_pid) case Some(file) => file.exists() && process_alive(Library.trim_line(File.read(file))) } @tailrec private def signal(s: String, count: Int = 1): Boolean = { count <= 0 || { isabelle.setup.Environment.kill_process(group_pid, s) val running = root_process_alive() || isabelle.setup.Environment.kill_process(group_pid, "0") if (running) { Time.seconds(0.1).sleep() signal(s, count - 1) } else false } } def terminate(): Unit = Isabelle_Thread.try_uninterruptible { signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL") proc.destroy() do_cleanup() } def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { isabelle.setup.Environment.kill_process(group_pid, "INT") } - // JVM shutdown hook - - private val shutdown_hook = Isabelle_Thread.create(() => terminate()) - - try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } - catch { case _: IllegalStateException => } - - // cleanup + private val shutdown_hook = + Isabelle_System.create_shutdown_hook { terminate() } + private def do_cleanup(): Unit = { - try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } - catch { case _: IllegalStateException => } + Isabelle_System.remove_shutdown_hook(shutdown_hook) script_file.delete() winpid_file.foreach(_.delete()) timing.change { case None => if (timing_file.isFile) { val t = Word.explode(File.read(timing_file)) match { case List(Value.Long(elapsed), Value.Long(cpu)) => Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) case _ => Timing.zero } timing_file.delete Some(t) } else Some(Timing.zero) case some => some } cleanup() } // join def join(): Int = { val rc = proc.waitFor() do_cleanup() rc } // result def result( input: String = "", progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Watchdog] = None, strict: Boolean = true ): Process_Result = { val in = if (input.isEmpty) Future.value(stdin.close()) else Future.thread("bash_stdin") { stdin.write(input); stdin.flush(); stdin.close(); } val out_lines = Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } val err_lines = Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } val watchdog_thread = for ((time, check) <- watchdog) yield { Future.thread("bash_watchdog") { while (proc.isAlive) { time.sleep() if (check(this)) interrupt() } } } val rc = try { join() } catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt } watchdog_thread.foreach(_.cancel()) in.join out_lines.join err_lines.join if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt() Process_Result(rc, out_lines.join, err_lines.join, get_timing) } } /* server */ object Server { // input messages private val RUN = "run" private val KILL = "kill" // output messages private val UUID = "uuid" private val INTERRUPT = "interrupt" private val FAILURE = "failure" private val RESULT = "result" def start(port: Int = 0, debugging: => Boolean = false): Server = { val server = new Server(port, debugging) server.start() server } } class Server private(port: Int, debugging: => Boolean) extends isabelle.Server.Handler(port) { server => private val _processes = Synchronized(Map.empty[UUID.T, Bash.Process]) override def stop(): Unit = { for ((_, process) <- _processes.value) process.terminate() super.stop() } override def handle(connection: isabelle.Server.Connection): Unit = { def reply(chunks: List[String]): Unit = try { connection.write_byte_message(chunks.map(Bytes.apply)) } catch { case _: IOException => } def reply_failure(exn: Throwable): Unit = reply( if (Exn.is_interrupt(exn)) List(Server.INTERRUPT) else List(Server.FAILURE, Exn.message(exn))) def reply_result(result: Process_Result): Unit = reply( Server.RESULT :: result.rc.toString :: result.timing.elapsed.ms.toString :: result.timing.cpu.ms.toString :: result.out_lines.length.toString :: result.out_lines ::: result.err_lines) connection.read_byte_message().map(_.map(_.text)) match { case None => case Some(List(Server.KILL, UUID(uuid))) => if (debugging) Output.writeln("kill " + uuid) _processes.value.get(uuid).foreach(_.terminate()) case Some(List(Server.RUN, script, input, cwd, putenv, Value.Boolean(redirect), Value.Seconds(timeout), description)) => val uuid = UUID.random() val descr = make_description(description) if (debugging) { Output.writeln( "start " + quote(descr) + " (uuid=" + uuid + ", timeout=" + timeout.seconds + ")") } Exn.capture { Bash.process(script, description = description, cwd = XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match { case None => null case Some(s) => Path.explode(s).file }, env = Isabelle_System.settings( XML.Decode.list(XML.Decode.pair(XML.Decode.string, XML.Decode.string))( YXML.parse_body(putenv))), redirect= redirect) } match { case Exn.Exn(exn) => reply_failure(exn) case Exn.Res(process) => _processes.change(processes => processes + (uuid -> process)) reply(List(Server.UUID, uuid.toString)) Isabelle_Thread.fork(name = "bash_process") { @volatile var is_timeout = false val watchdog: Option[Watchdog] = if (timeout.is_zero) None else Some((timeout, _ => { is_timeout = true; true })) Exn.capture { process.result(input = input, watchdog = watchdog, strict = false) } match { case Exn.Exn(exn) => reply_failure(exn) case Exn.Res(res0) => val res = if (!res0.ok && is_timeout) res0.timeout_rc else res0 if (debugging) { Output.writeln( "stop " + quote(descr) + " (uuid=" + uuid + ", return_code=" + res.rc + ")") } reply_result(res) } _processes.change(provers => provers - uuid) } connection.await_close() } case Some(_) => reply_failure(ERROR("Bad protocol message")) } } } class Handler extends Session.Protocol_Handler { private var server: Server = null override def init(session: Session): Unit = { exit() server = Server.start(debugging = session.session_options.bool("bash_process_debugging")) } override def exit(): Unit = { if (server != null) { server.stop() server = null } } override def prover_options(options: Options): Options = { val address = if (server == null) "" else server.address val password = if (server == null) "" else server.password options + ("bash_process_address=" + address) + ("bash_process_password=" + password) } } } diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,476 +1,508 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Miscellaneous Isabelle system operations. */ package isabelle import java.util.{Map => JMap, HashMap} import java.io.{File => JFile, IOException} +import java.net.ServerSocket import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes object Isabelle_System { /* settings environment */ def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = { val env0 = isabelle.setup.Environment.settings() if (putenv.isEmpty) env0 else { val env = new HashMap(env0) for ((a, b) <- putenv) env.put(a, b) env } } def getenv(name: String, env: JMap[String, String] = settings()): String = Option(env.get(name)).getOrElse("") def getenv_strict(name: String, env: JMap[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) /* services */ type Service = Classpath.Service @volatile private var _classpath: Option[Classpath] = None def classpath(): Classpath = { if (_classpath.isEmpty) init() // unsynchronized check _classpath.get } def make_services[C](c: Class[C]): List[C] = classpath().make_services(c) /* init settings + classpath */ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = { isabelle.setup.Environment.init(isabelle_root, cygwin_root) synchronized { if (_classpath.isEmpty) _classpath = Some(Classpath()) } } /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse Mercurial.id_repository(root, rev = "") getOrElse error("Failed to identify Isabelle distribution " + root.expand) object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def export_isabelle_identifier(isabelle_identifier: String): String = "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths( args: List[String], fun: PartialFunction[List[Path], Unit] ): List[String] = { fun(args.map(Path.explode)) Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.java_path) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute) else { try { copy_dir(dir1, dir2); body } finally { rm_tree(dir2 ) } } } object Make_Directory extends Scala.Fun_Strings("make_directory") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, make_directory) } object Copy_Dir extends Scala.Fun_Strings("copy_dir") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed to copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun_Strings("copy_file") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_file) } object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete def cygwin_link(): Unit = { if (native) { error("Failed to create native symlink on Windows: " + quote(src_file.toString) + "\n(but it could work as Administrator)") } else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target) } try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => cygwin_link() case _: FileSystemException if Platform.is_windows => cygwin_link() } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } - def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { + def tmp_file( + name: String, + ext: String = "", + base_dir: JFile = isabelle_tmp_prefix(), + initialized: Boolean = true + ): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile - file.deleteOnExit() + if (initialized) file.deleteOnExit() else file.delete() file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun_Strings("rm_tree") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit() dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } + /* TCP/IP ports */ + + def local_port(): Int = { + val socket = new ServerSocket(0) + val port = socket.getLocalPort + socket.close() + port + } + + + /* JVM shutdown hook */ + + def create_shutdown_hook(body: => Unit): Thread = { + val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body }) + + try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } + catch { case _: IllegalStateException => } + + shutdown_hook + } + + def remove_shutdown_hook(shutdown_hook: Thread): Unit = + try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } + catch { case _: IllegalStateException => } + + /** external processes **/ /* GNU bash */ def bash(script: String, description: String = "", cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false, input: String = "", progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => () ): Process_Result = { Bash.process(script, description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } /* command-line tools */ def require_command(cmd: String, test: String = "--version"): Unit = { if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd)) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, strip: Int = 0, redirect: Boolean = false ): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") + (if (strip <= 0) "" else "--strip-components=" + strip + " ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash( "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(patch), cwd = base_dir.file).check_rc(_ <= 1) File.read(patch) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, progress: Progress = new Progress): HTTP.Content = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } } def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Bytes.write(file, download(url_name, progress = progress).bytes) object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here override def invoke(args: List[Bytes]): List[Bytes] = args.map(url => download(url.text).bytes) } /* repositories */ val isabelle_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/isabelle") val afp_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel") def official_releases(): List[String] = Library.trim_split_lines( isabelle_repository.read_file(Path.explode("Admin/Release/official"))) }