# HG changeset patch
# User wenzelm
# Date 1628367817 -7200
# Node ID 0f051404f487cf5e826548f4f5d35ddcf40c325e
# Parent  bba35ad317abeb39a429244f01f2399efe7a6e7c
clarified signature: more options for bash_process;

diff -r bba35ad317ab -r 0f051404f487 src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Sat Aug 07 22:23:37 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 bash_cmd;
+        val res = Isabelle_System.bash_process_script bash_cmd;
         val rc = Process_Result.rc res;
         val out = Process_Result.out res;
         val err = Process_Result.err res;
diff -r bba35ad317ab -r 0f051404f487 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 07 22:23:37 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 (cmd ^ File.bash_path file) in
+      let val res = Isabelle_System.bash_process_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 bba35ad317ab -r 0f051404f487 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Aug 07 22:23:37 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 cmd
+          Isabelle_System.bash_process_script cmd
           |> Process_Result.check
           |> Process_Result.timing_elapsed |> Time.toMilliseconds
           handle ERROR msg => cat_error "Compilation with GHC failed" msg
@@ -275,7 +275,7 @@
               val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
               val _ = current_size := k
               val res =
-                Isabelle_System.bash_process
+                Isabelle_System.bash_process_script
                   (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^
                     string_of_int k)
                 |> Process_Result.check
diff -r bba35ad317ab -r 0f051404f487 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Aug 07 22:23:37 2021 +0200
@@ -271,7 +271,10 @@
                 let val {output, timing} = SystemOnTPTP.run_system_encoded args
                 in (output, timing) end
               else
-                let val res = Isabelle_System.bash_process_redirect command
+                let
+                  val res =
+                    Isabelle_System.bash_process
+                      {script = command, input = "", redirect = true, timeout = Time.zeroTime}
                 in (Process_Result.out res, Process_Result.timing_elapsed res) end
 
             val _ =
diff -r bba35ad317ab -r 0f051404f487 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/Pure/System/bash.scala	Sat Aug 07 22:23:37 2021 +0200
@@ -194,13 +194,15 @@
     // result
 
     def result(
+      input: String = "",
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
       watchdog: Option[Watchdog] = None,
       strict: Boolean = true): Process_Result =
     {
-      stdin.close()
-
+      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 =
@@ -223,6 +225,10 @@
 
       watchdog_thread.foreach(_.cancel())
 
+      in.join
+      out_lines.join
+      err_lines.join
+
       if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join, get_timing)
@@ -237,16 +243,23 @@
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] =
     {
+      @volatile var is_timeout = false
       val result =
         Exn.capture {
-          val redirect = args.head == "true"
-          val script = cat_lines(args.tail)
-          Isabelle_System.bash(script, redirect = redirect)
+          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)
+          }
         }
 
       val is_interrupt =
         result match {
-          case Exn.Res(res) => res.rc == Process_Result.interrupt_rc
+          case Exn.Res(res) => res.rc == Process_Result.interrupt_rc && !is_timeout
           case Exn.Exn(exn) => Exn.is_interrupt(exn)
         }
 
@@ -254,7 +267,8 @@
         case _ if is_interrupt => Nil
         case Exn.Exn(exn) => List(Exn.message(exn))
         case Exn.Res(res) =>
-          res.rc.toString ::
+          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 ::
diff -r bba35ad317ab -r 0f051404f487 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sat Aug 07 22:23:37 2021 +0200
@@ -6,8 +6,9 @@
 
 signature ISABELLE_SYSTEM =
 sig
-  val bash_process: string -> Process_Result.T
-  val bash_process_redirect: string -> Process_Result.T
+  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_output: string -> string * int
   val bash: string -> int
   val bash_functions: unit -> string list
@@ -37,9 +38,10 @@
 
 (* bash *)
 
-fun invoke_bash_process redirect script =
+fun bash_process {script, input, redirect, timeout} =
   Scala.function "bash_process"
-    [Value.print_bool redirect, "export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
+   ["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 =>
@@ -48,6 +50,7 @@
             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,
@@ -56,14 +59,17 @@
          end
       | _ => raise Fail "Malformed Isabelle/Scala result");
 
-val bash_process = invoke_bash_process false;
-val bash_process_redirect = invoke_bash_process true;
+fun bash_process_script script =
+  bash_process {script = script, input = "", redirect = false, timeout = Time.zeroTime};
 
-val bash = bash_process #> Process_Result.print #> Process_Result.rc;
+fun bash script =
+  bash_process_script script
+  |> Process_Result.print
+  |> Process_Result.rc;
 
 fun bash_output s =
   let
-    val res = bash_process s;
+    val res = bash_process_script s;
     val _ = warning (Process_Result.err res);
   in (Process_Result.out res, Process_Result.rc res) end;
 
@@ -71,7 +77,7 @@
 (* bash functions *)
 
 fun bash_functions () =
-  bash_process "declare -Fx"
+  bash_process_script "declare -Fx"
   |> Process_Result.check
   |> Process_Result.out_lines
   |> map_filter (space_explode " " #> try List.last);
diff -r bba35ad317ab -r 0f051404f487 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Aug 07 22:23:37 2021 +0200
@@ -381,6 +381,7 @@
     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,
@@ -388,7 +389,7 @@
     cleanup: () => Unit = () => ()): Process_Result =
   {
     Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
-      result(progress_stdout = progress_stdout, progress_stderr = progress_stderr,
+      result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr,
         watchdog = watchdog, strict = strict)
   }
 
diff -r bba35ad317ab -r 0f051404f487 src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/Pure/System/process_result.ML	Sat Aug 07 22:23:37 2021 +0200
@@ -6,6 +6,8 @@
 
 signature PROCESS_RESULT =
 sig
+  val interrupt_rc: int
+  val timeout_rc: int
   type T
   val make:
    {rc: int,
@@ -27,6 +29,9 @@
 structure Process_Result: PROCESS_RESULT =
 struct
 
+val interrupt_rc = 130
+val timeout_rc = 142
+
 abstype T =
   Process_Result of
    {rc: int,
diff -r bba35ad317ab -r 0f051404f487 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/Pure/Tools/generated_files.ML	Sat Aug 07 22:23:37 2021 +0200
@@ -332,7 +332,7 @@
 (* execute compiler -- auxiliary *)
 
 fun execute dir title compile =
-  Isabelle_System.bash_process ("cd " ^ File.bash_path dir ^ " && " ^ compile)
+  Isabelle_System.bash_process_script ("cd " ^ File.bash_path dir ^ " && " ^ compile)
   |> Process_Result.check
   |> Process_Result.out
     handle ERROR msg =>
diff -r bba35ad317ab -r 0f051404f487 src/Pure/Tools/ghc.ML
--- a/src/Pure/Tools/ghc.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/Pure/Tools/ghc.ML	Sat Aug 07 22:23:37 2021 +0200
@@ -84,7 +84,7 @@
     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
+      Isabelle_System.bash_process_script
         ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
           " --bare " ^ File.bash_platform_path template_path)
       |> Process_Result.check;
diff -r bba35ad317ab -r 0f051404f487 src/Pure/Tools/jedit.ML
--- a/src/Pure/Tools/jedit.ML	Sat Aug 07 21:25:47 2021 +0200
+++ b/src/Pure/Tools/jedit.ML	Sat Aug 07 22:23:37 2021 +0200
@@ -36,7 +36,7 @@
 
 fun xml_resource name =
   let
-    val res = Isabelle_System.bash_process ("unzip -p \"$JEDIT_JAR\" " ^ Bash.string name);
+    val res = Isabelle_System.bash_process_script ("unzip -p \"$JEDIT_JAR\" " ^ Bash.string name);
     val rc = Process_Result.rc res;
   in
     res |> Process_Result.check |> Process_Result.out |> XML.parse