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