more test code

Auto/EvaluateAuto/EnvAnalysis.lean

@@ -1,4 +1,5 @@
 import Lean
+import Auto.EvaluateAuto.NameArr
 
 open Lean
 
@@ -17,6 +18,11 @@ def mathlibModules : CoreM (Array Name) := do
   let u := (← getEnv).header.moduleNames
   return u.filter (fun name => name.components[0]? == .some `Mathlib)
 
+/- Check that all mathlib modules names are ordinary -/
+def allMathlibModuleNamesCanBeFilename : CoreM Bool := do
+  let mms ← mathlibModules
+  return mms.all Name.canBeFilename
+
 /-- Pick `n` elements from array `xs`. Elements may duplicate -/
 def Array.randPick {α} (xs : Array α) (n : Nat) : IO (Array α) := do
   let mut ret := #[]

Auto/EvaluateAuto/NameArr.lean

@@ -3,6 +3,18 @@ open Lean
 
 namespace EvalAuto
 
+/--
+  Whether a name is a valid filename
+-/
+def Name.canBeFilename (n : Name) : Bool :=
+  n.components.all (fun n =>
+    match n with
+    | .str _ s =>
+      match s.get? 0 with
+      | .some c => s.all (fun c => c.isAlphanum || c == '_' || c == '\'')
+      | .none => false
+    | _ => false)
+
 /--
   Unique string representation of array of names
   We use `.` to separate fields of a name, and `\n` to separate names.

Auto/EvaluateAuto/Result.lean

@@ -13,6 +13,7 @@ inductive Result
   | nonProp
   | typeCheckFail
   | typeUnequal
+  | nonterminate
   -- `auto` does not produce subgoals, but other tactics we test might (such as `simp`)
   | subGoals
   | exception (e : Exception)
@@ -23,6 +24,7 @@ instance : ToMessageData Result where
   | .nonProp         => "Result.nonProp"
   | .typeCheckFail   => "Result.typeCheckFail"
   | .typeUnequal     => "Result.typeUnequal"
+  | .nonterminate    => "Result.nonterminate"
   | .subGoals        => "Result.subGoals"
   | .exception e     => m!"Result.exception ::\n{e.toMessageData}"
 
@@ -31,6 +33,7 @@ def Result.concise : Result → String
 | .nonProp => "N"
 | .typeCheckFail => "F"
 | .typeUnequal => "U"
+| .nonterminate => "T"
 | .subGoals => "G"
 | .exception _ => "E"
 

Auto/EvaluateAuto/TestAuto.lean

@@ -29,18 +29,24 @@ structure EvalAutoConfig where
   timeout       : Nat           := 10
   /-- Solver configuration -/
   solverConfig  : SolverConfig
-  /-- Optional logfile for saving the result of the evaluation -/
+  /-- Optional file for saving the log of the evaluation -/
   logFile       : Option String := .none
+  /-- Optional file for saving the result of the evaluation -/
+  resultFile    : Option String := .none
 
 instance : ToString EvalAutoConfig where
   toString : EvalAutoConfig → String
-  | ⟨maxHeartbeats, timeout, solverConfig, logFile⟩ =>
+  | ⟨maxHeartbeats, timeout, solverConfig, logFile, resultFile⟩ =>
     let logFileStr :=
       match logFile with
       | .some logFile => s!", logFile := {logFile}"
       | .none => ""
+    let resultFileStr :=
+      match resultFile with
+      | .some resultFile => s!", logFile := {resultFile}"
+      | .none => ""
     s!"\{maxHeartbeats := {maxHeartbeats}, timeout := {timeout}, " ++
-    s!"solverConfig := {solverConfig}{logFileStr}}"
+    s!"solverConfig := {solverConfig}{logFileStr}{resultFileStr}}"
 
 /--
   Run `Lean-auto` on `lem.type`, using premises collected from `lem.proof`
@@ -102,6 +108,7 @@ def disableAllSolvers (o : Options) : Options :=
 
 def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit := do
   let logFileHandle? : Option IO.FS.Handle ← config.logFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
+  let resultFileHandle? : Option IO.FS.Handle ← config.resultFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
   trace[auto.eval.printConfig] m!"Config = {config}"
   if let .some fhandle := logFileHandle? then
     fhandle.putStrLn s!"Config = {config}"
@@ -113,6 +120,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.flush
     let result : Result ← withCurrHeartbeats <|
       withReader (fun ctx => {ctx with maxHeartbeats := config.maxHeartbeats * 1000}) <|
         match config.solverConfig with
@@ -151,8 +159,7 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit
     results := results.push result
     if let .some fhandle := logFileHandle? then
       fhandle.putStrLn (toString (← MessageData.format m!"{result}"))
-  if let .some fhandle := logFileHandle? then
-    fhandle.putStrLn ""
+  if let .some fhandle := resultFileHandle? then
     fhandle.putStrLn s!"Elapsed time: {(← IO.monoMsNow) - startTime} ms"
     fhandle.putStrLn s!"\nSummary:\n"
     for ((name, result), idx) in (names.zip results).zipWithIndex do

Auto/EvaluateAuto/TestTactics.lean

@@ -81,6 +81,7 @@ section Tactics
     | useSimpAllWithPremises
     | useAesop
     | useAesopWithPremises
+  deriving BEq, Hashable
 
   instance : ToString RegisteredTactic where
     toString : RegisteredTactic → String
@@ -139,17 +140,32 @@ structure EvalTacticConfig where
   maxHeartbeats : Nat           := 65536
   /-- Tactics to run at each constant declaration -/
   tactics       : Array RegisteredTactic
-  /-- Optional logfile for saving the result of the evaluation -/
+  /-- Optional file for saving the log of the evaluation -/
   logFile       : Option String := .none
+  /-- Optional file for saving the result of the evaluation -/
+  resultFile    : Option String := .none
+  /--
+    On some problems, certain tactics may go into infinite loops not
+    guarded by `Core.checkMaxHeartbeats`. These instances should be
+    recorded here and avoided (throw error immediately) during evaluation.
+  -/
+  nonterminates : Array (RegisteredTactic × Name)
 
 instance : ToString EvalTacticConfig where
   toString : EvalTacticConfig → String
-  | ⟨maxHeartbeats, tactics, logFile⟩ =>
+  | ⟨maxHeartbeats, tactics, logFile, resultFile, nonterminates⟩ =>
     let logFileStr :=
       match logFile with
       | .some logFile => s!", logFile := {logFile}"
       | .none => ""
-    s!"\{maxHeartbeats := {maxHeartbeats}, tactics := {tactics}{logFileStr}}"
+    let resultFileStr :=
+      match resultFile with
+      | .some resultFile => s!", resultFile := {resultFile}"
+      | .none => ""
+    let nontermStr := String.intercalate ",\n" (nonterminates.map (fun (rt, n) => s!"    ({rt}, {n})")).toList
+    let nontermStr := if nonterminates.size != 0 then nontermStr ++ "\n" else nontermStr
+    s!"\{\n  maxHeartbeats := {maxHeartbeats}, tactics := {tactics}{logFileStr}{resultFileStr}" ++
+    s!"\n  nonterminates := #[\n{nontermStr}  ]\n}"
 
 /--
   Effectively `runTacticsAtConstantDeclaration` at each constant in `modName` which satisfies `filter`\
@@ -159,6 +175,7 @@ def evalAtModule
   (modName : Name) (searchPath : SearchPath) (filter : ConstantInfo → Bool)
   (config : EvalTacticConfig) : CoreM Unit:= do
   let logFileHandle? : Option IO.FS.Handle ← config.logFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
+  let resultFileHandle? : Option IO.FS.Handle ← config.resultFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
   trace[auto.eval.printConfig] m!"Config = {config}"
   if let .some fhandle := logFileHandle? then
     fhandle.putStrLn s!"Config = {config}"
@@ -170,24 +187,25 @@ def evalAtModule
   let inputHandle ← IO.FS.Handle.mk path .read
   let input ← inputHandle.readToEnd
   let startTime ← IO.monoMsNow
+  let nonterms := Std.HashSet.ofArray config.nonterminates
   let results ← runWithEffectOfCommands input path.toString .none (fun ctx st₁ st₂ ci => do
     if filter ci then
       let result ← evalAction
         {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env }
-        ci logFileHandle? config
+        ci logFileHandle? config nonterms
       return .some (ci.name, result)
     else
       return .none)
-  if let .some fhandle := logFileHandle? then
-    fhandle.putStrLn ""
+  if let .some fhandle := resultFileHandle? then
     fhandle.putStrLn s!"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}"
 where
   evalAction
     (context : Core.Context) (state : Core.State) (ci : ConstantInfo)
-    (logFileHandle? : Option IO.FS.Handle) (config : EvalTacticConfig) : IO (Array Result) := do
+    (logFileHandle? : Option IO.FS.Handle) (config : EvalTacticConfig)
+    (nonterms : Std.HashSet (RegisteredTactic × Name)) : IO (Array Result) := do
   config.tactics.zipWithIndex.mapM (fun (tactic, idx) => do
     let metaAction : MetaM Result :=
       Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic.toCiTactic ci)
@@ -196,14 +214,62 @@ where
       if let .some fhandle := logFileHandle? then
         fhandle.putStrLn ""
         fhandle.putStrLn s!"Testing tactic {idx} || {ci.name} : {← (Lean.Meta.ppExpr ci.type).run'}"
-      let result ← withCurrHeartbeats <|
-        withReader (fun ctx => { ctx with maxHeartbeats := config.maxHeartbeats * 1000 }) <|
-          Meta.MetaM.run' metaAction
+        fhandle.flush
+      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}"
       if let .some fhandle := logFileHandle? then
         fhandle.putStrLn (toString (← MessageData.format m!"{result}"))
       return result)
     let (result, _) ← coreAction.toIO context state
     return result)
 
+structure EvalTacticOnMathlibConfig where
+  /-- Timeout for each tactic -/
+  maxHeartbeats : Nat           := 65536
+  /-- Tactics to run at each constant declaration -/
+  tactics       : Array RegisteredTactic
+  /-- Folder for saving the result of the evaluation -/
+  resultFolder  : String
+  /--
+    On some problems, certain tactics may go into infinite loops not
+    guarded by `Core.checkMaxHeartbeats`. These instances should be
+    recorded here and avoided (throw error immediately) during evaluation.
+  -/
+  nonterminates : Array (RegisteredTactic × Name)
+
+/--
+  This should be run after `import Mathlib`
+-/
+def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : CoreM Unit := do
+  let mms ← mathlibModules
+  if !(← allMathlibModuleNamesCanBeFilename) then
+    throwError "{decl_name%} :: Some mathlib modules have extra-ordinary names. Evaluation code needs to be changed!"
+  if !(← System.FilePath.isDir config.resultFolder) then
+    IO.FS.createDir config.resultFolder
+  let evaluateFilesHandle ← IO.FS.Handle.mk (config.resultFolder ++ "/evaluateFiles.txt") .write
+  let all ← allHumanTheorems
+  for mm in mms do
+    evaluateFilesHandle.putStrLn mm.toString
+    evaluateFilesHandle.flush
+    let nComps := mm.components.length
+    let paths := (List.range nComps).map (fun i =>
+      String.join <| (mm.components.take (i + 1)).map (fun n => "/" ++ n.toString))
+    for extraDirPath in paths.dropLast do
+      let dirPath := config.resultFolder ++ extraDirPath
+      if !(← System.FilePath.isDir dirPath) then
+        IO.FS.createDir dirPath
+    let .some extraLogPath := paths.getLast?
+      | throwError "evalAtMathlibHumanTheorems :: Module name {mm} has zero components"
+    let logPath := config.resultFolder ++ extraLogPath
+    evalAtModule mm (← initSrcSearchPath) (fun ci => all.contains ci.name)
+      {maxHeartbeats := config.maxHeartbeats, tactics := config.tactics,
+       logFile := .some (logPath ++ ".log"), resultFile := .some (logPath ++ ".result")
+       nonterminates := config.nonterminates}
+
 end EvalAuto

Auto/Translation/LamUtils.lean

@@ -524,7 +524,7 @@ namespace Lam2D
 
   section CheckDefEq
 
-    def checkLamBaseTermSimpNFMap : MetaM Unit :=
+    private def checkLamBaseTermSimpNFMap : MetaM Unit :=
       for (name, e) in lamBaseTermSimpNFList do
         if !(← Meta.isTypeCorrect e) then
           throwError "{e} is not type correct"