# 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