From e3a6bbaeda6bf728c7e73b2de766efbf592bbf2f Mon Sep 17 00:00:00 2001 From: PratherConid Date: Thu, 2 Jan 2025 12:34:32 +0800 Subject: [PATCH 01/17] add aesop tactic --- Auto/EvaluateAuto/TestCode.lean | 59 ++++++++++++++++++++++++++++++--- 1 file changed, 54 insertions(+), 5 deletions(-) diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean index e5ec990..454fca1 100644 --- a/Auto/EvaluateAuto/TestCode.lean +++ b/Auto/EvaluateAuto/TestCode.lean @@ -164,13 +164,62 @@ def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := d for ((name, result), idx) in (names.zip results).zipWithIndex do fhandle.putStrLn s!"{idx} {result.concise} {name}" -def namesFileEval (cfg : EvalConfig) (fname : String) : CoreM Unit := do +def runAutoOnNamesFile (cfg : EvalConfig) (fname : String) : CoreM Unit := do let names ← NameArray.load fname runAutoOnConsts cfg names -def randEval (cfg : EvalConfig) (n : Nat) : CoreM Unit := do - let hthms ← allHumanTheorems - let asel ← Array.randPick hthms n - runAutoOnConsts cfg asel +open Elab Tactic +def useRfl : TacticM Unit := do evalTactic (← `(tactic| intros; rfl)) + +def useSimp : TacticM Unit := do evalTactic (← `(tactic| intros; simp)) + +def useSimpAll : TacticM Unit := do evalTactic (← `(tactic| intros; simp_all)) + +def useSimpAllWithPremises (ci : ConstantInfo) : TacticM Unit := do + let .some proof := ci.value? + | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" + let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => + return !(← Name.onlyLogicInType name)) + let usedThmTerms : Array Term := usedThmNames.map (fun name => ⟨mkIdent name⟩) + evalTactic (← `(tactic| intros; simp_all [$[$usedThmTerms:term],*])) + +private def mkAesopStx (addClauses : Array Syntax) : TSyntax `tactic := + let synth : SourceInfo := SourceInfo.synthetic default default false + TSyntax.mk ( + Syntax.node synth `Aesop.Frontend.Parser.aesopTactic + #[Syntax.atom synth "aesop", Syntax.node synth `null addClauses] + ) + +-- Only guaranteed to work for `aesop @ Lean v4.14.0` +def useAesop : TacticM Unit := evalTactic (mkAesopStx #[]) + +-- Only guaranteed to work for `aesop @ Lean v4.14.0` +def useAesopWithPremises (ci : ConstantInfo) : TacticM Unit := do + let .some proof := ci.value? + | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" + let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => + return !(← Name.onlyLogicInType name)) + let usedThmIdents := usedThmNames.map Lean.mkIdent + let addClauses := usedThmIdents.map mkAddIdentStx + let aesopStx := mkAesopStx addClauses + evalTactic aesopStx +where + synth : SourceInfo := SourceInfo.synthetic default default false + mkAddIdentStx (ident : Ident) : Syntax := + Syntax.node synth `Aesop.Frontend.Parser.«tactic_clause(Add_)» + #[Syntax.atom synth "(", Syntax.atom synth "add", + Syntax.node synth `null + #[Syntax.node synth `Aesop.Frontend.Parser.rule_expr___ + #[Syntax.node synth `Aesop.Frontend.Parser.feature_ + #[Syntax.node synth `Aesop.Frontend.Parser.phaseUnsafe + #[Syntax.atom synth "unsafe"] + ], + Syntax.node synth `Aesop.Frontend.Parser.rule_expr_ + #[Lean.Syntax.node synth `Aesop.Frontend.Parser.featIdent #[ident]] + ] + ], + Syntax.atom synth ")" + ] + end EvalAuto From 792a3d3929571628df624808989f7eae410cd19b Mon Sep 17 00:00:00 2001 From: PratherConid Date: Fri, 3 Jan 2025 02:02:12 -0800 Subject: [PATCH 02/17] support multiple tactics --- Auto/EvaluateAuto/CommandAnalysis.lean | 132 +++++++++++++++++++------ Auto/EvaluateAuto/TestCode.lean | 54 ---------- 2 files changed, 104 insertions(+), 82 deletions(-) diff --git a/Auto/EvaluateAuto/CommandAnalysis.lean b/Auto/EvaluateAuto/CommandAnalysis.lean index 019fd79..cf17fd4 100644 --- a/Auto/EvaluateAuto/CommandAnalysis.lean +++ b/Auto/EvaluateAuto/CommandAnalysis.lean @@ -1,5 +1,6 @@ import Lean import Auto.EvaluateAuto.EnvAnalysis +import Auto.EvaluateAuto.ConstAnalysis import Auto.EvaluateAuto.Result open Lean @@ -47,13 +48,36 @@ def runWithEffectOfCommands (runWithEffectOfCommandsCore cnt? action { inputCtx }).run' { commandState := commandState, parserState := parserState, cmdPos := parserState.pos } +open Elab Tactic in +/-- + Run `tactic` on a metavariable with type `e` and obtain the result +-/ +def Result.ofTacticOnExpr (e : Expr) (tactic : TacticM Unit) : TermElabM Result := do + let .mvar mid ← Meta.mkFreshExprMVar e + | throwError "{decl_name%} : Unexpected error" + let result : List MVarId ⊕ Exception ← tryCatchRuntimeEx + (do let goals ← Term.TermElabM.run' (Tactic.run mid tactic) {}; return .inl goals) + (fun e => return .inr e) + match result with + | .inl goals => + if goals.length >= 1 then + return .subGoals + let proof ← instantiateMVars (.mvar mid) + match Kernel.check (← getEnv) {} proof with + | Except.ok autoProofType => + match Kernel.isDefEq (← getEnv) {} autoProofType e with + | Except.ok true => return .success + | _ => return .typeUnequal + | Except.error _ => return .typeCheckFail + | .inr e => return (.exception e) + open Elab Tactic in /-- Note: Use `initSrcSearchPath` to get SearchPath of Lean4's builtin source files -/ -def runTacticAtConstantDeclaration +def runTacticsAtConstantDeclaration (name : Name) (searchPath : SearchPath) - (tactic : ConstantInfo → TacticM Unit) : CoreM Result := do + (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 @@ -65,34 +89,86 @@ def runTacticAtConstantDeclaration let path := path.normalize let inputHandle ← IO.FS.Handle.mk path .read let input ← inputHandle.readToEnd - let results ← runWithEffectOfCommands input path.toString {} (.some 1) (fun ctx st₁ st₂ ci => - let metaAction : MetaM (Option Result) := do - if ci.name != name then - return .none - let .mvar mid ← Meta.mkFreshExprMVar ci.type - | throwError "{decl_name%} :: Unexpected error" - let result : List MVarId ⊕ Exception ← - tryCatchRuntimeEx - (do let goals ← Term.TermElabM.run' (Tactic.run mid (tactic ci)) {}; return .inl goals) - (fun e => return .inr e) - match result with - | .inl goals => - if goals.length >= 1 then - return .some .subGoals - let proof ← instantiateMVars (.mvar mid) - match Kernel.check (← getEnv) {} proof with - | Except.ok autoProofType => - match Kernel.isDefEq (← getEnv) {} autoProofType ci.type with - | Except.ok true => return .some .success - | _ => return .some .typeUnequal - | Except.error _ => return .some .typeCheckFail - | .inr e => return .some (.exception e) - let coreAction : CoreM (Option Result) := metaAction.run' - let ioAction : IO (Option Result × _) := coreAction.toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env } - do - return (← ioAction).fst) + 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 +section Tactics + + open Elab Tactic + + def useRfl : TacticM Unit := do evalTactic (← `(tactic| intros; rfl)) + + def useSimp : TacticM Unit := do evalTactic (← `(tactic| intros; simp)) + + def useSimpAll : TacticM Unit := do evalTactic (← `(tactic| intros; simp_all)) + + def useSimpAllWithPremises (ci : ConstantInfo) : TacticM Unit := do + let .some proof := ci.value? + | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" + let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => + return !(← Name.onlyLogicInType name)) + let usedThmTerms : Array Term := usedThmNames.map (fun name => ⟨mkIdent name⟩) + evalTactic (← `(tactic| intros; simp_all [$[$usedThmTerms:term],*])) + + private def mkAesopStx (addClauses : Array Syntax) : TSyntax `tactic := + let synth : SourceInfo := SourceInfo.synthetic default default false + TSyntax.mk ( + Syntax.node synth `Aesop.Frontend.Parser.aesopTactic + #[Syntax.atom synth "aesop", Syntax.node synth `null addClauses] + ) + + /-- + Tactic sequence: `intros; aesop` + Only guaranteed to work for `aesop @ Lean v4.14.0` + -/ + def useAesop : TacticM Unit := do + let aesopStx := mkAesopStx #[] + let stx ← `(tactic|intros; $aesopStx) + evalTactic stx + + /-- + Tactic sequence: `intros; aesop (add unsafe premise₁) ⋯ (add unsafe premiseₙ)` + Only guaranteed to work for `aesop @ Lean v4.14.0` + -/ + def useAesopWithPremises (ci : ConstantInfo) : TacticM Unit := do + let .some proof := ci.value? + | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" + let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => + return !(← Name.onlyLogicInType name)) + let usedThmIdents := usedThmNames.map Lean.mkIdent + let addClauses := usedThmIdents.map mkAddIdentStx + let aesopStx := mkAesopStx addClauses + let stx ← `(tactic|intros; $aesopStx) + evalTactic stx + where + synth : SourceInfo := SourceInfo.synthetic default default false + mkAddIdentStx (ident : Ident) : Syntax := + Syntax.node synth `Aesop.Frontend.Parser.«tactic_clause(Add_)» + #[Syntax.atom synth "(", Syntax.atom synth "add", + Syntax.node synth `null + #[Syntax.node synth `Aesop.Frontend.Parser.rule_expr___ + #[Syntax.node synth `Aesop.Frontend.Parser.feature_ + #[Syntax.node synth `Aesop.Frontend.Parser.phaseUnsafe + #[Syntax.atom synth "unsafe"] + ], + Syntax.node synth `Aesop.Frontend.Parser.rule_expr_ + #[Lean.Syntax.node synth `Aesop.Frontend.Parser.featIdent #[ident]] + ] + ], + Syntax.atom synth ")" + ] + +end Tactics + end EvalAuto diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean index 454fca1..82eb6f0 100644 --- a/Auto/EvaluateAuto/TestCode.lean +++ b/Auto/EvaluateAuto/TestCode.lean @@ -168,58 +168,4 @@ def runAutoOnNamesFile (cfg : EvalConfig) (fname : String) : CoreM Unit := do let names ← NameArray.load fname runAutoOnConsts cfg names -open Elab Tactic -def useRfl : TacticM Unit := do evalTactic (← `(tactic| intros; rfl)) - -def useSimp : TacticM Unit := do evalTactic (← `(tactic| intros; simp)) - -def useSimpAll : TacticM Unit := do evalTactic (← `(tactic| intros; simp_all)) - -def useSimpAllWithPremises (ci : ConstantInfo) : TacticM Unit := do - let .some proof := ci.value? - | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" - let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => - return !(← Name.onlyLogicInType name)) - let usedThmTerms : Array Term := usedThmNames.map (fun name => ⟨mkIdent name⟩) - evalTactic (← `(tactic| intros; simp_all [$[$usedThmTerms:term],*])) - -private def mkAesopStx (addClauses : Array Syntax) : TSyntax `tactic := - let synth : SourceInfo := SourceInfo.synthetic default default false - TSyntax.mk ( - Syntax.node synth `Aesop.Frontend.Parser.aesopTactic - #[Syntax.atom synth "aesop", Syntax.node synth `null addClauses] - ) - --- Only guaranteed to work for `aesop @ Lean v4.14.0` -def useAesop : TacticM Unit := evalTactic (mkAesopStx #[]) - --- Only guaranteed to work for `aesop @ Lean v4.14.0` -def useAesopWithPremises (ci : ConstantInfo) : TacticM Unit := do - let .some proof := ci.value? - | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" - let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => - return !(← Name.onlyLogicInType name)) - let usedThmIdents := usedThmNames.map Lean.mkIdent - let addClauses := usedThmIdents.map mkAddIdentStx - let aesopStx := mkAesopStx addClauses - evalTactic aesopStx -where - synth : SourceInfo := SourceInfo.synthetic default default false - mkAddIdentStx (ident : Ident) : Syntax := - Syntax.node synth `Aesop.Frontend.Parser.«tactic_clause(Add_)» - #[Syntax.atom synth "(", Syntax.atom synth "add", - Syntax.node synth `null - #[Syntax.node synth `Aesop.Frontend.Parser.rule_expr___ - #[Syntax.node synth `Aesop.Frontend.Parser.feature_ - #[Syntax.node synth `Aesop.Frontend.Parser.phaseUnsafe - #[Syntax.atom synth "unsafe"] - ], - Syntax.node synth `Aesop.Frontend.Parser.rule_expr_ - #[Lean.Syntax.node synth `Aesop.Frontend.Parser.featIdent #[ident]] - ] - ], - Syntax.atom synth ")" - ] - - end EvalAuto From 7f07d6ce08b446fd0b24f1e325b26b47f0a20076 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Fri, 3 Jan 2025 14:40:13 -0800 Subject: [PATCH 03/17] refactor --- Auto/EvaluateAuto/CommandAnalysis.lean | 147 +++++++----------- Auto/EvaluateAuto/Result.lean | 24 +++ .../{TestCode.lean => TestAuto.lean} | 1 - Auto/EvaluateAuto/TestTactics.lean | 79 ++++++++++ 4 files changed, 156 insertions(+), 95 deletions(-) rename Auto/EvaluateAuto/{TestCode.lean => TestAuto.lean} (99%) create mode 100644 Auto/EvaluateAuto/TestTactics.lean diff --git a/Auto/EvaluateAuto/CommandAnalysis.lean b/Auto/EvaluateAuto/CommandAnalysis.lean index cf17fd4..0ac5f04 100644 --- a/Auto/EvaluateAuto/CommandAnalysis.lean +++ b/Auto/EvaluateAuto/CommandAnalysis.lean @@ -4,9 +4,27 @@ import Auto.EvaluateAuto.ConstAnalysis import Auto.EvaluateAuto.Result open Lean +register_option auto.evalAuto.ensureAesop : Bool := { + defValue := false + descr := "Enable/Disable enforcement of importing `aesop`" +} + namespace EvalAuto open Elab Frontend + +def processHeaderEnsuring (header : Syntax) (opts : Options) (messages : MessageLog) + (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (leakEnv := false) (ensuring : Array Import := #[]) + : IO (Environment × MessageLog) := do + try + let env ← importModules (leakEnv := leakEnv) (headerToImports header ++ ensuring) opts trustLevel + pure (env, messages) + catch e => + let env ← mkEmptyEnvironment + let spos := header.getPos?.getD 0 + let pos := inputCtx.fileMap.toPosition spos + pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos }) + def runWithEffectOfCommandsCore (cnt? : Option Nat) (action : Context → State → State → ConstantInfo → IO (Option α)) : FrontendM (Array α) := do @@ -40,40 +58,22 @@ def runWithEffectOfCommandsCore -/ def runWithEffectOfCommands (input : String) (fileName : String) (opts : Options := {}) (cnt? : Option Nat) - (action : Context → State → State → ConstantInfo → IO (Option α)) : IO (Array α) := do + (action : Context → State → State → ConstantInfo → IO (Option α)) : CoreM (Array α) := do let inputCtx := Parser.mkInputContext input fileName let (header, parserState, messages) ← Parser.parseHeader inputCtx - let (env, messages) ← processHeader header opts messages 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 (runWithEffectOfCommandsCore cnt? action { inputCtx }).run' { commandState := commandState, parserState := parserState, cmdPos := parserState.pos } -open Elab Tactic in +open Tactic in /-- - Run `tactic` on a metavariable with type `e` and obtain the result --/ -def Result.ofTacticOnExpr (e : Expr) (tactic : TacticM Unit) : TermElabM Result := do - let .mvar mid ← Meta.mkFreshExprMVar e - | throwError "{decl_name%} : Unexpected error" - let result : List MVarId ⊕ Exception ← tryCatchRuntimeEx - (do let goals ← Term.TermElabM.run' (Tactic.run mid tactic) {}; return .inl goals) - (fun e => return .inr e) - match result with - | .inl goals => - if goals.length >= 1 then - return .subGoals - let proof ← instantiateMVars (.mvar mid) - match Kernel.check (← getEnv) {} proof with - | Except.ok autoProofType => - match Kernel.isDefEq (← getEnv) {} autoProofType e with - | Except.ok true => return .success - | _ => return .typeUnequal - | Except.error _ => return .typeCheckFail - | .inr e => return (.exception e) - -open Elab Tactic in -/-- - Note: Use `initSrcSearchPath` to get SearchPath of Lean4's builtin source files + 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) @@ -103,72 +103,31 @@ def runTacticsAtConstantDeclaration | throwError "{decl_name%} :: Unexpected error" return result -section Tactics - - open Elab Tactic - - def useRfl : TacticM Unit := do evalTactic (← `(tactic| intros; rfl)) - - def useSimp : TacticM Unit := do evalTactic (← `(tactic| intros; simp)) - - def useSimpAll : TacticM Unit := do evalTactic (← `(tactic| intros; simp_all)) - - def useSimpAllWithPremises (ci : ConstantInfo) : TacticM Unit := do - let .some proof := ci.value? - | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" - let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => - return !(← Name.onlyLogicInType name)) - let usedThmTerms : Array Term := usedThmNames.map (fun name => ⟨mkIdent name⟩) - evalTactic (← `(tactic| intros; simp_all [$[$usedThmTerms:term],*])) - - private def mkAesopStx (addClauses : Array Syntax) : TSyntax `tactic := - let synth : SourceInfo := SourceInfo.synthetic default default false - TSyntax.mk ( - Syntax.node synth `Aesop.Frontend.Parser.aesopTactic - #[Syntax.atom synth "aesop", Syntax.node synth `null addClauses] - ) - - /-- - Tactic sequence: `intros; aesop` - Only guaranteed to work for `aesop @ Lean v4.14.0` - -/ - def useAesop : TacticM Unit := do - let aesopStx := mkAesopStx #[] - let stx ← `(tactic|intros; $aesopStx) - evalTactic stx - - /-- - Tactic sequence: `intros; aesop (add unsafe premise₁) ⋯ (add unsafe premiseₙ)` - Only guaranteed to work for `aesop @ Lean v4.14.0` - -/ - def useAesopWithPremises (ci : ConstantInfo) : TacticM Unit := do - let .some proof := ci.value? - | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" - let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => - return !(← Name.onlyLogicInType name)) - let usedThmIdents := usedThmNames.map Lean.mkIdent - let addClauses := usedThmIdents.map mkAddIdentStx - let aesopStx := mkAesopStx addClauses - let stx ← `(tactic|intros; $aesopStx) - evalTactic stx - where - synth : SourceInfo := SourceInfo.synthetic default default false - mkAddIdentStx (ident : Ident) : Syntax := - Syntax.node synth `Aesop.Frontend.Parser.«tactic_clause(Add_)» - #[Syntax.atom synth "(", Syntax.atom synth "add", - Syntax.node synth `null - #[Syntax.node synth `Aesop.Frontend.Parser.rule_expr___ - #[Syntax.node synth `Aesop.Frontend.Parser.feature_ - #[Syntax.node synth `Aesop.Frontend.Parser.phaseUnsafe - #[Syntax.atom synth "unsafe"] - ], - Syntax.node synth `Aesop.Frontend.Parser.rule_expr_ - #[Lean.Syntax.node synth `Aesop.Frontend.Parser.featIdent #[ident]] - ] - ], - Syntax.atom synth ")" - ] - -end Tactics +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 126fbd9..2820776 100644 --- a/Auto/EvaluateAuto/Result.lean +++ b/Auto/EvaluateAuto/Result.lean @@ -29,4 +29,28 @@ def Result.concise : Result → String | .subGoals => "G" | .exception _ => "E" + +open Elab Tactic in +/-- + Run `tactic` on a metavariable with type `e` and obtain the result +-/ +def Result.ofTacticOnExpr (e : Expr) (tactic : TacticM Unit) : TermElabM Result := do + let .mvar mid ← Meta.mkFreshExprMVar e + | throwError "{decl_name%} : Unexpected error" + let result : List MVarId ⊕ Exception ← tryCatchRuntimeEx + (do let goals ← Term.TermElabM.run' (Tactic.run mid tactic) {}; return .inl goals) + (fun e => return .inr e) + match result with + | .inl goals => + if goals.length >= 1 then + return .subGoals + let proof ← instantiateMVars (.mvar mid) + match Kernel.check (← getEnv) {} proof with + | Except.ok autoProofType => + match Kernel.isDefEq (← getEnv) {} autoProofType e with + | Except.ok true => return .success + | _ => return .typeUnequal + | Except.error _ => return .typeCheckFail + | .inr e => return (.exception e) + end EvalAuto diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestAuto.lean similarity index 99% rename from Auto/EvaluateAuto/TestCode.lean rename to Auto/EvaluateAuto/TestAuto.lean index 82eb6f0..a080fba 100644 --- a/Auto/EvaluateAuto/TestCode.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -3,7 +3,6 @@ import Auto.EvaluateAuto.Result import Auto.EvaluateAuto.ConstAnalysis import Auto.EvaluateAuto.EnvAnalysis import Auto.EvaluateAuto.NameArr -import Auto.EvaluateAuto.CommandAnalysis import Auto.Tactic open Lean Auto diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean new file mode 100644 index 0000000..9a6a401 --- /dev/null +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -0,0 +1,79 @@ +import Lean +import Auto.EvaluateAuto.Result +import Auto.EvaluateAuto.ConstAnalysis +import Auto.EvaluateAuto.EnvAnalysis +import Auto.EvaluateAuto.NameArr +import Auto.EvaluateAuto.CommandAnalysis +open Lean + +namespace EvalAuto + +section Tactics + + open Elab Tactic + + def useRfl : TacticM Unit := do evalTactic (← `(tactic| intros; rfl)) + + def useSimp : TacticM Unit := do evalTactic (← `(tactic| intros; simp)) + + def useSimpAll : TacticM Unit := do evalTactic (← `(tactic| intros; simp_all)) + + def useSimpAllWithPremises (ci : ConstantInfo) : TacticM Unit := do + let .some proof := ci.value? + | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" + let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => + return !(← Name.onlyLogicInType name)) + let usedThmTerms : Array Term := usedThmNames.map (fun name => ⟨mkIdent name⟩) + evalTactic (← `(tactic| intros; simp_all [$[$usedThmTerms:term],*])) + + private def mkAesopStx (addClauses : Array Syntax) : TSyntax `tactic := + let synth : SourceInfo := SourceInfo.synthetic default default false + TSyntax.mk ( + Syntax.node synth `Aesop.Frontend.Parser.aesopTactic + #[Syntax.atom synth "aesop", Syntax.node synth `null addClauses] + ) + + /-- + Tactic sequence: `intros; aesop` + Only guaranteed to work for `aesop @ Lean v4.14.0` + -/ + def useAesop : TacticM Unit := do + let aesopStx := mkAesopStx #[] + let stx ← `(tactic|intros; $aesopStx) + evalTactic stx + + /-- + Tactic sequence: `intros; aesop (add unsafe premise₁) ⋯ (add unsafe premiseₙ)` + Only guaranteed to work for `aesop @ Lean v4.14.0` + -/ + def useAesopWithPremises (ci : ConstantInfo) : TacticM Unit := do + let .some proof := ci.value? + | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" + let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => + return !(← Name.onlyLogicInType name)) + let usedThmIdents := usedThmNames.map Lean.mkIdent + let addClauses := usedThmIdents.map mkAddIdentStx + let aesopStx := mkAesopStx addClauses + let stx ← `(tactic|intros; $aesopStx) + evalTactic stx + where + synth : SourceInfo := SourceInfo.synthetic default default false + mkAddIdentStx (ident : Ident) : Syntax := + Syntax.node synth `Aesop.Frontend.Parser.«tactic_clause(Add_)» + #[Syntax.atom synth "(", Syntax.atom synth "add", + Syntax.node synth `null + #[Syntax.node synth `Aesop.Frontend.Parser.rule_expr___ + #[Syntax.node synth `Aesop.Frontend.Parser.feature_ + #[Syntax.node synth `Aesop.Frontend.Parser.phaseUnsafe + #[Syntax.atom synth "unsafe"] + ], + Syntax.node synth `Aesop.Frontend.Parser.rule_expr_ + #[Lean.Syntax.node synth `Aesop.Frontend.Parser.featIdent #[ident]] + ] + ], + Syntax.atom synth ")" + ] + +end Tactics + +end EvalAuto From 1d6194355ec468f36aae67c80fa7b32e826e6c29 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Fri, 3 Jan 2025 23:04:18 -0800 Subject: [PATCH 04/17] 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 From 30441a8bc339230d3592acf11cbdd3dee7b60de1 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sat, 4 Jan 2025 00:50:58 -0800 Subject: [PATCH 05/17] bump to v4.15.0 --- Auto/Lib/MetaExtra.lean | 14 ++++++++++++++ Auto/Lib/MetaState.lean | 19 ++++++++++++------- lean-toolchain | 2 +- 3 files changed, 27 insertions(+), 8 deletions(-) diff --git a/Auto/Lib/MetaExtra.lean b/Auto/Lib/MetaExtra.lean index c0d5893..3958fa9 100644 --- a/Auto/Lib/MetaExtra.lean +++ b/Auto/Lib/MetaExtra.lean @@ -23,6 +23,8 @@ partial def Meta.normalizeNondependentForall (e : Expr) : MetaM Expr := do let e' ← whnfNondependentForall e match e' with | .forallE name ty body bi => + if body.hasLooseBVar 0 then + return e let ty' ← normalizeNondependentForall ty let body' ← normalizeNondependentForall body return .forallE name ty' body' bi @@ -142,4 +144,16 @@ def Meta.exToExcept (x : MetaM α) : MetaM (Except Exception α) := def Meta.runtimeExToExcept (x : MetaM α) : MetaM (Except Exception α) := tryCatchRuntimeEx (do let v ← x; return .ok v) (fun e => return .error e) +/-- + Workaround for modifying the `lctx` field of `Meta.Context` +-/ +def Meta.Context.modifyLCtx (ctx : Context) (lctx : LocalContext) : CoreM Context := + MetaM.run' (withLCtx' lctx read) ctx + +/-- + Workaround for modifying the `localInstances` field of `Meta.Context` +-/ +def Meta.Context.modifyLocalInstances (ctx : Context) (localInsts : LocalInstances) : CoreM Context := + MetaM.run' (withLCtx ctx.lctx localInsts read) ctx + end Auto diff --git a/Auto/Lib/MetaState.lean b/Auto/Lib/MetaState.lean index efc26b5..736c53a 100644 --- a/Auto/Lib/MetaState.lean +++ b/Auto/Lib/MetaState.lean @@ -76,7 +76,7 @@ private def runWithFVars (lctx : LocalContext) (fvarids : Array FVarId) (k : Met | .ldecl _ fvarId userName type value nonDep kind => newlctx := newlctx.mkLetDecl fvarId userName type value nonDep kind | .none => throwError "{decl_name%} :: Unknown free variable {Expr.fvar fid}" - withReader (fun ctx => {ctx with lctx := newlctx}) k + Meta.withLCtx' newlctx k private def runWithIntroducedFVarsImp (m : MetaStateM (Array FVarId × α)) (k : α → MetaM β) : MetaM β := do let s ← get @@ -116,19 +116,22 @@ def mkLocalDecl (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := LocalDeclKind.default) : MetaStateM Unit := do let ctx ← getToContext let lctx := ctx.lctx - setToContext ({ctx with lctx := lctx.mkLocalDecl fvarId userName type bi kind}) + let newCtx ← Meta.Context.modifyLCtx ctx (lctx.mkLocalDecl fvarId userName type bi kind) + setToContext newCtx def mkLetDecl (fvarId : FVarId) (userName : Name) (type value : Expr) (nonDep : Bool := false) (kind : LocalDeclKind := default) : MetaStateM Unit := do let ctx ← getToContext let lctx := ctx.lctx - setToContext ({ctx with lctx := lctx.mkLetDecl fvarId userName type value nonDep kind}) + let newCtx ← Meta.Context.modifyLCtx ctx (lctx.mkLetDecl fvarId userName type value nonDep kind) + setToContext newCtx private def withNewLocalInstance (className : Name) (fvar : Expr) : MetaStateM Unit := do let localDecl ← runMetaM <| Meta.getFVarLocalDecl fvar if !localDecl.isImplementationDetail then let ctx ← getToContext - setToContext ({ ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } }) + let newCtx ← Meta.Context.modifyLocalInstances ctx (ctx.localInstances.push { className := className, fvar := fvar }) + setToContext newCtx private def withNewFVar (fvar fvarType : Expr) : MetaStateM Unit := do if let some c ← runMetaM <| Meta.isClass? fvarType then @@ -149,10 +152,12 @@ def withLetDecl (n : Name) (type : Expr) (val : Expr) (kind : LocalDeclKind) : M return fvarId def withTemporaryLCtx [MonadLiftT MetaStateM n] [Monad n] (lctx : LocalContext) (localInsts : LocalInstances) (k : n α) : n α := do - let initlctx ← getToContext - MetaState.setToContext {initlctx with lctx := lctx, localInstances := localInsts} + let initCtx ← getToContext + let newCtx ← (Meta.Context.modifyLCtx initCtx lctx : MetaStateM _) + let newCtx ← (Meta.Context.modifyLocalInstances newCtx localInsts : MetaStateM _) + MetaState.setToContext newCtx let ret ← k - MetaState.setToContext initlctx + MetaState.setToContext initCtx return ret end Auto.MetaState diff --git a/lean-toolchain b/lean-toolchain index 401bc14..f8e93da 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 \ No newline at end of file +leanprover/lean4:v4.15.0 \ No newline at end of file From 02b2947b55139d07c4f8924e25d204a3e2ce1a2c Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sun, 5 Jan 2025 02:34:58 -0800 Subject: [PATCH 06/17] 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" From 26f82a7a16fcd4a27b98af7ae81524cfc0760bcb Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sun, 5 Jan 2025 16:36:06 -0800 Subject: [PATCH 07/17] fix aesop invocation --- Auto/EvaluateAuto/TestTactics.lean | 50 ++++++++++++++++++------------ 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index f57fcb9..6e56d2a 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -26,19 +26,28 @@ section Tactics let usedThmTerms : Array Term := usedThmNames.map (fun name => ⟨mkIdent name⟩) evalTactic (← `(tactic| intros; simp_all [$[$usedThmTerms:term],*])) - private def mkAesopStx (addClauses : Array Syntax) : TSyntax `tactic := + private def mkAesopConfigStx (subHeartbeats : Nat) : CoreM Syntax := do + let synth : SourceInfo := SourceInfo.synthetic default default false + let shStx := Syntax.node synth `num #[Syntax.atom synth (toString subHeartbeats)] + let shStx := TSyntax.mk shStx + let stx ← `(term | { maxSimpHeartbeats := $shStx, maxRuleHeartbeats := $shStx, maxUnfoldHeartbeats := $shStx }) + return Syntax.node synth `Aesop.Frontend.Parser.«tactic_clause(Config:=_)» + #[Syntax.atom synth "(", Syntax.atom synth "config", Syntax.atom synth ":=", stx] + + private def mkAesopStx (tacticClauses : Array Syntax) : TSyntax `tactic := let synth : SourceInfo := SourceInfo.synthetic default default false TSyntax.mk ( Syntax.node synth `Aesop.Frontend.Parser.aesopTactic - #[Syntax.atom synth "aesop", Syntax.node synth `null addClauses] + #[Syntax.atom synth "aesop", Syntax.node synth `null tacticClauses] ) /-- Tactic sequence: `intros; aesop` Only guaranteed to work for `aesop @ Lean v4.14.0` -/ - def useAesop : TacticM Unit := do - let aesopStx := mkAesopStx #[] + def useAesop (subHeartbeats : Nat) : TacticM Unit := do + let configStx ← mkAesopConfigStx subHeartbeats + let aesopStx := mkAesopStx #[configStx] let stx ← `(tactic|intros; $aesopStx) evalTactic stx @@ -46,14 +55,15 @@ section Tactics Tactic sequence: `intros; aesop (add unsafe premise₁) ⋯ (add unsafe premiseₙ)` Only guaranteed to work for `aesop @ Lean v4.14.0` -/ - def useAesopWithPremises (ci : ConstantInfo) : TacticM Unit := do + def useAesopWithPremises (subHeartbeats : Nat) (ci : ConstantInfo) : TacticM Unit := do let .some proof := ci.value? | throwError "{decl_name%} :: ConstantInfo of {ci.name} has no value" let usedThmNames ← (← Expr.getUsedTheorems proof).filterM (fun name => return !(← Name.onlyLogicInType name)) let usedThmIdents := usedThmNames.map Lean.mkIdent + let configClause ← mkAesopConfigStx subHeartbeats let addClauses := usedThmIdents.map mkAddIdentStx - let aesopStx := mkAesopStx addClauses + let aesopStx := mkAesopStx (#[configClause] ++ addClauses) let stx ← `(tactic|intros; $aesopStx) evalTactic stx where @@ -79,26 +89,26 @@ section Tactics | useSimp | useSimpAll | useSimpAllWithPremises - | useAesop - | useAesopWithPremises + | useAesop (subHeartbeats : Nat) + | useAesopWithPremises (subHeartbeats : Nat) deriving BEq, Hashable instance : ToString RegisteredTactic where toString : RegisteredTactic → String - | .useRfl => "useRfl" - | .useSimp => "useSimp" - | .useSimpAll => "useSimpAll" - | .useSimpAllWithPremises => "useSimpAllWithPremises" - | .useAesop => "useAesop" - | .useAesopWithPremises => "useAesopWithPremises" + | .useRfl => "useRfl" + | .useSimp => "useSimp" + | .useSimpAll => "useSimpAll" + | .useSimpAllWithPremises => "useSimpAllWithPremises" + | .useAesop sh => s!"useAesop {sh}" + | .useAesopWithPremises sh => s!"useAesopWithPremises {sh}" 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 + | .useRfl => fun _ => EvalAuto.useRfl + | .useSimp => fun _ => EvalAuto.useSimp + | .useSimpAll => fun _ => EvalAuto.useSimpAll + | .useSimpAllWithPremises => EvalAuto.useSimpAllWithPremises + | .useAesop sh => fun _ => EvalAuto.useAesop sh + | .useAesopWithPremises sh => EvalAuto.useAesopWithPremises sh end Tactics From beca432ca2dae9cd3688e5957bf8ab4d125cf71f Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sun, 5 Jan 2025 19:08:22 -0800 Subject: [PATCH 08/17] tactic test code mostly done --- Auto/EvaluateAuto/ConstAnalysis.lean | 9 +++++ Auto/EvaluateAuto/TestTactics.lean | 56 ++++++++++++++++++++++++---- 2 files changed, 58 insertions(+), 7 deletions(-) diff --git a/Auto/EvaluateAuto/ConstAnalysis.lean b/Auto/EvaluateAuto/ConstAnalysis.lean index c732453..1e1c926 100644 --- a/Auto/EvaluateAuto/ConstAnalysis.lean +++ b/Auto/EvaluateAuto/ConstAnalysis.lean @@ -11,6 +11,15 @@ def Name.getConstsOfModule (module : Name) : CoreM (Array Name) := do let (mod, _) ← readModuleData mFile return mod.constNames +def tallyNamesByModule (names : Array Name) : CoreM (Std.HashMap Name (Array Name)) := do + let mut ret : Std.HashMap Name (Array Name) := {} + for name in names do + let .some modName ← Lean.findModuleOf? name + | throwError "{decl_name%} :: Cannot find module of {name}" + let orig := (ret.get? modName).getD #[] + ret := ret.insert modName (orig.push name) + return ret + /-- Used as a wrapper in other functions -/ def Name.getCi (name : Name) (parentFunc : Name) : CoreM ConstantInfo := do let .some ci := (← getEnv).find? name diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index 6e56d2a..af69870 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -253,8 +253,14 @@ structure EvalTacticOnMathlibConfig where -/ nonterminates : Array (RegisteredTactic × Name) +abbrev EvalProc := IO.Process.Child ⟨.piped, .piped, .piped⟩ + +def EvalProc.create (path : String) (args : Array String) : IO EvalProc := + IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped, cmd := path, args := args} + /-- - This should be run after `import Mathlib` + This should be run after `import Mathlib`, and should be run with a `cwd` where + `lake env` creates an environment in which `Mathlib` and `lean-auto` are available -/ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : CoreM Unit := do let mms ← mathlibModules @@ -263,9 +269,9 @@ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : Cor 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 + let allTally ← tallyNamesByModule (← allHumanTheorems) for mm in mms do - evaluateFilesHandle.putStrLn mm.toString + evaluateFilesHandle.putStr mm.toString evaluateFilesHandle.flush let nComps := mm.components.length let paths := (List.range nComps).map (fun i => @@ -276,10 +282,46 @@ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : Cor IO.FS.createDir dirPath let .some extraLogPath := paths.getLast? | throwError "evalAtMathlibHumanTheorems :: Module name {mm} has zero components" + let evalProc ← EvalProc.create "lake" #["env", "lean", "--stdin"] 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} + let validThms := (allTally.get? mm).getD #[] + evalProc.stdin.putStr (evalFile mm validThms logPath config.tactics) + let (_, evalProc) ← evalProc.takeStdin + let retCode ← evalProc.wait + evaluateFilesHandle.putStrLn s!" : {retCode}" + evaluateFilesHandle.flush +where + evalFile + (mm : Name) (validThms : Array Name) + (logPath : String) (tacs : Array RegisteredTactic) : String := + let lb := "{" + let rb := "}" + let thmsStrs : List String := + match validThms.toList.getLast? with + | .some last => + validThms.toList.dropLast.map (fun n => s!" {repr n},") ++ [s!" {repr last}"] + | .none => [] + let tacsStr := String.intercalate ", " (tacs.map (fun tac => "." ++ toString tac)).toList + let lines := [ + s!"import {mm}", + "import Auto.EvaluateAuto.TestTactics", + "import Aesop", + "open Lean EvalAuto", + "", + "def humanThms : Std.HashSet Name := Std.HashSet.ofList [" + ] ++ thmsStrs ++ [ + "]", + "", + "def action : CoreM Unit := do", + " let p ← initSrcSearchPath", + s!" let _ ← evalAtModule ({repr mm}) p (fun ci => humanThms.contains ci.name)", + s!" {lb} tactics := #[{tacsStr}],", + s!" logFile := {repr (logPath ++ ".log")}, resultFile := {repr (logPath ++ ".result")},", + s!" nonterminates := #[] {rb}", + "", + "set_option auto.evalAuto.ensureAesop true", + "#eval action" + ] + String.intercalate "\n" lines end EvalAuto From 66d55fd8bf3e37f86ef0e217a3f4bb34aaaa8f89 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sun, 5 Jan 2025 21:49:07 -0800 Subject: [PATCH 09/17] concurrent evaluation --- Auto/EvaluateAuto/TestTactics.lean | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index af69870..b8cb8fc 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -252,6 +252,10 @@ structure EvalTacticOnMathlibConfig where recorded here and avoided (throw error immediately) during evaluation. -/ nonterminates : Array (RegisteredTactic × Name) + /-- + Number of threads to use + -/ + nthreads : Nat abbrev EvalProc := IO.Process.Child ⟨.piped, .piped, .piped⟩ @@ -270,8 +274,9 @@ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : Cor IO.FS.createDir config.resultFolder let evaluateFilesHandle ← IO.FS.Handle.mk (config.resultFolder ++ "/evaluateFiles.txt") .write let allTally ← tallyNamesByModule (← allHumanTheorems) + let mut running := #[] for mm in mms do - evaluateFilesHandle.putStr mm.toString + evaluateFilesHandle.putStrLn mm.toString evaluateFilesHandle.flush let nComps := mm.components.length let paths := (List.range nComps).map (fun i => @@ -287,10 +292,22 @@ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : Cor let validThms := (allTally.get? mm).getD #[] evalProc.stdin.putStr (evalFile mm validThms logPath config.tactics) let (_, evalProc) ← evalProc.takeStdin - let retCode ← evalProc.wait - evaluateFilesHandle.putStrLn s!" : {retCode}" - evaluateFilesHandle.flush + running := running.push (mm, evalProc) + while running.size >= config.nthreads do + running ← tryWaitOn evaluateFilesHandle running + while running.size != 0 do + running ← tryWaitOn evaluateFilesHandle running where + tryWaitOn (evaluateFilesHandle : IO.FS.Handle) (running : Array (Name × _)) : CoreM (Array (Name × _)) := do + let mut running' := #[] + for (mm, proc) in running do + let retCode? ← proc.tryWait + match retCode? with + | .some retCode => + evaluateFilesHandle.putStrLn s!"{mm} : {retCode}" + evaluateFilesHandle.flush + | .none => running' := running'.push (mm, proc) + return running' evalFile (mm : Name) (validThms : Array Name) (logPath : String) (tacs : Array RegisteredTactic) : String := From ec1e82e2bfe9367a47d5d179e704b24aef4c37c1 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sun, 5 Jan 2025 23:54:28 -0800 Subject: [PATCH 10/17] parsing evaluation result --- Auto/EvaluateAuto/NameArr.lean | 102 ++++++++++++++--------------- Auto/EvaluateAuto/Result.lean | 11 +++- Auto/EvaluateAuto/TestAuto.lean | 2 +- Auto/EvaluateAuto/TestTactics.lean | 37 ++++++++++- 4 files changed, 94 insertions(+), 58 deletions(-) diff --git a/Auto/EvaluateAuto/NameArr.lean b/Auto/EvaluateAuto/NameArr.lean index 72955d7..fa7c640 100644 --- a/Auto/EvaluateAuto/NameArr.lean +++ b/Auto/EvaluateAuto/NameArr.lean @@ -11,75 +11,71 @@ def Name.canBeFilename (n : Name) : Bool := match n with | .str _ s => match s.get? 0 with - | .some c => s.all (fun c => c.isAlphanum || c == '_' || c == '\'') + | .some _ => 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. - A `.` is appended to the end of each name. - A `\n` is further appended to the end of the last name. - We use `\` to escape `.` and `\n` occurring in the fields of names, i.e., - `\.` represents literal `.`, `\\n` represents literal `\n`, and - `\\` represents literal `\`. + Unique string representation of names, where it is ensured that `\n` does not occur + A `.` is appended to the end of the name + We use "\\d" to represent ".", "\\n" to represent "\n", "\\\\" to represent "\\" To distinguish `mkStr` and `mkNum`, we prepend `\` to all `mkNum` fields -/ -def NameArray.repr (ns : Array Name) : String := +def Name.uniqRepr (n : Name) : String := let strRepr (s : String) : String := - ((s.replace "\\" "\\\\").replace "." "\\.").replace "\n" "\\\n" + ((s.replace "\\" "\\\\").replace "." "\\d").replace "\n" "\\n" let compRepr (c : Name) : String := match c with | .anonymous => "" | .mkNum _ n => s!"\\{n}" | .mkStr _ s => strRepr s - let nameRepr (n : Name) : String := - String.join (n.components.map (fun c => compRepr c ++ ".")) - String.join (ns.map (fun n => nameRepr n ++ "\n")).toList + String.join (n.components.map (fun c => compRepr c ++ ".")) -/- - Parse string representation of array of names - We use `.` to separate fields of a name, and `\n` to separate names - We use `\` to escape `.` and `\n` occurring in the fields of names, i.e., - `\.` represents literal `.`, `\\n` represents literal `\n`, and - `\\` represents literal `\`. - To distinguish `mkStr` and `mkNum`, we prepend `\` to all `mkNum` fields +/-- + Parsing unique representation of names, see `Name.uniqRepr` -/ -def NameArray.parse (repr : String) : Array Name := Id.run <| do - let mut curField := "" - let mut curFields : Array (String ⊕ Nat) := #[] - let mut allNames : Array Name := #[] - let mut escape := false - let mut num := false - for c in repr.data do - if !escape && c == '.' then - if num then - curFields := curFields.push (.inr ((String.toNat? curField).getD 0)) +def Name.parseUniqRepr (n : String) : Name := + let compParse (s : String) : String ⊕ Nat := Id.run <| do + let s := s.data + if s[0]? == '\\' then + if let .some c := s[1]? then + if c.isDigit then + return .inr ((String.toNat? (String.mk (s.drop 1))).getD 0) + let mut ret := "" + let mut escape := false + for c in s do + if !escape then + if c != '\\' then + ret := ret.push c + else + escape := true else - curFields := curFields.push (.inl curField) - curField := "" - num := false - continue - if !escape && c == '\n' then - let curName := curFields.foldl (fun prev sn => - match sn with - | .inl s => Name.mkStr prev s - | .inr n => Name.mkNum prev n) .anonymous - allNames := allNames.push curName - curFields := #[] - continue - if escape && c.isDigit then - num := true - if c == '\\' then - if escape then escape := false - curField := curField.push c - else - escape := true - else - escape := false - curField := curField.push c - return allNames + match c with + | '\\' => ret := ret.push '\\' + | 'd' => ret := ret.push '.' + | 'n' => ret := ret.push '\n' + | _ => ret := ret.push c + return .inl ret + let components := ((n.splitOn ".").dropLast).map compParse + components.foldl (fun prev sn => + match sn with + | .inl s => Name.mkStr prev s + | .inr n => Name.mkNum prev n) .anonymous + +/-- + Each name in the array is represented using `Name.uniqRepr` + Names are separated using `\n`. A `\n` is further appended to the end of the last name. +-/ +def NameArray.repr (ns : Array Name) : String := + String.join (ns.map (fun n => Name.uniqRepr n ++ "\n")).toList + +/- + Each name in the array is represented using `Name.uniqRepr` + Names are separated using `\n`. A `\n` is further appended to the end of the last name. +-/ +def NameArray.parse (repr : String) : Array Name := + Array.mk ((repr.splitOn "\n").map Name.parseUniqRepr).dropLast def NameArray.save (ns : Array Name) (fname : String) : IO Unit := do let fd ← IO.FS.Handle.mk fname .write diff --git a/Auto/EvaluateAuto/Result.lean b/Auto/EvaluateAuto/Result.lean index 717d897..2af7235 100644 --- a/Auto/EvaluateAuto/Result.lean +++ b/Auto/EvaluateAuto/Result.lean @@ -36,7 +36,16 @@ def Result.concise : Result → String | .nonterminate => "T" | .subGoals => "G" | .exception _ => "E" - +#check Exception +def Result.ofConcise? : String → Option Result +| "S" => .some .success +| "N" => .some .nonProp +| "F" => .some .typeCheckFail +| "U" => .some .typeUnequal +| "T" => .some .nonterminate +| "G" => .some .subGoals +| "E" => .some (.exception (.error Syntax.missing "Filled_in_by_Result.ofConcise?")) +| _ => .none open Elab Tactic in /-- diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 374787b..9d12f01 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -163,7 +163,7 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit 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}" + fhandle.putStrLn s!"{idx} {result.concise} {Name.uniqRepr name}" def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := do let names ← NameArray.load fname diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index b8cb8fc..ef6f65e 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -210,7 +210,7 @@ def evalAtModule 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}" + fhandle.putStrLn s!"{idx} {result.map Result.concise} {Name.uniqRepr name}" where evalAction (context : Core.Context) (state : Core.State) (ci : ConstantInfo) @@ -269,7 +269,7 @@ def EvalProc.create (path : String) (args : Array String) : IO EvalProc := 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!" + 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 @@ -341,4 +341,35 @@ where ] String.intercalate "\n" lines -end EvalAuto +/-- + Read results generated by `evalTacticsAtMathlibHumanTheorems` +-/ +def readTacticEvalResult (config : EvalTacticOnMathlibConfig) : + CoreM (Array (Name × Array (Name × Array Result))) := do + let resultFolder := config.resultFolder + if !(← System.FilePath.isDir resultFolder) then + throwError "{decl_name%} :: {config.resultFolder} is not a directory" + let allPaths ← System.FilePath.walkDir resultFolder + let mut ret := #[] + for path in allPaths do + if !(← System.FilePath.isDir path) && path.toString.takeRight 7 == ".result" then + let suffix := (path.toString.drop (resultFolder.length + 1)).dropRight 7 + let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous + let lines := (← IO.FS.readFile path).splitOn "\n" + if lines[3]? != .some "Summary:" || lines[4]? != .some "" then + throwError "{decl_name%} :: Format of result file changed, please change analysis code" + let lines := (lines.drop 4).filter (fun s => s != "") + let lineAnalysis ← (Array.mk lines).mapM analyzeLine + ret := ret.push (modName, lineAnalysis) + return ret +where + analyzeLine (line : String) : CoreM (Name × Array Result) := 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 line := (line.dropWhile (fun c => c != ']')).drop 2 + let name := Name.parseUniqRepr line + return (name, tr) From 6886c6000277bbb866817d5a4606e4c7769e39a3 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Mon, 6 Jan 2025 01:34:48 -0800 Subject: [PATCH 11/17] small fix --- Auto/EvaluateAuto/Result.lean | 5 ++++- Auto/EvaluateAuto/TestTactics.lean | 7 ++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/Auto/EvaluateAuto/Result.lean b/Auto/EvaluateAuto/Result.lean index 2af7235..636a5b8 100644 --- a/Auto/EvaluateAuto/Result.lean +++ b/Auto/EvaluateAuto/Result.lean @@ -18,6 +18,9 @@ inductive Result | subGoals | exception (e : Exception) +instance : Inhabited Result where + default := .success + instance : ToMessageData Result where toMessageData : Result → MessageData | .success => "Result.success" @@ -36,7 +39,7 @@ def Result.concise : Result → String | .nonterminate => "T" | .subGoals => "G" | .exception _ => "E" -#check Exception + def Result.ofConcise? : String → Option Result | "S" => .some .success | "N" => .some .nonProp diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index ef6f65e..4082192 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -355,9 +355,10 @@ def readTacticEvalResult (config : EvalTacticOnMathlibConfig) : if !(← System.FilePath.isDir path) && path.toString.takeRight 7 == ".result" then let suffix := (path.toString.drop (resultFolder.length + 1)).dropRight 7 let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous - let lines := (← IO.FS.readFile path).splitOn "\n" - if lines[3]? != .some "Summary:" || lines[4]? != .some "" then - throwError "{decl_name%} :: Format of result file changed, please change analysis code" + let content ← IO.FS.readFile path + let lines := content.splitOn "\n" + if lines[2]? != .some "Summary:" || lines[3]? != .some "" then + throwError "{decl_name%} :: Format of result file changed, please change analysis code. Result file : {path}" let lines := (lines.drop 4).filter (fun s => s != "") let lineAnalysis ← (Array.mk lines).mapM analyzeLine ret := ret.push (modName, lineAnalysis) From 25c8f253f0d78a2e65f1612e22cd19c15eaf7c1c Mon Sep 17 00:00:00 2001 From: PratherConid Date: Tue, 7 Jan 2025 13:36:11 -0800 Subject: [PATCH 12/17] add support for raw native prover --- Auto/EvaluateAuto/TestAuto.lean | 45 ++++++++++++++++++++------------- 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 9d12f01..9985a19 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -10,7 +10,11 @@ open Lean Auto namespace EvalAuto inductive SolverConfig where + -- Use `duper` as the backend prover | native + -- Use `duper` as the backend prover, without any preprocessing + | rawNative + -- Use `lean-smt`, currently not supported | leanSmt | smt (solverName : Solver.SMT.SolverName) | tptp (solverName : Solver.TPTP.SolverName) (path : String) @@ -18,6 +22,7 @@ inductive SolverConfig where instance : ToString SolverConfig where toString : SolverConfig → String | .native => "native" + | .rawNative => "rawNative" | .leanSmt => "leanSmt" | .smt sn => s!"smt {sn}" | .tptp sn path => s!"tptp {sn} {path}" @@ -49,24 +54,25 @@ instance : ToString EvalAutoConfig where s!"solverConfig := {solverConfig}{logFileStr}{resultFileStr}}" /-- - Run `Lean-auto` on `lem.type`, using premises collected from `lem.proof` + Run `prover` on `lem.type`, using premises collected from `lem.proof` Premises which only contain logic constants are filtered because they are assumed to be known by the prover -/ -private def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : CoreM Result := do +private def runProverOnAutoLemma + (lem : Auto.Lemma) (prover : Array Lemma → Array Lemma → MetaM Expr) : CoreM Result := do if !(← Meta.MetaM.run' <| Meta.isProp lem.type) then return .nonProp -- **TODO: Aux theorem like those ending in `.proof_1`** let usedThmNames ← (← Expr.getUsedTheorems lem.proof).filterM (fun name => return !(← Name.onlyLogicInType name)) let usedThms ← usedThmNames.mapM (fun n => Lemma.ofConst n (.leaf "collected by hammertest")) - let autoProofFn : MetaM Expr := Meta.forallTelescope lem.type fun bs body => do + let proverFn : MetaM Expr := Meta.forallTelescope lem.type fun bs body => do let negGoal := Expr.app (.const ``Not []) body let negGoalImpFalse ← Meta.withLocalDeclD `negGoal negGoal fun negGoalFVar => do let inhLemmas ← Auto.Inhabitation.getInhFactsFromLCtx let lctxLemmas ← Auto.collectLctxLemmas true #[] let allLemmas ← (lctxLemmas ++ usedThms).mapM (Auto.unfoldConstAndPreprocessLemma #[]) - let proofOfFalse ← Auto.runAuto declName? allLemmas inhLemmas + let proofOfFalse ← prover allLemmas inhLemmas Meta.mkLambdaFVars #[negGoalFVar] proofOfFalse let goal := mkApp2 (.const ``Classical.byContradiction []) body negGoalImpFalse Meta.mkLambdaFVars bs goal @@ -74,31 +80,32 @@ private def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : Co let metaContext : Meta.Context := { config := Elab.Term.setElabConfig {} } let result : Expr ⊕ Exception ← Lean.Core.tryCatchRuntimeEx - (do let autoProof ← Meta.MetaM.run' autoProofFn (ctx := metaContext); return .inl autoProof) + (do let proof ← Meta.MetaM.run' proverFn (ctx := metaContext); return .inl proof) (fun e => return .inr e) match result with - | .inl autoProof => - match Kernel.check (← getEnv) {} autoProof with - | Except.ok autoProofType => - match Kernel.isDefEq (← getEnv) {} autoProofType lem.type with + | .inl proof => + match Kernel.check (← getEnv) {} proof with + | Except.ok proofType => + match Kernel.isDefEq (← getEnv) {} proofType lem.type with | Except.ok true => return .success | _ => return .typeUnequal | Except.error _ => return .typeCheckFail | .inr e => return .exception e /-- - Run `Lean-auto` on the type of ``name``, using premises collected + Run `prover` on the type of ``name``, using premises collected from the proof of `name` Premises which only contain logic constants are filtered because they are assumed to be known by the prover -/ -def runAutoOnConst (name : Name) : CoreM Result := do +def runProverOnConst + (name : Name) (prover : Array Lemma → Array Lemma → MetaM Expr) : CoreM Result := do let ci ← Name.getCi name decl_name% let .some v := ci.value? | throwError "{decl_name%} :: {name} has no value" let lemmaPre ← Auto.Lemma.ofConst name (.leaf "ofConst") let lemmaV := {lemmaPre with proof := v} - runAutoOnAutoLemma (.some name) lemmaV + runProverOnAutoLemma lemmaV prover def disableAllSolvers (o : Options) : Options := let o := auto.native.set o false @@ -124,15 +131,17 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit let result : Result ← withCurrHeartbeats <| withReader (fun ctx => {ctx with maxHeartbeats := config.maxHeartbeats * 1000}) <| match config.solverConfig with - | .native => + | .native => withOptions (fun o => let o := disableAllSolvers o let o := auto.native.set o true let o := auto.mono.mode.set o MonoMode.hol - o) <| runAutoOnConst name - | .leanSmt => + o) <| runProverOnConst name (Auto.runAuto (.some name)) + | .rawNative => + runProverOnConst name Solver.Native.queryNative + | .leanSmt => throwError "Lean-SMT is currently not supported" - | .smt sn => + | .smt sn => withOptions (fun o => let o := disableAllSolvers o let o := auto.smt.set o true @@ -140,7 +149,7 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit let o := auto.smt.timeout.set o config.timeout let o := auto.smt.trust.set o true let o := auto.mono.mode.set o MonoMode.fol - o) <| runAutoOnConst name + o) <| runProverOnConst name (Auto.runAuto (.some name)) | .tptp sn path => withOptions (fun o => let o := disableAllSolvers o @@ -154,7 +163,7 @@ def runAutoOnConsts (config : EvalAutoConfig) (names : Array Name) : CoreM Unit | .zeport _ => auto.tptp.zeport.path.set o path | .eproverHo => auto.tptp.eproverHo.path.set o path | .vampire => auto.tptp.vampire.path.set o path) <| - runAutoOnConst name + runProverOnConst name (Auto.runAuto (.some name)) trace[auto.eval.printResult] m!"{result}" results := results.push result if let .some fhandle := logFileHandle? then From 2e43ab8877899030a00b699a7c5492b5ea91998b Mon Sep 17 00:00:00 2001 From: PratherConid Date: Tue, 7 Jan 2025 14:30:41 -0800 Subject: [PATCH 13/17] eval auto on mathlib --- Auto/EvaluateAuto/OS.lean | 4 ++ Auto/EvaluateAuto/TestAuto.lean | 86 ++++++++++++++++++++++++++++++ Auto/EvaluateAuto/TestTactics.lean | 18 +++---- Auto/Solver/SMT.lean | 2 +- Auto/Solver/TPTP.lean | 4 +- 5 files changed, 99 insertions(+), 15 deletions(-) create mode 100644 Auto/EvaluateAuto/OS.lean diff --git a/Auto/EvaluateAuto/OS.lean b/Auto/EvaluateAuto/OS.lean new file mode 100644 index 0000000..aae9b8a --- /dev/null +++ b/Auto/EvaluateAuto/OS.lean @@ -0,0 +1,4 @@ +abbrev EvalProc := IO.Process.Child ⟨.piped, .piped, .piped⟩ + +def EvalProc.create (path : String) (args : Array String) : IO EvalProc := + IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped, cmd := path, args := args} diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 9985a19..5976ab7 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -1,4 +1,5 @@ import Lean +import Auto.EvaluateAuto.OS import Auto.EvaluateAuto.Result import Auto.EvaluateAuto.ConstAnalysis import Auto.EvaluateAuto.EnvAnalysis @@ -18,6 +19,7 @@ inductive SolverConfig where | leanSmt | smt (solverName : Solver.SMT.SolverName) | tptp (solverName : Solver.TPTP.SolverName) (path : String) + deriving Repr instance : ToString SolverConfig where toString : SolverConfig → String @@ -178,4 +180,88 @@ def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := d let names ← NameArray.load fname runAutoOnConsts cfg names +structure EvalAutoOnMathlibConfig where + /-- Timeout for Lean code (Lean-auto + native provers) -/ + maxHeartbeats : Nat := 65536 + /-- Timeout for external provers, i.e. TPTP solvers and SMT solvers -/ + timeout : Nat := 10 + /-- Solver configuration -/ + solverConfig : SolverConfig + /-- Folder for saving the result of the evaluation -/ + resultFolder : String + /-- Number of threads to use -/ + nthreads : Nat + /-- Batch size -/ + batchSize : Nat + +def Array.groupBySize (xs : Array α) (size : Nat) : Option (Array (Array α)) := + if size == 0 then + .none + else + let n := (xs.size + size - 1) / size + let ret := Array.mk <| (List.range n).map (fun i => Array.mk <| (xs.toList.drop (size * i)).take size) + some ret + +def evalAutoAtMathlibHumanTheorems (config : EvalAutoOnMathlibConfig) : CoreM Unit := do + 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 + let .some batches := Array.groupBySize all config.batchSize + | throwError "Batch size must be nonzero" + let mut running := #[] + for (batch, idx) in batches.zipWithIndex do + evaluateFilesHandle.putStrLn (toString idx) + evaluateFilesHandle.flush + let evalProc ← EvalProc.create "lake" #["env", "lean", "--stdin"] + let logPath := config.resultFolder ++ toString idx + evalProc.stdin.putStr (evalFile batch logPath) + let (_, evalProc) ← evalProc.takeStdin + running := running.push (idx, evalProc) + while running.size >= config.nthreads do + running ← tryWaitOn evaluateFilesHandle running + while running.size != 0 do + running ← tryWaitOn evaluateFilesHandle running +where + tryWaitOn (evaluateFilesHandle : IO.FS.Handle) (running : Array (Nat × _)) : CoreM (Array (Nat × _)) := do + let mut running' := #[] + for (idx, proc) in running do + let retCode? ← proc.tryWait + match retCode? with + | .some retCode => + evaluateFilesHandle.putStrLn s!"{idx} : {retCode}" + evaluateFilesHandle.flush + | .none => running' := running'.push (idx, proc) + return running' + evalFile + (thms : Array Name) (logPath : String) : String := + let lb := "{" + let rb := "}" + let thmsStrs : List String := + match thms.toList.getLast? with + | .some last => + thms.toList.dropLast.map (fun n => s!" {repr n},") ++ [s!" {repr last}"] + | .none => [] + let lines := [ + s!"import Mathlib", + "import Auto.EvaluateAuto.TestAuto", + "import Auto.Tactic", + "open Lean EvalAuto", + "", + "def thms : Std.HashSet Name := Std.HashSet.ofList [" + ] ++ thmsStrs ++ [ + "]", + "", + "def action : CoreM Unit := do", + " let p ← initSrcSearchPath", + s!" let _ ← runAutoOnConsts", + s!" {lb} maxHeartbeats := {config.maxHeartbeats}, timeout := {config.timeout},", + s!" solverConfig := {repr config.solverConfig},", + s!" logFile := Option.some ({repr (logPath ++ ".log")}), resultFile := Option.some ({repr (logPath ++ ".result")}){rb}", + " thms", + "", + "#eval action" + ] + String.intercalate "\n" lines + end EvalAuto diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index 4082192..32700df 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -1,4 +1,5 @@ import Lean +import Auto.EvaluateAuto.OS import Auto.EvaluateAuto.Result import Auto.EvaluateAuto.ConstAnalysis import Auto.EvaluateAuto.EnvAnalysis @@ -252,16 +253,9 @@ structure EvalTacticOnMathlibConfig where recorded here and avoided (throw error immediately) during evaluation. -/ nonterminates : Array (RegisteredTactic × Name) - /-- - Number of threads to use - -/ + /-- Number of threads to use -/ nthreads : Nat -abbrev EvalProc := IO.Process.Child ⟨.piped, .piped, .piped⟩ - -def EvalProc.create (path : String) (args : Array String) : IO EvalProc := - IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped, cmd := path, args := args} - /-- This should be run after `import Mathlib`, and should be run with a `cwd` where `lake env` creates an environment in which `Mathlib` and `lean-auto` are available @@ -290,7 +284,7 @@ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : Cor let evalProc ← EvalProc.create "lake" #["env", "lean", "--stdin"] let logPath := config.resultFolder ++ extraLogPath let validThms := (allTally.get? mm).getD #[] - evalProc.stdin.putStr (evalFile mm validThms logPath config.tactics) + evalProc.stdin.putStr (evalFile mm validThms logPath config) let (_, evalProc) ← evalProc.takeStdin running := running.push (mm, evalProc) while running.size >= config.nthreads do @@ -310,7 +304,7 @@ where return running' evalFile (mm : Name) (validThms : Array Name) - (logPath : String) (tacs : Array RegisteredTactic) : String := + (logPath : String) (config : EvalTacticOnMathlibConfig) : String := let lb := "{" let rb := "}" let thmsStrs : List String := @@ -318,7 +312,7 @@ where | .some last => validThms.toList.dropLast.map (fun n => s!" {repr n},") ++ [s!" {repr last}"] | .none => [] - let tacsStr := String.intercalate ", " (tacs.map (fun tac => "." ++ toString tac)).toList + let tacsStr := String.intercalate ", " (config.tactics.map (fun tac => "." ++ toString tac)).toList let lines := [ s!"import {mm}", "import Auto.EvaluateAuto.TestTactics", @@ -332,7 +326,7 @@ where "def action : CoreM Unit := do", " let p ← initSrcSearchPath", s!" let _ ← evalAtModule ({repr mm}) p (fun ci => humanThms.contains ci.name)", - s!" {lb} tactics := #[{tacsStr}],", + s!" {lb} maxHeartbeats := {config.maxHeartbeats}, tactics := #[{tacsStr}],", s!" logFile := {repr (logPath ++ ".log")}, resultFile := {repr (logPath ++ ".result")},", s!" nonterminates := #[] {rb}", "", diff --git a/Auto/Solver/SMT.lean b/Auto/Solver/SMT.lean index 0b31907..8f7bb2e 100644 --- a/Auto/Solver/SMT.lean +++ b/Auto/Solver/SMT.lean @@ -62,7 +62,7 @@ inductive SolverName where | z3 | cvc4 | cvc5 -deriving BEq, Hashable, Inhabited +deriving BEq, Hashable, Inhabited, Repr instance : ToString SolverName where toString : SolverName → String diff --git a/Auto/Solver/TPTP.lean b/Auto/Solver/TPTP.lean index 478e815..8de7170 100644 --- a/Auto/Solver/TPTP.lean +++ b/Auto/Solver/TPTP.lean @@ -43,7 +43,7 @@ namespace Solver.TPTP inductive ZEPortType where | fo | lams -deriving BEq, Hashable, Inhabited +deriving BEq, Hashable, Inhabited, Repr inductive SolverName where -- Disable TPTP prover @@ -53,7 +53,7 @@ inductive SolverName where -- E prover, higher-order version | eproverHo | vampire -deriving BEq, Hashable, Inhabited +deriving BEq, Hashable, Inhabited, Repr instance : ToString SolverName where toString : SolverName → String From ce5671fba2ec8506d66c40558821cbff7fa9335f Mon Sep 17 00:00:00 2001 From: PratherConid Date: Tue, 7 Jan 2025 15:05:01 -0800 Subject: [PATCH 14/17] fix --- Auto/EvaluateAuto/TestAuto.lean | 9 +++++++-- Auto/EvaluateAuto/TestTactics.lean | 5 +++-- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 5976ab7..351eb62 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -202,6 +202,11 @@ def Array.groupBySize (xs : Array α) (size : Nat) : Option (Array (Array α)) : let ret := Array.mk <| (List.range n).map (fun i => Array.mk <| (xs.toList.drop (size * i)).take size) some ret +/-- + This should be run after `import Mathlib, import Auto.EvaluateAuto.TestTactics`, + and should be run with a `cwd` where `lake env` creates an environment in which + `Mathlib` and `lean-auto` are available +-/ def evalAutoAtMathlibHumanTheorems (config : EvalAutoOnMathlibConfig) : CoreM Unit := do if !(← System.FilePath.isDir config.resultFolder) then IO.FS.createDir config.resultFolder @@ -214,7 +219,7 @@ def evalAutoAtMathlibHumanTheorems (config : EvalAutoOnMathlibConfig) : CoreM Un evaluateFilesHandle.putStrLn (toString idx) evaluateFilesHandle.flush let evalProc ← EvalProc.create "lake" #["env", "lean", "--stdin"] - let logPath := config.resultFolder ++ toString idx + let logPath := config.resultFolder ++ "/" ++ toString idx evalProc.stdin.putStr (evalFile batch logPath) let (_, evalProc) ← evalProc.takeStdin running := running.push (idx, evalProc) @@ -248,7 +253,7 @@ where "import Auto.Tactic", "open Lean EvalAuto", "", - "def thms : Std.HashSet Name := Std.HashSet.ofList [" + "def thms : Array Name := #[" ] ++ thmsStrs ++ [ "]", "", diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean index 32700df..0994996 100644 --- a/Auto/EvaluateAuto/TestTactics.lean +++ b/Auto/EvaluateAuto/TestTactics.lean @@ -257,8 +257,9 @@ structure EvalTacticOnMathlibConfig where nthreads : Nat /-- - This should be run after `import Mathlib`, and should be run with a `cwd` where - `lake env` creates an environment in which `Mathlib` and `lean-auto` are available + This should be run after `import Mathlib` and `import Auto.EvaluateAuto.TestTactics`, + and should be run with a `cwd` where `lake env` creates an environment in which + `Mathlib` and `lean-auto` are available -/ def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : CoreM Unit := do let mms ← mathlibModules From 128b0975d262992d69d02a60e3b5728a85bc3297 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Tue, 7 Jan 2025 16:07:51 -0800 Subject: [PATCH 15/17] fix messages --- Auto/EvaluateAuto/TestAuto.lean | 14 +++++++++++--- Auto/Translation/Monomorphization.lean | 2 +- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 351eb62..3fc94d3 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -205,13 +205,13 @@ def Array.groupBySize (xs : Array α) (size : Nat) : Option (Array (Array α)) : /-- This should be run after `import Mathlib, import Auto.EvaluateAuto.TestTactics`, and should be run with a `cwd` where `lake env` creates an environment in which - `Mathlib` and `lean-auto` are available + `Mathlib, lean-auto` and `duper` are available -/ def evalAutoAtMathlibHumanTheorems (config : EvalAutoOnMathlibConfig) : CoreM Unit := do 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 + let all ← allHumanTheoremsFromPackage "Mathlib" let .some batches := Array.groupBySize all config.batchSize | throwError "Batch size must be nonzero" let mut running := #[] @@ -251,7 +251,15 @@ where s!"import Mathlib", "import Auto.EvaluateAuto.TestAuto", "import Auto.Tactic", - "open Lean EvalAuto", + "import Duper.Tactic", + "open Lean Auto EvalAuto", + "", + "def Auto.duperRaw (lemmas : Array Lemma) (inhs : Array Lemma) : MetaM Expr := do", + " let lemmas : Array (Expr × Expr × Array Name × Bool) ← lemmas.mapM", + " (fun ⟨⟨proof, ty, _⟩, _⟩ => do return (ty, ← Meta.mkAppM ``eq_true #[proof], #[], true))", + " Duper.runDuper lemmas.toList 0", + "", + "attribute [rebind Auto.Native.solverFunc] Auto.duperRaw", "", "def thms : Array Name := #[" ] ++ thmsStrs ++ [ diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean index 0b7b434..fe47a0e 100644 --- a/Auto/Translation/Monomorphization.lean +++ b/Auto/Translation/Monomorphization.lean @@ -888,7 +888,7 @@ namespace FVarRep let m₄ := m!"· λ binders whose type contain bound variables, e.g. `fun (x : a) => x` where `a` is a bound variable" let m₅ := m!"· Other (TODO)" let m₆ := m!"`set_option auto.mono.ignoreNonQuasiHigherOrder true` will instruct Lean-auto to ignore " ++ - m!"all the `LemmaInst`s which contain expressions that cannot be handeled by the current procedure" + m!"all the `LemmaInst`s which contain expressions that cannot be handled by the current procedure" m₁ ++ "\n" ++ m₂ ++ "\n" ++ m₃ ++ "\n" ++ m₄ ++ "\n" ++ m₅ ++ "\n" ++ m₆ def unknownExpr2FVar (e : Expr) : FVarRepM (Expr ⊕ MessageData) := do From 26d9cb3da795010b3e4e2110e155e8b13ed2c2c0 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Fri, 10 Jan 2025 20:29:48 -0800 Subject: [PATCH 16/17] set ignorenonquasi option --- Auto/EvaluateAuto/TestAuto.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 3fc94d3..426f058 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -265,6 +265,8 @@ where ] ++ thmsStrs ++ [ "]", "", + "set_option auto.mono.ignoreNonQuasiHigherOrder true", + "", "def action : CoreM Unit := do", " let p ← initSrcSearchPath", s!" let _ ← runAutoOnConsts", From 384d3081a9ae0eb01cdf8765480060e1a11c75a3 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Fri, 10 Jan 2025 23:04:25 -0800 Subject: [PATCH 17/17] add readresult for auto evaluation --- Auto/EvaluateAuto/TestAuto.lean | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean index 426f058..4c16414 100644 --- a/Auto/EvaluateAuto/TestAuto.lean +++ b/Auto/EvaluateAuto/TestAuto.lean @@ -279,4 +279,34 @@ where ] String.intercalate "\n" lines +/-- + Read results generated by `evalAutoAtMathlibHumanTheorems` +-/ +def readAutoEvalResult (config : EvalAutoOnMathlibConfig) : + CoreM (Array (Name × Result)) := do + let resultFolder := config.resultFolder + if !(← System.FilePath.isDir resultFolder) then + throwError "{decl_name%} :: {config.resultFolder} is not a directory" + let allFiles := (← System.FilePath.readDir resultFolder).map IO.FS.DirEntry.path + let mut ret := #[] + for file in allFiles do + if !(← System.FilePath.isDir file) && file.toString.takeRight 7 == ".result" then + let content ← IO.FS.readFile file + let lines := content.splitOn "\n" + if lines[2]? != .some "Summary:" || lines[3]? != .some "" then + throwError "{decl_name%} :: Format of result file changed, please change analysis code. Result file : {file}" + let lines := (lines.drop 4).filter (fun s => s != "") + let lineAnalysis ← (Array.mk lines).mapM analyzeLine + ret := ret.append lineAnalysis + return ret +where + analyzeLine (line : String) : CoreM (Name × Result) := do + let line := (line.dropWhile (fun c => c != ' ')).drop 1 + let s := line.takeWhile (fun c => c != ' ') + let .some tr := 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 name := Name.parseUniqRepr line + return (name, tr) + end EvalAuto