# HG changeset patch
# User wenzelm
# Date 1615660185 -3600
# Node ID 9d1b5c0bdec8e8dbceeb7f1c64a11f0b4fa30de1
# Parent  97bb6ef3dbd421b3d8fb0fabeefca2bfad912ca9
more direct elapsed run_time via bash_process wrapper (via Scala and C);

diff -r 97bb6ef3dbd4 -r 9d1b5c0bdec8 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Mar 13 15:39:48 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Mar 13 19:29:45 2021 +0100
@@ -175,17 +175,6 @@
         end
       | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set"))
 
-    fun split_time s =
-      let
-        val split = String.tokens (fn c => str c = "\n")
-        val (output, t) = s |> split |> (try split_last #> the_default ([], "0")) |>> cat_lines
-        val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
-        val digit = Scan.one Symbol.is_ascii_digit
-        val num3 = digit ::: digit ::: (digit >> single) >> (fst o read_int)
-        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
-        val as_time = raw_explode #> Scan.read Symbol.stopper time #> the_default 0
-      in (output, as_time t |> Time.fromMilliseconds) end
-
     fun run () =
       let
         (* If slicing is disabled, we expand the last slice to fill the entire time available. *)
@@ -276,9 +265,7 @@
             val args =
               arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path)
                 (ord, ord_info, sel_weights)
-            val command =
-              "(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")"
-              |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
+            val command = "exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args
 
             val _ =
               atp_problem
@@ -287,9 +274,11 @@
               |> File.write_list prob_path
 
             val ((output, run_time), (atp_proof, outcome)) =
-              Timeout.apply generous_slice_timeout Isabelle_System.bash_output command
-              |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
-              |> fst |> split_time
+              Timeout.apply generous_slice_timeout Isabelle_System.bash_process command
+              |> (fn res =>
+                (Process_Result.out res |>
+                  (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I),
+                 Process_Result.timing_elapsed res))
               |> (fn accum as (output, _) =>
                 (accum,
                  extract_tstplike_proof_and_outcome verbose proof_delims known_failures output