# HG changeset patch # User wenzelm # Date 1628770726 -7200 # Node ID d030b988d470061e400b8e4ed78ea337281e7001 # Parent dd1639961016102d9270e7e6529b6a33709207f8 provide bash_process server for Isabelle/ML and other external programs; clarified signature for Bash.params; diff -r dd1639961016 -r d030b988d470 etc/build.props --- a/etc/build.props Thu Aug 12 13:55:45 2021 +0200 +++ b/etc/build.props Thu Aug 12 14:18:46 2021 +0200 @@ -274,6 +274,7 @@ src/Tools/jEdit/src/timing_dockable.scala \ src/Tools/jEdit/src/token_markup.scala services = \ + isabelle.Bash$Handler \ isabelle.Bibtex$File_Format \ isabelle.Document_Build$Build_Engine \ isabelle.Document_Build$LuaLaTeX_Engine \ diff -r dd1639961016 -r d030b988d470 etc/options --- a/etc/options Thu Aug 12 13:55:45 2021 +0200 +++ b/etc/options Thu Aug 12 14:18:46 2021 +0200 @@ -373,3 +373,10 @@ 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 -r dd1639961016 -r d030b988d470 src/HOL/Tools/Nunchaku/nunchaku_tool.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Thu Aug 12 14:18:46 2021 +0200 @@ -103,7 +103,7 @@ [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()]; val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem; val _ = File.write prob_path prob_str; - val res = Isabelle_System.bash_process_script bash_cmd; + val res = Isabelle_System.bash_process (Bash.script bash_cmd); val rc = Process_Result.rc res; val out = Process_Result.out res; val err = Process_Result.err res; diff -r dd1639961016 -r d030b988d470 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 12 14:18:46 2021 +0200 @@ -818,7 +818,7 @@ if getenv env_var = "" then (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "") else - let val res = Isabelle_System.bash_process_script (cmd ^ File.bash_path file) in + let val res = Isabelle_System.bash_process (Bash.script (cmd ^ File.bash_path file)) in res |> Process_Result.check |> Process_Result.out handle ERROR msg => cat_error ("Error caused by prolog system " ^ env_var ^ diff -r dd1639961016 -r d030b988d470 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 12 14:18:46 2021 +0200 @@ -262,7 +262,7 @@ (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ " -o " ^ File.bash_platform_path executable ^ ";" val compilation_time = - Isabelle_System.bash_process_script cmd + Isabelle_System.bash_process (Bash.script cmd) |> Process_Result.check |> Process_Result.timing_elapsed |> Time.toMilliseconds handle ERROR msg => cat_error "Compilation with GHC failed" msg @@ -275,9 +275,9 @@ val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k val res = - Isabelle_System.bash_process_script + Isabelle_System.bash_process (Bash.script (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ - string_of_int k) + string_of_int k)) |> Process_Result.check val response = Process_Result.out res val timing = res |> Process_Result.timing_elapsed |> Time.toMilliseconds; diff -r dd1639961016 -r d030b988d470 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Aug 12 14:18:46 2021 +0200 @@ -271,10 +271,7 @@ let val {output, timing} = SystemOnTPTP.run_system_encoded args in (output, timing) end else - let - val res = - Isabelle_System.bash_process - {script = command, input = "", redirect = true, timeout = Time.zeroTime} + let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) in (Process_Result.out res, Process_Result.timing_elapsed res) end val _ = diff -r dd1639961016 -r d030b988d470 src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/System/bash.ML Thu Aug 12 14:18:46 2021 +0200 @@ -8,11 +8,24 @@ sig val string: string -> string val strings: string list -> string + type params + val dest_params: params -> + {script: string, input: string, cwd: Path.T option, putenv: (string * string) list, + redirect: bool, timeout: Time.time, description: string} + val script: string -> params + val input: string -> params -> params + val cwd: Path.T -> params -> params + val putenv: (string * string) list -> params -> params + val redirect: params -> params + val timeout: Time.time -> params -> params + val description: string -> params -> params end; structure Bash: BASH = struct +(* concrete syntax *) + fun string "" = "\"\"" | string str = str |> translate_string (fn ch => @@ -32,4 +45,50 @@ val strings = space_implode " " o map string; + +(* server parameters *) + +abstype params = + Params of + {script: string, input: string, cwd: Path.T option, putenv: (string * string) list, + redirect: bool, timeout: Time.time, description: string} +with + +fun dest_params (Params args) = args; + +fun make_params (script, input, cwd, putenv, redirect, timeout, description) = + Params {script = script, input = input, cwd = cwd, putenv = putenv, redirect = redirect, + timeout = timeout, description = description}; + +fun map_params f (Params {script, input, cwd, putenv, redirect, timeout, description}) = + make_params (f (script, input, cwd, putenv, redirect, timeout, description)); + +fun script script = make_params (script, "", NONE, [], false, Time.zeroTime, ""); + +fun input input = + map_params (fn (script, _, cwd, putenv, redirect, timeout, description) => + (script, input, cwd, putenv, redirect, timeout, description)); + +fun cwd cwd = + map_params (fn (script, input, _, putenv, redirect, timeout, description) => + (script, input, SOME cwd, putenv, redirect, timeout, description)); + +fun putenv putenv = + map_params (fn (script, input, cwd, _, redirect, timeout, description) => + (script, input, cwd, putenv, redirect, timeout, description)); + +val redirect = + map_params (fn (script, input, cwd, putenv, _, timeout, description) => + (script, input, cwd, putenv, true, timeout, description)); + +fun timeout timeout = + map_params (fn (script, input, cwd, putenv, redirect, _, description) => + (script, input, cwd, putenv, redirect, timeout, description)); + +fun description description = + map_params (fn (script, input, cwd, putenv, redirect, timeout, _) => + (script, input, cwd, putenv, redirect, timeout, description)); + end; + +end; diff -r dd1639961016 -r d030b988d470 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/System/bash.scala Thu Aug 12 14:18:46 2021 +0200 @@ -236,44 +236,150 @@ } - /* Scala function */ + /* 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" - object Process extends Scala.Fun_Strings("bash_process", thread = true) + 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) { - val here = Scala_Project.here - def apply(args: List[String]): List[String] = + server => + + private val _processes = Synchronized(Map.empty[UUID.T, Bash.Process]) + + override def stop(): Unit = { - @volatile var is_timeout = false - val result = - Exn.capture { - args match { - case List(script, input, Value.Boolean(redirect), Value.Int(timeout)) => - Isabelle_System.bash(script, input = input, redirect = redirect, - watchdog = - if (timeout == 0) None - else Some((Time.ms(timeout), _ => { is_timeout = true; true })), - strict = false) - case _ => error("Bad number of args: " + args.length) + for ((_, process) <- _processes.value) process.terminate() + super.stop() + } + + override def handle(connection: isabelle.Server.Connection): Unit = + { + def reply(chunks: List[String]): Unit = + connection.write_byte_message(chunks.map(Bytes.apply)) + + 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 = proper_string(description) getOrElse "bash_process" + if (debugging) { + Output.writeln( + "start " + quote(descr) + " (uuid=" + uuid + ", timeout=" + timeout.seconds + ")") } - } - val is_interrupt = - result match { - case Exn.Res(res) => res.rc == Process_Result.interrupt_rc && !is_timeout - case Exn.Exn(exn) => Exn.is_interrupt(exn) - } + Exn.capture { + Bash.process(script, + 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)) - result match { - case _ if is_interrupt => Nil - case Exn.Exn(exn) => List(Exn.message(exn)) - case Exn.Res(res) => - val rc = if (!res.ok && is_timeout) Process_Result.timeout_rc else res.rc - rc.toString :: - res.timing.elapsed.ms.toString :: - res.timing.cpu.ms.toString :: - res.out_lines.length.toString :: - res.out_lines ::: res.err_lines + 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 -r dd1639961016 -r d030b988d470 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/System/isabelle_system.ML Thu Aug 12 14:18:46 2021 +0200 @@ -6,9 +6,7 @@ signature ISABELLE_SYSTEM = sig - val bash_process: - {script: string, input: string, redirect: bool, timeout: Time.time} -> Process_Result.T - val bash_process_script: string -> Process_Result.T + val bash_process: Bash.params -> Process_Result.T val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list @@ -38,38 +36,61 @@ (* bash *) -fun bash_process {script, input, redirect, timeout} = - Scala.function "bash_process" - ["export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script, - input, Value.print_bool redirect, Value.print_int (Time.toMilliseconds timeout)] - |> (fn [] => raise Exn.Interrupt - | [err] => error err - | a :: b :: c :: d :: lines => - let - val rc = Value.parse_int a; - val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); - val (out_lines, err_lines) = chop (Value.parse_int d) lines; - in - if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed else (); - Process_Result.make - {rc = rc, - out_lines = out_lines, - err_lines = err_lines, - timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} - end - | _ => raise Fail "Malformed Isabelle/Scala result"); +val absolute_path = Path.implode o File.absolute_path; + +fun bash_process params = + let + val {script, input, cwd, putenv, redirect, timeout, description: string} = + Bash.dest_params params; + val run = + ["run", script, input, + let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end, + let open XML.Encode in YXML.string_of_body o list (pair string string) end + (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv), + Value.print_bool redirect, + Value.print_real (Time.toReal timeout), + description]; + + val address = Options.default_string \<^system_option>\bash_process_address\; + val password = Options.default_string \<^system_option>\bash_process_password\; + + val _ = address = "" andalso raise Fail "Bad bash_process server address"; + fun with_streams f = Socket_IO.with_streams' f address password; -fun bash_process_script script = - bash_process {script = script, input = "", redirect = false, timeout = Time.zeroTime}; + fun kill (SOME uuid) = with_streams (fn s => Byte_Message.write_message (#2 s) ["kill", uuid]) + | kill NONE = (); + in + Thread_Attributes.uninterruptible (fn restore_attributes => fn () => + let + fun loop maybe_uuid streams = + (case restore_attributes Byte_Message.read_message (#1 streams) of + SOME ["uuid", uuid] => loop (SOME uuid) streams + | SOME ["interrupt"] => raise Exn.Interrupt + | SOME ["failure", msg] => raise Fail msg + | SOME ("result" :: a :: b :: c :: d :: lines) => + let + val rc = Value.parse_int a; + val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); + val (out_lines, err_lines) = chop (Value.parse_int d) lines; + in + if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed + else + Process_Result.make + {rc = rc, + out_lines = out_lines, + err_lines = err_lines, + timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} + end + | _ => raise Fail "Malformed bash_process server result") + handle exn => (kill maybe_uuid; Exn.reraise exn); + in with_streams (fn s => (Byte_Message.write_message (#2 s) run; loop NONE s)) end) () + end; -fun bash script = - bash_process_script script - |> Process_Result.print - |> Process_Result.rc; +val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let - val res = bash_process_script s; + val res = bash_process (Bash.script s); val _ = warning (Process_Result.err res); in (Process_Result.out res, Process_Result.rc res) end; @@ -77,7 +98,7 @@ (* bash functions *) fun bash_functions () = - bash_process_script "declare -Fx" + bash_process (Bash.script "declare -Fx") |> Process_Result.check |> Process_Result.out_lines |> map_filter (space_explode " " #> try List.last); @@ -89,7 +110,6 @@ (* directory and file operations *) -val absolute_path = Path.implode o File.absolute_path; fun scala_function name = ignore o Scala.function name o map absolute_path; fun make_directory path = (scala_function "make_directory" [path]; path); diff -r dd1639961016 -r d030b988d470 src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/System/scala.scala Thu Aug 12 14:18:46 2021 +0200 @@ -270,7 +270,6 @@ Bytes.Decode_Base64, Bytes.Encode_Base64, Doc.Doc_Names, - Bash.Process, Bibtex.Check_Database, Isabelle_System.Make_Directory, Isabelle_System.Copy_Dir, diff -r dd1639961016 -r d030b988d470 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/Tools/generated_files.ML Thu Aug 12 14:18:46 2021 +0200 @@ -332,7 +332,7 @@ (* execute compiler -- auxiliary *) fun execute dir title compile = - Isabelle_System.bash_process_script ("cd " ^ File.bash_path dir ^ " && " ^ compile) + Isabelle_System.bash_process (Bash.script compile |> Bash.cwd dir) |> Process_Result.check |> Process_Result.out handle ERROR msg => diff -r dd1639961016 -r d030b988d470 src/Pure/Tools/ghc.ML --- a/src/Pure/Tools/ghc.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/Tools/ghc.ML Thu Aug 12 14:18:46 2021 +0200 @@ -84,9 +84,9 @@ val template_path = dir + (Path.basic name |> Path.ext "hsfiles"); val _ = File.write template_path (project_template {depends = depends, modules = modules}); val _ = - Isabelle_System.bash_process_script - ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ - " --bare " ^ File.bash_platform_path template_path) + Isabelle_System.bash_process + (Bash.script ("isabelle ghc_stack new " ^ Bash.string name ^ + " --bare " ^ File.bash_platform_path template_path) |> Bash.cwd dir) |> Process_Result.check; in () end; diff -r dd1639961016 -r d030b988d470 src/Pure/Tools/jedit.ML --- a/src/Pure/Tools/jedit.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/Tools/jedit.ML Thu Aug 12 14:18:46 2021 +0200 @@ -36,7 +36,8 @@ fun xml_resource name = let - val res = Isabelle_System.bash_process_script ("unzip -p \"$JEDIT_JAR\" " ^ Bash.string name); + val res = + Isabelle_System.bash_process (Bash.script ("unzip -p \"$JEDIT_JAR\" " ^ Bash.string name)); val rc = Process_Result.rc res; in res |> Process_Result.check |> Process_Result.out |> XML.parse