--- 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 =
--- 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 *)
--- 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
--- 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 =
--- 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))
}
--- 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);
--- 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";
--- 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")
}
}
}
--- 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;
--- /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;
--- 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))
--- 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)
--- 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
--- 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;
--- 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;
--- 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;