From 8650ab97adf33e2d69754189e329f001d5c41a66 Mon Sep 17 00:00:00 2001
From: PratherConid <syxx2013050321@163.com>
Date: Sun, 12 Jan 2025 01:31:47 -0800
Subject: [PATCH] add IO.monoMsNow time stamp

---
 Auto/EvaluateAuto/TestAuto.lean    | 1 +
 Auto/EvaluateAuto/TestTactics.lean | 1 +
 2 files changed, 2 insertions(+)

diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
index 4c16414..60880cb 100644
--- a/Auto/EvaluateAuto/TestAuto.lean
+++ b/Auto/EvaluateAuto/TestAuto.lean
@@ -129,6 +129,7 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit
     if let .some fhandle := logFileHandle? then
       fhandle.putStrLn ""
       fhandle.putStrLn s!"Testing || {name} : {← (Lean.Meta.ppExpr ci.type).run'}"
+      fhandle.putStrLn s!"IO.monoMsNow : {← IO.monoMsNow}"
       fhandle.flush
     let result : Result ← withCurrHeartbeats <|
       withReader (fun ctx => {ctx with maxHeartbeats := config.maxHeartbeats * 1000}) <|
diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean
index 0994996..4c4889a 100644
--- a/Auto/EvaluateAuto/TestTactics.lean
+++ b/Auto/EvaluateAuto/TestTactics.lean
@@ -225,6 +225,7 @@ where
       if let .some fhandle := logFileHandle? then
         fhandle.putStrLn ""
         fhandle.putStrLn s!"Testing tactic {idx} || {ci.name} : {← (Lean.Meta.ppExpr ci.type).run'}"
+        fhandle.putStrLn s!"IO.monoMsNow : {← IO.monoMsNow}"
         fhandle.flush
       let result ← (do
         if nonterms.contains (tactic, ci.name) then