add timing information in evaluation output

Auto.lean

@@ -1,4 +1,5 @@
 import Auto.Tactic
-import Auto.EvaluateAuto.TestCode
+import Auto.EvaluateAuto.TestAuto
+import Auto.EvaluateAuto.TestTactics
 
 def hello := "world"

Auto/EvaluateAuto/TestAuto.lean

@@ -133,16 +133,17 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit
   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 := #[]
+  let globalStartTime ← IO.monoMsNow
+  let mut results : Array (Result × Nat) := #[]
   for name in names do
     let ci ← Name.getCi name decl_name%
     trace[auto.eval.printProblem] m!"Testing || {name} : {ci.type}"
     if let .some fhandle := logFileHandle? then
       fhandle.putStrLn ""
-      fhandle.putStrLn s!"Testing || {name} : {← (Lean.Meta.ppExpr ci.type).run'}"
       fhandle.putStrLn s!"Timestamp : {← Std.Time.Timestamp.now}"
+      fhandle.putStrLn s!"Testing || {name} : {← (Lean.Meta.ppExpr ci.type).run'}"
       fhandle.flush
+    let startTime ← IO.monoMsNow
     let result : Result ← withCurrHeartbeats <|
       withReader (fun ctx => {ctx with maxHeartbeats := config.maxHeartbeats * 1000}) <|
         if nonterms.contains name then
@@ -182,15 +183,16 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit
               | .eproverHo      => auto.tptp.eproverHo.path.set o path
               | .vampire        => auto.tptp.vampire.path.set o path) <|
                 runProverOnConst name (Auto.runAuto (.some name))
-    trace[auto.eval.printResult] m!"{result}"
-    results := results.push result
+    let problemTime := (← IO.monoMsNow) - startTime
+    trace[auto.eval.printResult] m!"{result}\nElapsed time: {problemTime}ms"
+    results := results.push (result, problemTime)
     if let .some fhandle := logFileHandle? then
-      fhandle.putStrLn (toString (← MessageData.format m!"{result}"))
+      fhandle.putStrLn (toString (← MessageData.format m!"{result}\nElapsed time : {problemTime}ms"))
   if let .some fhandle := resultFileHandle? then
-    fhandle.putStrLn s!"Elapsed time: {(← IO.monoMsNow) - startTime} ms"
+    fhandle.putStrLn s!"Total elapsed time: {(← IO.monoMsNow) - globalStartTime} ms"
     fhandle.putStrLn s!"\nSummary:\n"
     for ((name, result), idx) in (names.zip results).zipWithIndex do
-      fhandle.putStrLn s!"{idx} {result.concise} {Name.uniqRepr name}"
+      fhandle.putStrLn s!"{idx} {result.fst.concise} {result.snd} {Name.uniqRepr name}"
 
 def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := do
   let names ← NameArray.load fname
@@ -319,7 +321,7 @@ where
   Read results generated by `evalAutoAtMathlibHumanTheorems`
 -/
 def readAutoEvalResult (config : EvalAutoOnMathlibConfig) :
-  CoreM (Array (Name × Result)) := do
+  CoreM (Array (Name × Result × Nat)) := do
   let resultFolder := config.resultFolder
   if !(← System.FilePath.isDir resultFolder) then
     throwError "{decl_name%} :: {config.resultFolder} is not a directory"
@@ -336,13 +338,17 @@ def readAutoEvalResult (config : EvalAutoOnMathlibConfig) :
       ret := ret.append lineAnalysis
   return ret
 where
-  analyzeLine (line : String) : CoreM (Name × Result) := do
+  analyzeLine (line : String) : CoreM (Name × Result × Nat) := do
     let line := (line.dropWhile (fun c => c != ' ')).drop 1
     let s := line.takeWhile (fun c => c != ' ')
-    let .some tr := Result.ofConcise? s
+    let .some res := Result.ofConcise? s
       | throwError s!"{decl_name%} :: {s} is not a concise representation of a `Result`"
-    let line := (line.dropWhile (fun c => c != ' ')).drop 2
+    let line := (line.dropWhile (fun c => c != ' ')).drop 1
+    let s := line.takeWhile (fun c => c != ' ')
+    let .some t := String.toNat? s
+      | throwError s!"{decl_name%} :: {s} is not a string representation of a Nat"
+    let line := (line.dropWhile (fun c => c != ' ')).drop 1
     let name := Name.parseUniqRepr line
-    return (name, tr)
+    return (name, res, t)
 
 end EvalAuto

Auto/EvaluateAuto/TestTactics.lean

@@ -210,36 +210,39 @@ def evalTacticsAtModule
     else
       return .none)
   if let .some fhandle := resultFileHandle? then
-    fhandle.putStrLn s!"Elapsed time : {(← IO.monoMsNow) - startTime} ms"
+    fhandle.putStrLn s!"Total elapsed time : {(← IO.monoMsNow) - startTime} ms"
     fhandle.putStrLn s!"\nSummary:\n"
     for ((name, result), idx) in results.zipWithIndex do
-      fhandle.putStrLn s!"{idx} {result.map Result.concise} {Name.uniqRepr name}"
+      let resultStrs := result.map (fun (r, t) => Result.concise r ++ " " ++ toString t)
+      fhandle.putStrLn s!"{idx} {resultStrs} {Name.uniqRepr name}"
 where
   evalAction
     (context : Core.Context) (state : Core.State) (ci : ConstantInfo)
     (logFileHandle? : Option IO.FS.Handle) (config : EvalTacticConfig)
-    (nonterms : Std.HashSet (RegisteredTactic × Name)) : IO (Array Result) := do
+    (nonterms : Std.HashSet (RegisteredTactic × Name)) : IO (Array (Result × Nat)) := do
   config.tactics.zipWithIndex.mapM (fun (tactic, idx) => do
     let metaAction : MetaM Result :=
       Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic.toCiTactic ci)
-    let coreAction : CoreM Result := (do
+    let coreAction : CoreM (Result × Nat) := (do
       trace[auto.eval.printProblem] m!"Testing tactic {idx} || {ci.name} : {ci.type}"
       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!"Timestamp : {← Std.Time.Timestamp.now}"
+        fhandle.putStrLn s!"Testing tactic {idx} || {ci.name} : {← (Lean.Meta.ppExpr ci.type).run'}"
         fhandle.flush
+      let problemStartTime ← IO.monoMsNow
       let result ← (do
         if nonterms.contains (tactic, ci.name) then
           return Result.nonterminate
         else
           withCurrHeartbeats <|
             withReader (fun ctx => { ctx with maxHeartbeats := config.maxHeartbeats * 1000 }) <|
               Meta.MetaM.run' metaAction)
-      trace[auto.eval.printResult] m!"{result}"
+      let problemTime := (← IO.monoMsNow) - problemStartTime
+      trace[auto.eval.printResult] m!"{result}\nElapsed time : {problemTime}ms"
       if let .some fhandle := logFileHandle? then
-        fhandle.putStrLn (toString (← MessageData.format m!"{result}"))
-      return result)
+        fhandle.putStrLn (toString (← MessageData.format m!"{result}\nElapsed time : {problemTime}ms"))
+      return (result, problemTime))
     let (result, _) ← coreAction.toIO context state
     return result)
 
@@ -353,7 +356,7 @@ where
   Read results generated by `evalTacticsAtMathlibHumanTheorems`
 -/
 def readTacticEvalResult (config : EvalTacticOnMathlibConfig) :
-  CoreM (Array (Name × Array (Name × Array Result))) := do
+  CoreM (Array (Name × Array (Name × Array (Result × Nat)))) := do
   let resultFolder := config.resultFolder
   if !(← System.FilePath.isDir resultFolder) then
     throwError "{decl_name%} :: {config.resultFolder} is not a directory"
@@ -372,13 +375,18 @@ def readTacticEvalResult (config : EvalTacticOnMathlibConfig) :
       ret := ret.push (modName, lineAnalysis)
   return ret
 where
-  analyzeLine (line : String) : CoreM (Name × Array Result) := do
+  analyzeLine (line : String) : CoreM (Name × Array (Result × Nat)) := do
     let line := (line.dropWhile (fun c => c != ' ')).drop 3
     let tr := (line.takeWhile (fun c => c != ']')).splitOn ", "
-    let tr : Array Result ← (Array.mk tr).mapM (fun s => do
-      match Result.ofConcise? s with
-      | .some r => return r
-      | .none => throwError s!"{decl_name%} :: {s} is not a concise representation of a `Result`")
+    let tr : Array (Result × Nat) ← (Array.mk tr).mapM (fun s => do
+      let sr := s.take 1
+      let st := s.drop 2
+      match Result.ofConcise? sr with
+      | .some r =>
+        match String.toNat? st with
+        | .some t => return (r, t)
+        | .none => throwError s!"{decl_name%} :: {st} is not a string representation of a Nat"
+      | .none => throwError s!"{decl_name%} :: {sr} is not a concise representation of a `Result`")
     let line := (line.dropWhile (fun c => c != ']')).drop 2
     let name := Name.parseUniqRepr line
     return (name, tr)