provide bash_process server for Isabelle/ML and other external programs;
clarified signature for Bash.params;
--- 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 \
--- 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 = ""
--- 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;
--- 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 ^
--- 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;
--- 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 _ =
--- 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;
--- 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)
+ }
+ }
}
--- 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>\<open>bash_process_address\<close>;
+ val password = Options.default_string \<^system_option>\<open>bash_process_password\<close>;
+
+ 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);
--- 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,
--- 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 =>
--- 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;
--- 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