# HG changeset patch # User wenzelm # Date 1614030110 -3600 # Node ID 652b8913437472fd76d0b4718e49eda1f1a25a3b # Parent ce4fe0b1cfdac0c31b3a5fa70bd8836102495294# Parent 0e7a3c055f39ae8754fc5e2966888634f2b124a1 merged diff -r ce4fe0b1cfda -r 652b89134374 src/HOL/Tools/Nunchaku/nunchaku_tool.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Mon Feb 22 22:41:50 2021 +0100 @@ -103,30 +103,33 @@ [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 {out = output, err = error, rc = code, ...} = Isabelle_System.bash_process bash_cmd; + val res = Isabelle_System.bash_process bash_cmd; + val rc = Process_Result.rc res; + val out = Process_Result.out res; + val err = Process_Result.err res; val backend = - (case map_filter (try (unprefix "{backend:")) (split_lines output) of + (case map_filter (try (unprefix "{backend:")) (split_lines out) of [s] => hd (space_explode "," s) | _ => unknown_solver); in - if String.isPrefix "SAT" output then - (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []}) - else if String.isPrefix "UNSAT" output then + if String.isPrefix "SAT" out then + (if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []}) + else if String.isPrefix "UNSAT" out then if complete then Unsat backend else Unknown NONE - else if String.isSubstring "TIMEOUT" output + else if String.isSubstring "TIMEOUT" out (* FIXME: temporary *) - orelse String.isSubstring "kodkod failed (errcode 152)" error then + orelse String.isSubstring "kodkod failed (errcode 152)" err then Timeout - else if String.isPrefix "UNKNOWN" output then + else if String.isPrefix "UNKNOWN" out then Unknown NONE - else if code = 126 then + else if rc = 126 then Nunchaku_Cannot_Execute - else if code = 127 then + else if rc = 127 then Nunchaku_Not_Found else - Unknown_Error (code, - simplify_spaces (elide_string 1000 (if error <> "" then error else output))) + Unknown_Error (rc, + simplify_spaces (elide_string 1000 (if err <> "" then err else out))) end); fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem = diff -r ce4fe0b1cfda -r 652b89134374 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Feb 22 22:41:50 2021 +0100 @@ -818,11 +818,12 @@ if getenv env_var = "" then (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "") else - (case Isabelle_System.bash_output (cmd ^ File.bash_path file) of - (out, 0) => out - | (_, rc) => - error ("Error caused by prolog system " ^ env_var ^ - ": return code " ^ string_of_int rc)) + let val res = Isabelle_System.bash_process (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 ^ + ": return code " ^ string_of_int (Process_Result.rc res)) msg + end end @@ -865,7 +866,7 @@ (l :: r :: []) => parse_term (unprefix " " r) | _ => raise Fail "unexpected equation in prolog output") fun parse_solution s = map dest_eq (space_explode ";" s) - in map parse_solution (Library.trim_split_lines sol) end + in map parse_solution (split_lines sol) end (* calling external interpreter and getting results *) diff -r ce4fe0b1cfda -r 652b89134374 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Feb 22 22:41:50 2021 +0100 @@ -214,10 +214,6 @@ |> Exn.capture f |> Exn.release -fun elapsed_time description e = - let val ({elapsed, ...}, result) = Timing.timing e () - in (result, (description, Time.toMilliseconds elapsed)) end - fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = let @@ -265,23 +261,29 @@ (map File.bash_platform_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ " -o " ^ File.bash_platform_path executable ^ ";" - val (_, compilation_time) = - elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) - val _ = Quickcheck.add_timing compilation_time current_result + val compilation_time = + Isabelle_System.bash_process cmd + |> Process_Result.check + |> Process_Result.timing_elapsed |> Time.toMilliseconds + handle ERROR msg => cat_error "Compilation with GHC failed" msg + val _ = Quickcheck.add_timing ("Haskell compilation", compilation_time) current_result fun haskell_string_of_bool v = if v then "True" else "False" - val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else () fun with_size genuine_only k = if k > size then (NONE, !current_result) else let val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k - val ((response, _), timing) = - elapsed_time ("execution of size " ^ string_of_int k) - (fn () => Isabelle_System.bash_output - (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ - string_of_int k)) - val _ = Quickcheck.add_timing timing current_result + val res = + Isabelle_System.bash_process + (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ + string_of_int k) + |> Process_Result.check + val response = Process_Result.out res + val timing = res |> Process_Result.timing_elapsed |> Time.toMilliseconds; + val _ = + Quickcheck.add_timing + ("execution of size " ^ string_of_int k, timing) current_result in if response = "NONE" then with_size genuine_only (k + 1) else diff -r ce4fe0b1cfda -r 652b89134374 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Feb 22 22:41:50 2021 +0100 @@ -574,7 +574,7 @@ (warning (case extract_known_atp_failure known_perl_failures output of SOME failure => string_of_atp_failure failure - | NONE => trim_line output); []))) () + | NONE => output); []))) () handle Timeout.TIMEOUT _ => [] fun find_remote_system name [] systems = diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/Admin/components.scala --- a/src/Pure/Admin/components.scala Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/Admin/components.scala Mon Feb 22 22:41:50 2021 +0100 @@ -279,9 +279,8 @@ } yield { progress.echo("Digesting remote " + entry.name) - Library.trim_line( - ssh.execute("cd " + ssh.bash_path(components_dir) + - "; sha1sum " + Bash.string(entry.name)).check.out) + ssh.execute("cd " + ssh.bash_path(components_dir) + + "; sha1sum " + Bash.string(entry.name)).check.out } write_components_sha1(read_components_sha1(lines)) } diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/General/exn.ML Mon Feb 22 22:41:50 2021 +0100 @@ -105,7 +105,7 @@ (* POSIX return code *) fun return_code exn rc = - if is_interrupt exn then (130: int) else rc; + if is_interrupt exn then 130 else rc; fun capture_exit rc f x = f x handle exn => exit (return_code exn rc); diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/ROOT.ML Mon Feb 22 22:41:50 2021 +0100 @@ -294,6 +294,7 @@ (*Isabelle system*) ML_file "PIDE/protocol_command.ML"; ML_file "System/scala.ML"; +ML_file "System/process_result.ML"; ML_file "System/isabelle_system.ML"; diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/System/bash.scala Mon Feb 22 22:41:50 2021 +0100 @@ -223,8 +223,11 @@ case _ if is_interrupt => "" case Exn.Exn(exn) => Exn.message(exn) case Exn.Res(res) => - (res.rc.toString :: res.out_lines.length.toString :: - res.out_lines ::: res.err_lines).mkString("\u0000") + (res.rc.toString :: + res.timing.elapsed.ms.toString :: + res.timing.cpu.ms.toString :: + res.out_lines.length.toString :: + res.out_lines ::: res.err_lines).mkString("\u0000") } } } diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/System/isabelle_system.ML Mon Feb 22 22:41:50 2021 +0100 @@ -6,10 +6,7 @@ signature ISABELLE_SYSTEM = sig - type process_result = - {rc: int, out_lines: string list, err_lines: string list, out: string, err: string} - val bash_process: string -> process_result - val bash_output_check: string -> string + val bash_process: string -> Process_Result.T val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list @@ -31,45 +28,42 @@ (* bash *) -type process_result = - {rc: int, out_lines: string list, err_lines: string list, out: string, err: string}; - -fun bash_process script : process_result = +fun bash_process script = Scala.function_thread "bash_process" ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |> space_explode "\000" |> (fn [] => raise Exn.Interrupt | [err] => error err - | a :: b :: lines => + | a :: b :: c :: d :: lines => let val rc = Value.parse_int a; - val ((out, err), (out_lines, err_lines)) = - chop (Value.parse_int b) lines |> `(apply2 cat_lines); - in {rc = rc, out_lines = out_lines, err_lines = err_lines, out = out, err = err} end); + val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); + val (out_lines, err_lines) = chop (Value.parse_int d) lines; + in + 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"); -fun bash_output_check s = - (case bash_process s of - {rc = 0, out, ...} => trim_line out - | {err, ...} => error (trim_line err)); +val bash = bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let - val {out, err, rc, ...} = bash_process s; - val _ = warning (trim_line err); - in (out, rc) end; - -fun bash s = - let - val (out, rc) = bash_output s; - val _ = writeln (trim_line out); - in rc end; + val res = bash_process s; + val _ = warning (Process_Result.err res); + in (Process_Result.out res, Process_Result.rc res) end; (* bash functions *) fun bash_functions () = - bash_output_check "declare -Fx" - |> split_lines |> map_filter (space_explode " " #> try List.last); + bash_process "declare -Fx" + |> Process_Result.check + |> Process_Result.out_lines + |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN @@ -145,9 +139,12 @@ fun download url = with_tmp_file "download" "" (fn path => - ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path) - |> bash_process - |> (fn {rc = 0, ...} => File.read path - | {err, ...} => cat_error ("Failed to download " ^ quote url) err)); + let + val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path; + val res = bash_process s; + in + if Process_Result.ok res then File.read path + else cat_error ("Failed to download " ^ quote url) (Process_Result.err res) + end); end; diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/System/process_result.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/process_result.ML Mon Feb 22 22:41:50 2021 +0100 @@ -0,0 +1,62 @@ +(* Title: Pure/System/process_result.scala + Author: Makarius + +Result of system process. +*) + +signature PROCESS_RESULT = +sig + type T + val make: + {rc: int, + out_lines: string list, + err_lines: string list, + timing: Timing.timing} -> T + val rc: T -> int + val out_lines: T -> string list + val err_lines: T -> string list + val timing: T -> Timing.timing + val timing_elapsed: T -> Time.time + val out: T -> string + val err: T -> string + val ok: T -> bool + val check: T -> T + val print: T -> T +end; + +structure Process_Result: PROCESS_RESULT = +struct + +abstype T = + Process_Result of + {rc: int, + out_lines: string list, + err_lines: string list, + timing: Timing.timing} +with + +val make = Process_Result; +fun rep (Process_Result args) = args; + +val rc = #rc o rep; +val out_lines = #out_lines o rep; +val err_lines = #err_lines o rep; + +val timing = #timing o rep; +val timing_elapsed = #elapsed o timing; + +end; + +val out = trim_line o cat_lines o out_lines; +val err = trim_line o cat_lines o err_lines; + +fun ok result = rc result = 0; + +fun check result = if ok result then result else error (err result); + +fun print result = + (warning (err result); + writeln (out result); + make {rc = rc result, out_lines = [], err_lines = [], timing = timing result}); + +end; diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/System/process_result.scala Mon Feb 22 22:41:50 2021 +0100 @@ -38,8 +38,8 @@ err_lines: List[String] = Nil, timing: Timing = Timing.zero) { - def out: String = cat_lines(out_lines) - def err: String = cat_lines(err_lines) + def out: String = Library.trim_line(cat_lines(out_lines)) + def err: String = Library.trim_line(cat_lines(err_lines)) def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs.flatMap(split_lines)) diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/Thy/presentation.scala Mon Feb 22 22:41:50 2021 +0100 @@ -680,7 +680,7 @@ if (!result.ok) { val message = Exn.cat_message( - Library.trim_line(result.err), + result.err, cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), "Failed to build document " + quote(doc.name)) throw new Build_Error(log_lines, message) diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/Tools/doc.scala Mon Feb 22 22:41:50 2021 +0100 @@ -22,7 +22,7 @@ dir <- dirs() catalog = dir + Path.basic("Contents") if catalog.is_file - line <- split_lines(Library.trim_line(File.read(catalog))) + line <- Library.trim_split_lines(File.read(catalog)) } yield (dir, line) sealed abstract class Entry diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/Tools/generated_files.ML Mon Feb 22 22:41:50 2021 +0100 @@ -332,7 +332,9 @@ (* execute compiler -- auxiliary *) fun execute dir title compile = - Isabelle_System.bash_output_check ("cd " ^ File.bash_path dir ^ " && " ^ compile) + Isabelle_System.bash_process ("cd " ^ File.bash_path dir ^ " && " ^ compile) + |> Process_Result.check + |> Process_Result.out handle ERROR msg => let val (s, pos) = Input.source_content title in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end; diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/Tools/ghc.ML --- a/src/Pure/Tools/ghc.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/Tools/ghc.ML Mon Feb 22 22:41:50 2021 +0100 @@ -84,9 +84,10 @@ 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_output_check + Isabelle_System.bash_process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ - " --bare " ^ File.bash_platform_path template_path); + " --bare " ^ File.bash_platform_path template_path) + |> Process_Result.check; in () end; end; diff -r ce4fe0b1cfda -r 652b89134374 src/Pure/Tools/jedit.ML --- a/src/Pure/Tools/jedit.ML Mon Feb 22 18:28:12 2021 +0000 +++ b/src/Pure/Tools/jedit.ML Mon Feb 22 22:41:50 2021 +0100 @@ -35,10 +35,13 @@ val xml_file = XML.parse o File.read; fun xml_resource name = - let val script = "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name in - (case Isabelle_System.bash_output script of - (txt, 0) => XML.parse txt - | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)) + let + val res = + Isabelle_System.bash_process ("unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name); + val rc = Process_Result.rc res; + in + res |> Process_Result.check |> Process_Result.out |> XML.parse + handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc) end;