add IO.monoMsNow time stamp

leanprover-community · Jan 12, 2025 · 8650ab9 · 8650ab9
1 parent 384d308
commit 8650ab9
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git 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
@@ -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