# HG changeset patch
# User wenzelm
# Date 1614014216 -3600
# Node ID 057d8a164a7bdf7da968faf8dc9d6ede1621f3aa
# Parent  dcadb3243cfa97fc54bb6f2541fb0d73d2037176
more direct timing from bash_process wrapper;

diff -r dcadb3243cfa -r 057d8a164a7b src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Feb 22 17:19:05 2021 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Feb 22 18:16:56 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,9 +261,11 @@
               (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.print
+          |> Process_Result.timing |> #elapsed |> Time.toMilliseconds;
+        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 =
@@ -276,12 +274,16 @@
             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);
+              val _ = warning (Process_Result.err res);
+              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