From 1d6194355ec468f36aae67c80fa7b32e826e6c29 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Fri, 3 Jan 2025 23:04:18 -0800 Subject: [PATCH] more code for evaluating tactics --- Auto/EvaluateAuto/CommandAnalysis.lean | 67 +------------ Auto/EvaluateAuto/Result.lean | 5 + Auto/EvaluateAuto/TestAuto.lean | 27 ++--- Auto/EvaluateAuto/TestTactics.lean | 134 ++++++++++++++++++++++++- 4 files changed, 151 insertions(+), 82 deletions(-) diff --git a/Auto/EvaluateAuto/CommandAnalysis.lean b/Auto/EvaluateAuto/CommandAnalysis.lean index 0ac5f04..69a34f4 100644 --- a/Auto/EvaluateAuto/CommandAnalysis.lean +++ b/Auto/EvaluateAuto/CommandAnalysis.lean @@ -57,77 +57,16 @@ def runWithEffectOfCommandsCore the procedure is terminated. -/ def runWithEffectOfCommands - (input : String) (fileName : String) (opts : Options := {}) (cnt? : Option Nat) + (input : String) (fileName : String) (cnt? : Option Nat) (action : Context → State → State → ConstantInfo → IO (Option α)) : CoreM (Array α) := do let inputCtx := Parser.mkInputContext input fileName let (header, parserState, messages) ← Parser.parseHeader inputCtx let mut ensuring := #[] if auto.evalAuto.ensureAesop.get (← getOptions) then ensuring := ensuring.push { module := `Aesop } - let (env, messages) ← processHeaderEnsuring header opts messages inputCtx (ensuring := ensuring) - let commandState := Command.mkState env messages opts + let (env, messages) ← processHeaderEnsuring header {} messages inputCtx (ensuring := ensuring) + let commandState := Command.mkState env messages {} (runWithEffectOfCommandsCore cnt? action { inputCtx }).run' { commandState := commandState, parserState := parserState, cmdPos := parserState.pos } -open Tactic in -/-- - Use `runWithEffectOfCommands` to run tactics at the place just before - the command that created the constant `name`\ - Note: Use `initSrcSearchPath` to get SearchPath of source files --/ -def runTacticsAtConstantDeclaration - (name : Name) (searchPath : SearchPath) - (tactics : Array (ConstantInfo → TacticM Unit)) : CoreM (Array Result) := do - if ← isInitializerExecutionEnabled then - throwError "{decl_name%} :: Running this function with execution of `initialize` code enabled is unsafe" - let .some modName ← Lean.findModuleOf? name - | throwError "{decl_name%} :: Cannot find constant {name}" - let .some uri ← Server.documentUriFromModule searchPath modName - | throwError "{decl_name%} :: Cannot find module {modName}" - let .some path := System.Uri.fileUriToPath? uri - | throwError "{decl_name%} :: URI {uri} of {modName} is not a file" - let path := path.normalize - let inputHandle ← IO.FS.Handle.mk path .read - let input ← inputHandle.readToEnd - let results : Array (Array Result) ← runWithEffectOfCommands input path.toString {} (.some 1) (fun ctx st₁ st₂ ci => do - if name != ci.name then - return .none - let metaAction (tactic : ConstantInfo → TacticM Unit) : MetaM Result := - Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic ci) - let coreAction tactic : CoreM Result := (metaAction tactic).run' - let ioAction tactic : IO (Result × _) := - (coreAction tactic).toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env } - let resultsWithState ← tactics.mapM (fun tactic => ioAction tactic) - return .some (resultsWithState.map Prod.fst)) - let #[result] := results - | throwError "{decl_name%} :: Unexpected error" - return result - -open Tactic in -/-- - Effectively, `runTacticsAtConstantDeclaration` at each constant of the module `modName`\ - Note: Use `initSrcSearchPath` to get SearchPath of source files --/ -def runTacticsAtModule - (modName : Name) (searchPath : SearchPath) - (tactics : Array (ConstantInfo → TacticM Unit)) : CoreM (Array Result) := do - let .some uri ← Server.documentUriFromModule searchPath modName - | throwError "{decl_name%} :: Cannot find module {modName}" - let .some path := System.Uri.fileUriToPath? uri - | throwError "{decl_name%} :: URI {uri} of {modName} is not a file" - let path := path.normalize - let inputHandle ← IO.FS.Handle.mk path .read - let input ← inputHandle.readToEnd - let results : Array (Array Result) ← runWithEffectOfCommands input path.toString {} .none (fun ctx st₁ st₂ ci => do - let metaAction (tactic : ConstantInfo → TacticM Unit) : MetaM Result := - Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic ci) - let coreAction tactic : CoreM Result := (metaAction tactic).run' - let ioAction tactic : IO (Result × _) := - (coreAction tactic).toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env } - let resultsWithState ← tactics.mapM (fun tactic => ioAction tactic) - return .some (resultsWithState.map Prod.fst)) - let #[result] := results - | throwError "{decl_name%} :: Unexpected error" - return result - end EvalAuto diff --git a/Auto/EvaluateAuto/Result.lean b/Auto/EvaluateAuto/Result.lean index 2820776..df234f5 100644 --- a/Auto/EvaluateAuto/Result.lean +++ b/Auto/EvaluateAuto/Result.lean @@ -1,6 +1,11 @@ import Lean open Lean +initialize + registerTraceClass `auto.eval.printConfig + registerTraceClass `auto.eval.printProblem + registerTraceClass `auto.eval.printResult + namespace EvalAuto inductive Result diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index a080fba..177d283 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -7,11 +7,6 @@ import Auto.Tactic open Lean Auto -initialize - registerTraceClass `auto.eval.printConfig - registerTraceClass `auto.eval.printProblem - registerTraceClass `auto.eval.printResult - namespace EvalAuto inductive SolverConfig where @@ -27,7 +22,7 @@ instance : ToString SolverConfig where | .smt sn => s!"smt {sn}" | .tptp sn path => s!"tptp {sn} {path}" -structure EvalConfig where +structure EvalAutoConfig where /-- Timeout for Lean code (Lean-auto + native provers) -/ maxHeartbeats : Nat := 65536 /-- Timeout for external provers, i.e. TPTP solvers and SMT solvers -/ @@ -37,15 +32,15 @@ structure EvalConfig where /-- Optional logfile for saving the result of the evaluation -/ logFile : Option String := .none -instance : ToString EvalConfig where - toString : EvalConfig → String +instance : ToString EvalAutoConfig where + toString : EvalAutoConfig → String | ⟨maxHeartbeats, timeout, solverConfig, logFile⟩ => let logFileStr := match logFile with | .some logFile => s!", logFile := {logFile}" | .none => "" s!"\{maxHeartbeats := {maxHeartbeats}, timeout := {timeout}, " ++ - s!"solverConfig = {solverConfig}{logFileStr}}" + s!"solverConfig := {solverConfig}{logFileStr}}" /-- Run `Lean-auto` on `lem.type`, using premises collected from `lem.proof` @@ -105,17 +100,17 @@ def disableAllSolvers (o : Options) : Options := let o := auto.tptp.set o false o -def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := do - let logFileHandle : Option IO.FS.Handle ← config.logFile.mapM (fun fname => IO.FS.Handle.mk fname .write) +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) trace[auto.eval.printConfig] m!"Config = {config}" - if let .some fhandle := logFileHandle then + if let .some fhandle := logFileHandle? then fhandle.putStrLn s!"Config = {config}" let startTime ← IO.monoMsNow let mut results := #[] 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 + if let .some fhandle := logFileHandle? then fhandle.putStrLn "" fhandle.putStrLn s!"Testing || {name} : {← (Lean.Meta.ppExpr ci.type).run'}" let result : Result ← withCurrHeartbeats <| @@ -154,16 +149,16 @@ def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := d runAutoOnConst name trace[auto.eval.printResult] m!"{result}" results := results.push result - if let .some fhandle := logFileHandle then + if let .some fhandle := logFileHandle? then fhandle.putStrLn (toString (← MessageData.format m!"{result}")) - if let .some fhandle := logFileHandle then + if let .some fhandle := logFileHandle? then fhandle.putStrLn "" fhandle.putStrLn s!"Elapsed time: {(← IO.monoMsNow) - startTime} ms" fhandle.putStrLn s!"\nSummary:\n" for ((name, result), idx) in (names.zip results).zipWithIndex do fhandle.putStrLn s!"{idx} {result.concise} {name}" -def runAutoOnNamesFile (cfg : EvalConfig) (fname : String) : CoreM Unit := do +def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := do let names ← NameArray.load fname runAutoOnConsts cfg names diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index 9a6a401..e272256 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -8,9 +8,9 @@ open Lean namespace EvalAuto -section Tactics +open Elab Tactic - open Elab Tactic +section Tactics def useRfl : TacticM Unit := do evalTactic (← `(tactic| intros; rfl)) @@ -74,6 +74,136 @@ section Tactics Syntax.atom synth ")" ] + inductive RegisteredTactic where + | useRfl + | useSimp + | useSimpAll + | useSimpAllWithPremises + | useAesop + | useAesopWithPremises + + instance : ToString RegisteredTactic where + toString : RegisteredTactic → String + | .useRfl => "useRfl" + | .useSimp => "useSimp" + | .useSimpAll => "useSimpAll" + | .useSimpAllWithPremises => "useSimpAllWithPremises" + | .useAesop => "useAesop" + | .useAesopWithPremises => "useAesopWithPremises" + + def RegisteredTactic.toCiTactic : RegisteredTactic → ConstantInfo → TacticM Unit + | .useRfl => fun _ => EvalAuto.useRfl + | .useSimp => fun _ => EvalAuto.useSimp + | .useSimpAll => fun _ => EvalAuto.useSimpAll + | .useSimpAllWithPremises => EvalAuto.useSimpAllWithPremises + | .useAesop => fun _ => EvalAuto.useAesop + | .useAesopWithPremises => EvalAuto.useAesopWithPremises + end Tactics +/-- + Use `runWithEffectOfCommands` to run tactics at the place just before + the command that created the constant `name`\ + Note: Use `initSrcSearchPath` to get SearchPath of source files +-/ +def runTacticsAtConstantDeclaration + (name : Name) (searchPath : SearchPath) + (tactics : Array (ConstantInfo → TacticM Unit)) : CoreM (Array Result) := do + if ← isInitializerExecutionEnabled then + throwError "{decl_name%} :: Running this function with execution of `initialize` code enabled is unsafe" + let .some modName ← Lean.findModuleOf? name + | throwError "{decl_name%} :: Cannot find constant {name}" + let .some uri ← Server.documentUriFromModule searchPath modName + | throwError "{decl_name%} :: Cannot find module {modName}" + let .some path := System.Uri.fileUriToPath? uri + | throwError "{decl_name%} :: URI {uri} of {modName} is not a file" + let path := path.normalize + let inputHandle ← IO.FS.Handle.mk path .read + let input ← inputHandle.readToEnd + let results : Array (Array Result) ← runWithEffectOfCommands input path.toString (.some 1) (fun ctx st₁ st₂ ci => do + if name != ci.name then + return .none + let metaAction (tactic : ConstantInfo → TacticM Unit) : MetaM Result := + Term.TermElabM.run' <| Result.ofTacticOnExpr ci.type (tactic ci) + let coreAction tactic : CoreM Result := (metaAction tactic).run' + let ioAction tactic : IO (Result × _) := + (coreAction tactic).toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env } + let resultsWithState ← tactics.mapM (fun tactic => ioAction tactic) + return .some (resultsWithState.map Prod.fst)) + let #[result] := results + | throwError "{decl_name%} :: Unexpected error" + return result + +structure EvalTacticConfig where + /-- Timeout for each tactic -/ + maxHeartbeats : Nat := 65536 + /-- Tactics to run at each constant declaration -/ + tactics : Array RegisteredTactic + /-- Optional logfile for saving the result of the evaluation -/ + logFile : Option String := .none + +instance : ToString EvalTacticConfig where + toString : EvalTacticConfig → String + | ⟨maxHeartbeats, tactics, logFile⟩ => + let logFileStr := + match logFile with + | .some logFile => s!", logFile := {logFile}" + | .none => "" + s!"\{maxHeartbeats := {maxHeartbeats}, tactics := {tactics}{logFileStr}}" + +/-- + Effectively `runTacticsAtConstantDeclaration` at each constant in `modName` which satisfies `filter`\ + Note: Use `initSrcSearchPath` to get SearchPath of source files +-/ +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) + trace[auto.eval.printConfig] m!"Config = {config}" + if let .some fhandle := logFileHandle? then + fhandle.putStrLn s!"Config = {config}" + let .some uri ← Server.documentUriFromModule searchPath modName + | throwError "{decl_name%} :: Cannot find module {modName}" + let .some path := System.Uri.fileUriToPath? uri + | throwError "{decl_name%} :: URI {uri} of {modName} is not a file" + let path := path.normalize + let inputHandle ← IO.FS.Handle.mk path .read + let input ← inputHandle.readToEnd + let startTime ← IO.monoMsNow + 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 + return .some (ci.name, result) + else + return .none) + if let .some fhandle := logFileHandle? then + fhandle.putStrLn "" + 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 + 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 + 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'}" + let result ← 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) + end EvalAuto