--- 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;
--- 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 ^
--- 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
--- 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 _ =
--- 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 ::
--- 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);
--- 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)
}
--- 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,
--- 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 =>
--- 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;
--- 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