# HG changeset patch
# User desharna
# Date 1642763395 -3600
# Node ID d699eb2d26ad4151345d98ca3843192b11833803
# Parent  7c123c76a8c972be952e73ffa7f5853939b4f2b3
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads

diff -r 7c123c76a8c9 -r d699eb2d26ad src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Jan 20 13:56:51 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Jan 21 12:09:55 2022 +0100
@@ -137,10 +137,10 @@
     val goal_name_path = Path.basic (#name command)
     val line_path = Path.basic (string_of_int (the (Position.line_of pos)));
     val offset_path = Path.basic (string_of_int (the (Position.offset_of pos)));
-    val ({cpu, ...}, s) = Timing.timing run_action_function (fn () => run_action command);
+    val ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run_action command);
     val export_name =
       Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path +
-        line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds cpu)));
+        line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds elapsed)));
   in
     Export.export thy export_name [XML.Text s]
   end;
@@ -349,7 +349,8 @@
   | NONE => default);
 
 fun cpu_time f x =
-  let val ({cpu, ...}, y) = Timing.timing f x
-  in (y, Time.toMilliseconds cpu) end;
+  (* CPU time is problematics with multithreading as it refers to the per-process CPU time. *)
+  let val ({elapsed, ...}, y) = Timing.timing f x
+  in (y, Time.toMilliseconds elapsed) end;
 
 end