use timestamp instead of IO.monoMsNow

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

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
@@ -4,6 +4,7 @@ import Auto.EvaluateAuto.Result
 import Auto.EvaluateAuto.ConstAnalysis
 import Auto.EvaluateAuto.EnvAnalysis
 import Auto.EvaluateAuto.NameArr
+import Std
 import Auto.Tactic
 
 open Lean Auto
@@ -121,6 +122,7 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit
   trace[auto.eval.printConfig] m!"Config = {config}"
   if let .some fhandle := logFileHandle? then
     fhandle.putStrLn s!"Config = {config}"
+    fhandle.putStrLn s!"Start time : {← Std.Time.Timestamp.now}"
   let startTime ← IO.monoMsNow
   let mut results := #[]
   for name in names do
@@ -129,7 +131,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.putStrLn s!"Timestamp : {← Std.Time.Timestamp.now}"
       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
@@ -5,6 +5,7 @@ import Auto.EvaluateAuto.ConstAnalysis
 import Auto.EvaluateAuto.EnvAnalysis
 import Auto.EvaluateAuto.NameArr
 import Auto.EvaluateAuto.CommandAnalysis
+import Std
 open Lean
 
 namespace EvalAuto
@@ -190,6 +191,7 @@ def evalAtModule
   trace[auto.eval.printConfig] m!"Config = {config}"
   if let .some fhandle := logFileHandle? then
     fhandle.putStrLn s!"Config = {config}"
+    fhandle.putStrLn s!"Start time : {← Std.Time.Timestamp.now}"
   let .some uri ← Server.documentUriFromModule searchPath modName
     | throwError "{decl_name%} :: Cannot find module {modName}"
   let .some path := System.Uri.fileUriToPath? uri
@@ -225,7 +227,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.putStrLn s!"Timestamp : {← Std.Time.Timestamp.now}"
         fhandle.flush
       let result ← (do
         if nonterms.contains (tactic, ci.name) then