# HG changeset patch
# User desharna
# Date 1634548319 -7200
# Node ID 64c0d78d2f19ce9aa7d7ab803df25d356eef5a01
# Parent  9a2d290a3a0b06e5d4e219bbe5a00c845e50dc87
added timing to Mirabelle action arith

diff -r 9a2d290a3a0b -r 64c0d78d2f19 src/HOL/Tools/Mirabelle/mirabelle_arith.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Mon Oct 18 11:11:22 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Mon Oct 18 11:11:59 2021 +0200
@@ -13,10 +13,9 @@
 fun make_action ({timeout, ...} : Mirabelle.action_context) =
   let
     fun run_action ({pre, ...} : Mirabelle.command) =
-      if Mirabelle.can_apply timeout Arith_Data.arith_tac pre then
-        "succeeded"
-      else
-        ""
+      (case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
+        ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
+      | (_, false) => "failed")
   in {run_action = run_action, finalize = K ""} end
 
 val () = Mirabelle.register_action "arith" make_action