# 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