From 02b2947b55139d07c4f8924e25d204a3e2ce1a2c Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sun, 5 Jan 2025 02:34:58 -0800 Subject: [PATCH] more test code --- Auto/EvaluateAuto/EnvAnalysis.lean | 6 +++ Auto/EvaluateAuto/NameArr.lean | 12 +++++ Auto/EvaluateAuto/Result.lean | 3 ++ Auto/EvaluateAuto/TestAuto.lean | 17 ++++-- Auto/EvaluateAuto/TestTactics.lean | 86 ++++++++++++++++++++++++++---- Auto/Translation/LamUtils.lean | 2 +- 6 files changed, 110 insertions(+), 16 deletions(-) diff --git a/Auto/EvaluateAuto/EnvAnalysis.lean b/Auto/EvaluateAuto/EnvAnalysis.lean index b1e5ad0..8c17cc4 100644 --- a/Auto/EvaluateAuto/EnvAnalysis.lean +++ b/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 := #[] diff --git a/Auto/EvaluateAuto/NameArr.lean b/Auto/EvaluateAuto/NameArr.lean index 0393e7e..72955d7 100644 --- a/Auto/EvaluateAuto/NameArr.lean +++ b/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. diff --git a/Auto/EvaluateAuto/Result.lean b/Auto/EvaluateAuto/Result.lean index df234f5..717d897 100644 --- a/Auto/EvaluateAuto/Result.lean +++ b/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" diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 177d283..374787b 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/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 diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index e272256..f57fcb9 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/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,16 +187,16 @@ 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 @@ -187,7 +204,8 @@ def evalAtModule 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,9 +214,14 @@ 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}")) @@ -206,4 +229,47 @@ where 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 diff --git a/Auto/Translation/LamUtils.lean b/Auto/Translation/LamUtils.lean index d4a84cb..2b410bd 100644 --- a/Auto/Translation/LamUtils.lean +++ b/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"