provide bash_process server for Isabelle/ML and other external programs;
authorwenzelm
Thu, 12 Aug 2021 14:18:46 +0200
changeset 74417 d030b988d470
parent 74416 dd1639961016
child 74418 a97d5356f1d9
provide bash_process server for Isabelle/ML and other external programs; clarified signature for Bash.params;
etc/build.props
etc/options
src/HOL/Tools/Nunchaku/nunchaku_tool.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/Pure/System/bash.ML
src/Pure/System/bash.scala
src/Pure/System/isabelle_system.ML
src/Pure/System/scala.scala
src/Pure/Tools/generated_files.ML
src/Pure/Tools/ghc.ML
src/Pure/Tools/jedit.ML
--- 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