From 9894ad7c7e2a8e7fde305e1a542f708fd1481c5e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:16:14 -0800 Subject: [PATCH 01/45] refactor: InfoTree functions --- Pantograph/Frontend.lean | 2 +- Pantograph/Frontend/Elab.lean | 82 ++----------------------------- Pantograph/Frontend/InfoTree.lean | 81 ++++++++++++++++++++++++++++++ 3 files changed, 85 insertions(+), 80 deletions(-) create mode 100644 Pantograph/Frontend/InfoTree.lean diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean index fd91823..9a41567 100644 --- a/Pantograph/Frontend.lean +++ b/Pantograph/Frontend.lean @@ -1,4 +1,4 @@ -/- Adapted from lean-training-data by semorrison -/ import Pantograph.Frontend.Basic import Pantograph.Frontend.Elab +import Pantograph.Frontend.InfoTree import Pantograph.Frontend.MetaTranslate diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index ceecfae..b3173a7 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -7,77 +7,10 @@ import Pantograph.Frontend.Basic import Pantograph.Frontend.MetaTranslate import Pantograph.Goal import Pantograph.Protocol +import Pantograph.Frontend.InfoTree open Lean -namespace Lean.Elab.Info -/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/ -protected def stx? : Info → Option Syntax - | .ofTacticInfo info => info.stx - | .ofTermInfo info => info.stx - | .ofCommandInfo info => info.stx - | .ofMacroExpansionInfo info => info.stx - | .ofOptionInfo info => info.stx - | .ofFieldInfo info => info.stx - | .ofCompletionInfo info => info.stx - | .ofUserWidgetInfo info => info.stx - | .ofCustomInfo info => info.stx - | .ofFVarAliasInfo _ => none - | .ofFieldRedeclInfo info => info.stx - | .ofOmissionInfo info => info.stx -/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/ -protected def isOriginal (i : Info) : Bool := - match i.stx? with - | none => true -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative. - | some stx => match stx.getHeadInfo with - | .original .. => true - | _ => false -end Lean.Elab.Info - -namespace Lean.Elab.TacticInfo - -/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/ -def name? (t : TacticInfo) : Option Name := - match t.stx with - | Syntax.node _ n _ => some n - | _ => none -/-- Decide whether a tactic is "substantive", -or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/ -def isSubstantive (t : TacticInfo) : Bool := - match t.name? with - | none => false - | some `null => false - | some ``cdot => false - | some ``cdotTk => false - | some ``Lean.Parser.Term.byTactic => false - | some ``Lean.Parser.Tactic.tacticSeq => false - | some ``Lean.Parser.Tactic.tacticSeq1Indented => false - | some ``Lean.Parser.Tactic.«tactic_<;>_» => false - | some ``Lean.Parser.Tactic.paren => false - | _ => true - -end Lean.Elab.TacticInfo - -namespace Lean.Elab.InfoTree - -/-- -Keep `.node` nodes and `.hole` nodes satisfying predicates. - -Returns a `List InfoTree`, although in most situations this will be a singleton. --/ -partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : - InfoTree → List InfoTree - | .context ctx tree => tree.filter p m |>.map (.context ctx) - | .node info children => - if p info then - [.node info (children.toList.map (filter p m)).join.toPArray'] - else - (children.toList.map (filter p m)).join - | .hole mvar => if m mvar then [.hole mvar] else [] - -end Lean.Elab.InfoTree - - namespace Pantograph.Frontend -- Info tree filtering functions @@ -131,19 +64,10 @@ protected def usedConstants (t: TacticInvocation) : NameSet := end TacticInvocation -/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ -partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) : - List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) := - match t with - | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred - | .node i children => - (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) - | _ => [] - /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, each equipped with its relevant `ContextInfo`, and any children info trees. -/ private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := - let infos := findAllInfo t none fun i => match i with + let infos := t.findAllInfo none fun i => match i with | .ofTacticInfo _ => true | _ => false infos.filterMap fun p => match p with @@ -178,7 +102,7 @@ structure InfoWithContext where context?: Option Elab.ContextInfo := .none private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext := - let infos := findAllInfo t none fun i => match i with + let infos := t.findAllInfo none fun i => match i with | .ofTermInfo { expectedType?, expr, stx, .. } => expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry | .ofTacticInfo { stx, goalsBefore, .. } => diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean new file mode 100644 index 0000000..4e60710 --- /dev/null +++ b/Pantograph/Frontend/InfoTree.lean @@ -0,0 +1,81 @@ +/- Adapted from lean-training-data by semorrison -/ +import Lean.Elab.InfoTree +import Lean.Parser.Term + +open Lean + +namespace Lean.Elab.Info +/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/ +protected def stx? : Info → Option Syntax + | .ofTacticInfo info => info.stx + | .ofTermInfo info => info.stx + | .ofCommandInfo info => info.stx + | .ofMacroExpansionInfo info => info.stx + | .ofOptionInfo info => info.stx + | .ofFieldInfo info => info.stx + | .ofCompletionInfo info => info.stx + | .ofUserWidgetInfo info => info.stx + | .ofCustomInfo info => info.stx + | .ofFVarAliasInfo _ => none + | .ofFieldRedeclInfo info => info.stx + | .ofOmissionInfo info => info.stx +/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/ +protected def isOriginal (i : Info) : Bool := + match i.stx? with + | none => true -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative. + | some stx => match stx.getHeadInfo with + | .original .. => true + | _ => false +end Lean.Elab.Info + +namespace Lean.Elab.TacticInfo + +/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/ +def name? (t : TacticInfo) : Option Name := + match t.stx with + | Syntax.node _ n _ => some n + | _ => none +/-- Decide whether a tactic is "substantive", +or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/ +def isSubstantive (t : TacticInfo) : Bool := + match t.name? with + | none => false + | some `null => false + | some ``cdot => false + | some ``cdotTk => false + | some ``Lean.Parser.Term.byTactic => false + | some ``Lean.Parser.Tactic.tacticSeq => false + | some ``Lean.Parser.Tactic.tacticSeq1Indented => false + | some ``Lean.Parser.Tactic.«tactic_<;>_» => false + | some ``Lean.Parser.Tactic.paren => false + | _ => true + +end Lean.Elab.TacticInfo + +namespace Lean.Elab.InfoTree + +/-- +Keep `.node` nodes and `.hole` nodes satisfying predicates. + +Returns a `List InfoTree`, although in most situations this will be a singleton. +-/ +partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : + InfoTree → List InfoTree + | .context ctx tree => tree.filter p m |>.map (.context ctx) + | .node info children => + if p info then + [.node info (children.toList.map (filter p m)).join.toPArray'] + else + (children.toList.map (filter p m)).join + | .hole mvar => if m mvar then [.hole mvar] else [] + +/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ +partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) : + List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) := + match t with + | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred + | .node i children => + (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) + | _ => [] + +end Lean.Elab.InfoTree From a8e7a1a726c7fe5595c92e5c5b8ff4228628ab65 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:34:52 -0800 Subject: [PATCH 02/45] feat: Erase macro scopes in sexp --- Pantograph/Delate.lean | 6 +++--- Test/Delate.lean | 2 +- Test/Library.lean | 2 +- Test/Proofs.lean | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index be17729..141abd9 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -346,20 +346,20 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM let args := " ".intercalate args pure s!"({fn'} {args})" | .lam binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" | .forallE binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" | .letE name type value body _ => do -- Dependent boolean flag diacarded - let name' := serializeName name + let name' := name.eraseMacroScopes let type' ← self type let value' ← self value let body' ← self body diff --git a/Test/Delate.lean b/Test/Delate.lean index 227ab24..d918dc8 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -32,7 +32,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do let entries: List (String × String) := [ -- This one contains unhygienic variable names which must be suppressed - ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"), + ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"), -- These ones are normal and easy ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"), ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"), diff --git a/Test/Library.lean b/Test/Library.lean index d995374..df1ba4d 100644 --- a/Test/Library.lean +++ b/Test/Library.lean @@ -24,7 +24,7 @@ def test_expr_echo (env: Environment): IO LSpec.TestSeq := do }, expr := { pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩", - sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))", + sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall a 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))", } })) return tests diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8e3e2a2..02c1bf6 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -282,9 +282,9 @@ def test_or_comm: TestM Unit := do serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" - let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" - let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" - let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" + let caseL := s!"(:lambda h (:fv {fvP}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let caseR := s!"(:lambda h (:fv {fvQ}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))" addTest $ LSpec.test "(2 parent)" (state2parent == s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})") From 44aef76a10a9638caecef46326130ffd7c9fad29 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:57:19 -0800 Subject: [PATCH 03/45] refactor: Remove sanitization for mvarId/fvarId --- Pantograph/Delate.lean | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 141abd9..4b3bd51 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -327,11 +327,11 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM -- Lean these are handled using a `#` prefix. pure s!"{deBruijnIndex}" | .fvar fvarId => - let name := ofName fvarId.name + let name := fvarId.name pure s!"(:fv {name})" | .mvar mvarId => do let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv" - let name := ofName mvarId.name + let name := mvarId.name pure s!"(:{pref} {name})" | .sort level => let level := serializeSortLevel level sanitize @@ -387,7 +387,6 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM | .implicit => " :implicit" | .strictImplicit => " :strictImplicit" | .instImplicit => " :instImplicit" - ofName (name: Name) := serializeName name sanitize def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp?: Option String ← match options.printExprPretty with @@ -420,13 +419,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava match localDecl with | .cdecl _ fvarId userName _ _ _ => return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName := toString userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } @@ -436,7 +435,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava let userName := userName.simpMacroScopes let type ← instantiate type return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -450,7 +449,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava else pure $ .none return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -469,7 +468,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava | false => ppVar localDecl return var::acc return { - name := ofName goal.name, + name := goal.name.toString, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serializeExpression options (← instantiate mvarDecl.type)), From 7c9b092200ffc3365060cf7e0d6d0db1c809aeb4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 30 Nov 2024 23:21:16 -0800 Subject: [PATCH 04/45] test: Dual monad testing stub --- Test/Common.lean | 2 ++ Test/Main.lean | 4 +++- Test/Serial.lean | 56 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+), 1 deletion(-) create mode 100644 Test/Serial.lean diff --git a/Test/Common.lean b/Test/Common.lean index 3998293..ce21ce8 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -130,6 +130,8 @@ def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done +def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := + t.run LSpec.TestSeq.done def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := diff --git a/Test/Main.lean b/Test/Main.lean index 25bb0d9..6bf410e 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,11 +1,12 @@ import LSpec +import Test.Delate import Test.Environment import Test.Frontend import Test.Integration import Test.Library import Test.Metavar import Test.Proofs -import Test.Delate +import Test.Serial import Test.Tactic -- Test running infrastructure @@ -51,6 +52,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Delate", Delate.suite env_default), + ("Serial", Serial.suite env_default), ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), diff --git a/Test/Serial.lean b/Test/Serial.lean new file mode 100644 index 0000000..4cca464 --- /dev/null +++ b/Test/Serial.lean @@ -0,0 +1,56 @@ +import LSpec +import Test.Common +import Lean +import Pantograph.Library + +open Lean + +namespace Pantograph.Test.Serial + +structure MultiState where + coreContext : Core.Context + coreStates : Array Core.State + +abbrev TestM := StateRefT MultiState $ TestT $ EIO LSpec.TestSeq + +def runCoreM { α } (id : Nat) (testCoreM: TestT CoreM α) : TestM α := do + let multiState ← get + let state ← match multiState.coreStates[id]? with + | .some state => pure state + | .none => + let test := LSpec.test "Invalid index" (id < multiState.coreStates.size) + throw test + let coreM := runTestWithResult testCoreM + match ← (coreM.run' multiState.coreContext state).toBaseIO with + | .error _ => do + let test := LSpec.test "Exception" false + throw test + | .ok (a, tests) => do + set $ (← getThe LSpec.TestSeq) ++ tests + return a + +def simple : TestM Unit := do + return + +structure Test where + name : String + nInstances : Nat + routine: TestM Unit + +protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do + -- Create the state + let state : MultiState := { + coreContext := ← createCoreContext #[], + coreStates := Array.range test.nInstances |>.map λ _ => { env }, + } + match ← (runTest $ test.routine.run' state).toBaseIO with + | .ok e => return e + | .error e => return e + +def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := + let tests: List Test := [ + { name := "simple", nInstances := 2, routine := simple } + ] + tests.map (fun test => (test.name, test.run env)) + +end Pantograph.Test.Serial From 0f946880ae87a5b746b188dcc946ee8c2cbefa8b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 4 Dec 2024 10:44:33 -0800 Subject: [PATCH 05/45] test: Environment pickling --- Pantograph/Serial.lean | 4 +-- Repl.lean | 4 +-- Test/Common.lean | 9 +++++- Test/Serial.lean | 73 ++++++++++++++++++++++++++++++------------ 4 files changed, 64 insertions(+), 26 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 2f04bdb..e60fc54 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -55,7 +55,7 @@ and when unpickling, we build a fresh `Environment` from the imports, and then add the new constants. -/ @[export pantograph_env_pickle_m] -def env_pickle (env : Environment) (path : System.FilePath) : IO Unit := +def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit := Pantograph.pickle path (env.header.imports, env.constants.map₂) /-- @@ -65,7 +65,7 @@ We construct a fresh `Environment` with the relevant imports, and then replace the new constants. -/ @[export pantograph_env_unpickle_m] -def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do +def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path let env ← importModules imports {} 0 return (← env.replay (Std.HashMap.ofList map₂.toList), region) diff --git a/Repl.lean b/Repl.lean index e162f05..f0572a1 100644 --- a/Repl.lean +++ b/Repl.lean @@ -90,10 +90,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do let env ← Lean.MonadEnv.getEnv - env_pickle env args.path + environmentPickle env args.path return .ok {} env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do - let (env, _) ← env_unpickle args.path + let (env, _) ← environmentUnpickle args.path Lean.setEnv env return .ok {} expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do diff --git a/Test/Common.lean b/Test/Common.lean index ce21ce8..0a0b44c 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -125,9 +125,16 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do abbrev TestT := StateT LSpec.TestSeq -def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do +def addTest [Monad m] (test: LSpec.TestSeq) : TestT m Unit := do set $ (← get) ++ test +def checkEq [Monad m] [DecidableEq α] (desc : String) (lhs rhs : α) : TestT m Unit := do + addTest $ LSpec.check desc (lhs == rhs) +def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do + addTest $ LSpec.check desc flag +def fail [Monad m] (desc : String) : TestT m Unit := do + addTest $ LSpec.check desc false + def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := diff --git a/Test/Serial.lean b/Test/Serial.lean index 4cca464..d1ce661 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -7,30 +7,60 @@ open Lean namespace Pantograph.Test.Serial +def tempPath : IO System.FilePath := do + Prod.snd <$> IO.FS.createTempFile + structure MultiState where coreContext : Core.Context - coreStates : Array Core.State + env: Environment -abbrev TestM := StateRefT MultiState $ TestT $ EIO LSpec.TestSeq +abbrev TestM := TestT $ StateRefT MultiState $ IO -def runCoreM { α } (id : Nat) (testCoreM: TestT CoreM α) : TestM α := do - let multiState ← get - let state ← match multiState.coreStates[id]? with - | .some state => pure state - | .none => - let test := LSpec.test "Invalid index" (id < multiState.coreStates.size) - throw test +instance : MonadEnv TestM where + getEnv := return (← getThe MultiState).env + modifyEnv f := do modifyThe MultiState fun s => { s with env := f s.env } + +def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM (α × Core.State) := do + let multiState ← getThe MultiState let coreM := runTestWithResult testCoreM - match ← (coreM.run' multiState.coreContext state).toBaseIO with - | .error _ => do - let test := LSpec.test "Exception" false - throw test - | .ok (a, tests) => do + match ← (coreM.run multiState.coreContext state).toBaseIO with + | .error e => do + throw $ .userError $ ← e.toMessageData.toString + | .ok ((a, tests), state') => do set $ (← getThe LSpec.TestSeq) ++ tests - return a + return (a, state') -def simple : TestM Unit := do - return +def test_environment_pickling : TestM Unit := do + let stateSrc: Core.State := { env := ← getEnv } + let stateDst: Core.State := { env := ← getEnv } + + let name := `mystery + let envPicklePath ← tempPath + let ((), _) ← runCoreM stateSrc do + let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default + let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default + let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx + (name := name) + (levelParams := []) + (type := type) + (value := value) + (hints := Lean.mkReducibilityHintsRegularEx 1) + (safety := Lean.DefinitionSafety.safe) + (all := []) + let env' ← match (← getEnv).addDecl (← getOptions) c with + | .error e => do + let error ← (e.toMessageData (← getOptions)).toString + throwError error + | .ok env' => pure env' + environmentPickle env' envPicklePath + + let _ ← runCoreM stateDst do + let (env', _) ← environmentUnpickle envPicklePath + checkTrue s!"Has symbol {name}" (env'.find? name).isSome + let anotherName := `mystery2 + checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone + + IO.FS.removeFile envPicklePath structure Test where name : String @@ -41,15 +71,16 @@ protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq : -- Create the state let state : MultiState := { coreContext := ← createCoreContext #[], - coreStates := Array.range test.nInstances |>.map λ _ => { env }, + env, } - match ← (runTest $ test.routine.run' state).toBaseIO with + match ← ((runTest $ test.routine).run' state).toBaseIO with | .ok e => return e - | .error e => return e + | .error e => + return LSpec.check "Emitted exception" (e.toString == "") def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := let tests: List Test := [ - { name := "simple", nInstances := 2, routine := simple } + { name := "environment_pickling", nInstances := 2, routine := test_environment_pickling }, ] tests.map (fun test => (test.name, test.run env)) From 105fb7af4bed8da4969ef1265106c239861dece9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 14:23:55 -0800 Subject: [PATCH 06/45] feat: Goal state pickling --- Pantograph/Serial.lean | 89 ++++++++++++++++++++++++++++++++++++++++++ Test/Serial.lean | 36 +++++++++++++---- 2 files changed, 118 insertions(+), 7 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index e60fc54..bd01169 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -2,6 +2,7 @@ import Lean.Environment import Lean.Replay import Init.System.IOError import Std.Data.HashMap +import Pantograph.Goal /-! Input/Output functions @@ -70,4 +71,92 @@ def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedR let env ← importModules imports {} 0 return (← env.replay (Std.HashMap.ofList map₂.toList), region) + +open Lean.Core in +structure CompactCoreState where + -- env : Environment + nextMacroScope : MacroScope := firstFrontendMacroScope + 1 + ngen : NameGenerator := {} + -- traceState : TraceState := {} + -- cache : Cache := {} + -- messages : MessageLog := {} + -- infoState : Elab.InfoState := {} + +@[export pantograph_goal_state_pickle_m] +def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit := + let { + savedState := { + term := { + meta := { + core, + meta, + } + «elab», + }, + tactic + } + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + } := goalState + --let env := core.env + Pantograph.pickle path ( + ({ core with } : CompactCoreState), + meta, + «elab», + tactic, + + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + ) + +@[export pantograph_goal_state_unpickle_m] +def goalStateUnpickle (path : System.FilePath) (env : Environment) + : IO (GoalState × CompactedRegion) := unsafe do + let (( + compactCore, + meta, + «elab», + tactic, + + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + ), region) ← Pantograph.unpickle ( + CompactCoreState × + Meta.State × + Elab.Term.State × + Elab.Tactic.State × + + MVarId × + Option MVarId × + Option (MVarId × MVarId × List MVarId) × + Option (MVarId × Expr) + ) path + let goalState := { + savedState := { + term := { + meta := { + core := { + compactCore with + passedHeartbeats := 0, + env, + }, + meta, + }, + «elab», + }, + tactic, + }, + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + } + return (goalState, region) + end Pantograph diff --git a/Test/Serial.lean b/Test/Serial.lean index d1ce661..fcdc155 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -31,12 +31,12 @@ def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM ( return (a, state') def test_environment_pickling : TestM Unit := do - let stateSrc: Core.State := { env := ← getEnv } - let stateDst: Core.State := { env := ← getEnv } + let coreSrc : Core.State := { env := ← getEnv } + let coreDst : Core.State := { env := ← getEnv } let name := `mystery let envPicklePath ← tempPath - let ((), _) ← runCoreM stateSrc do + let ((), _) ← runCoreM coreSrc do let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx @@ -54,7 +54,7 @@ def test_environment_pickling : TestM Unit := do | .ok env' => pure env' environmentPickle env' envPicklePath - let _ ← runCoreM stateDst do + let _ ← runCoreM coreDst do let (env', _) ← environmentUnpickle envPicklePath checkTrue s!"Has symbol {name}" (env'.find? name).isSome let anotherName := `mystery2 @@ -62,9 +62,30 @@ def test_environment_pickling : TestM Unit := do IO.FS.removeFile envPicklePath +def test_goal_state_pickling_simple : TestM Unit := do + let coreSrc : Core.State := { env := ← getEnv } + let coreDst : Core.State := { env := ← getEnv } + let statePath ← tempPath + + let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default + let stateGenerate : MetaM GoalState := runTermElabMInMeta do + GoalState.create type + + let ((), _) ← runCoreM coreSrc do + let state ← stateGenerate.run' + goalStatePickle state statePath + + let ((), _) ← runCoreM coreDst do + let (goalState, _) ← goalStateUnpickle statePath (← getEnv) + let metaM : MetaM (List Expr) := do + goalState.goals.mapM λ goal => goalState.withContext goal goal.getType + let types ← metaM.run' + checkTrue "Goals" $ types[0]!.equal type + + IO.FS.removeFile statePath + structure Test where name : String - nInstances : Nat routine: TestM Unit protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do @@ -76,11 +97,12 @@ protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq : match ← ((runTest $ test.routine).run' state).toBaseIO with | .ok e => return e | .error e => - return LSpec.check "Emitted exception" (e.toString == "") + return LSpec.check s!"Emitted exception: {e.toString}" (e.toString == "") def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := let tests: List Test := [ - { name := "environment_pickling", nInstances := 2, routine := test_environment_pickling }, + { name := "environment_pickling", routine := test_environment_pickling, }, + { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, }, ] tests.map (fun test => (test.name, test.run env)) From c54ce93ef5eb745a3db7668886f35ed034f42afb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 14:31:43 -0800 Subject: [PATCH 07/45] feat: Goal State IO in REPL --- Pantograph/Protocol.lean | 13 +++++++++++++ Repl.lean | 36 +++++++++++++++++++++++------------- 2 files changed, 36 insertions(+), 13 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index fcd5ebe..0cb6cac 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -289,6 +289,19 @@ structure GoalDiag where instantiate: Bool := true printSexp: Bool := false +structure GoalSave where + id: Nat + path: System.FilePath + deriving Lean.FromJson +structure GoalSaveResult where + deriving Lean.ToJson +structure GoalLoad where + path: System.FilePath + deriving Lean.FromJson +structure GoalLoadResult where + id: Nat + deriving Lean.ToJson + /-- Executes the Lean compiler on a single file -/ structure FrontendProcess where diff --git a/Repl.lean b/Repl.lean index f0572a1..3f8a3c6 100644 --- a/Repl.lean +++ b/Repl.lean @@ -15,6 +15,16 @@ structure State where /-- Main state monad for executing commands -/ abbrev MainM := ReaderT Context (StateT State Lean.CoreM) +def newGoalState (goalState: GoalState) : MainM Nat := do + let state ← get + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } + return stateId + + -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α @@ -50,6 +60,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "goal.continue" => run goal_continue | "goal.delete" => run goal_delete | "goal.print" => run goal_print + | "goal.save" => run goal_save + | "goal.load" => run goal_load | "frontend.process" => run frontend_process | cmd => let error: Protocol.InteractionError := @@ -62,14 +74,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorCommand := errorI "command" errorIndex := errorI "index" errorIO := errorI "io" - newGoalState (goalState: GoalState) : MainM Nat := do - let state ← get - let stateId := state.nextId - set { state with - goalStates := state.goalStates.insert stateId goalState, - nextId := state.nextId + 1 - } - return stateId -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -203,11 +207,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match nextState? with | .error error => return .error <| errorI "structure" error | .ok nextGoalState => - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert nextStateId nextGoalState, - nextId := state.nextId + 1 - } + let nextStateId ← newGoalState nextGoalState let goals ← goalSerialize nextGoalState (options := state.options) return .ok { nextStateId, @@ -224,6 +224,16 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .error $ errorIndex s!"Invalid state index {args.stateId}" let result ← runMetaInMainM <| goalPrint goalState state.options return .ok result + goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do + let state ← get + let .some goalState := state.goalStates[args.id]? | + return .error $ errorIndex s!"Invalid state index {args.id}" + goalStatePickle goalState args.path + return .ok {} + goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do + let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv) + let id ← newGoalState goalState + return .ok { id } frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do let options := (← get).options try From 3da85b7f04fda00d98222f4f988d05461cd03dc1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 16:00:46 -0800 Subject: [PATCH 08/45] doc: Documentation for save/load --- README.md | 57 +----------------------------------------------- doc/repl.md | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 64 insertions(+), 56 deletions(-) create mode 100644 doc/repl.md diff --git a/README.md b/README.md index 04213ae..5fec564 100644 --- a/README.md +++ b/README.md @@ -64,62 +64,7 @@ stat ``` where the application of `assumption` should lead to a failure. -### Commands - -See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. -* `reset`: Delete all cached expressions and proof trees -* `stat`: Display resource usage -* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the - type of an expression and format it. -* `env.catalog`: Display a list of all safe Lean symbols in the current environment -* `env.inspect {"name": , "value": }`: Show the type and package of a - given symbol; If value flag is set, the value is printed or hidden. By default - only the values of definitions are printed. -* `options.set { key: value, ... }`: Set one or more options (not Lean options; those - have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - - One particular option for interest for machine learning researchers is the - automatic mode (flag: `"automaticMode"`). By default it is turned on, with - all goals automatically resuming. This makes Pantograph act like a gym, - with no resumption necessary to manage your goals. -* `options.print`: Display the current set of options -* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: - Start a new proof from a given expression or symbol -* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a - given goal. The tactic is supplied as additional key-value pairs in one of the following formats: - - `{ "tactic": }`: Execute an ordinary tactic - - `{ "expr": }`: Assign the given proof term to the current goal - - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal - - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must - be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set - to the previous `rhs`. - - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of - exit, the goal id is ignored. -* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: - Execute continuation/resumption - - `{ "branch": }`: Continue on branch state. The current state must have no goals. - - `{ "goals": }`: Resume the given goals -* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list -* `goal.print {"stateId": }"`: Print a goal state -* `frontend.process { ["fileName": ",] ["file": ], invocations: - , sorrys: }`: Executes the Lean frontend on a file, collecting - either the tactic invocations (`"invocations": true`) or the sorrys into goal - states (`"sorrys": true`) - -### Errors - -When an error pertaining to the execution of a command happens, the returning JSON structure is - -``` json -{ "error": "type", "desc": "description" } -``` -Common error forms: -* `command`: Indicates malformed command structure which results from either - invalid command or a malformed JSON structure that cannot be fed to an - individual command. -* `index`: Indicates an invariant maintained by the output of one command and - input of another is broken. For example, attempting to query a symbol not - existing in the library or indexing into a non-existent proof state. +For a list of commands, see [REPL Documentation](doc/repl.md). ### Project Environment diff --git a/doc/repl.md b/doc/repl.md new file mode 100644 index 0000000..a31db4f --- /dev/null +++ b/doc/repl.md @@ -0,0 +1,63 @@ +# REPL + +## Commands + +See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. +* `reset`: Delete all cached expressions and proof trees +* `stat`: Display resource usage +* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the + type of an expression and format it. +* `env.catalog`: Display a list of all safe Lean symbols in the current environment +* `env.inspect {"name": , "value": }`: Show the type and package of a + given symbol; If value flag is set, the value is printed or hidden. By default + only the values of definitions are printed. +* `env.save { path }`, `env.load { path }`: Save/Load the current environment + to/from a file +* `options.set { key: value, ... }`: Set one or more options (not Lean options; those + have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` + + One particular option for interest for machine learning researchers is the + automatic mode (flag: `"automaticMode"`). By default it is turned on, with + all goals automatically resuming. This makes Pantograph act like a gym, + with no resumption necessary to manage your goals. +* `options.print`: Display the current set of options +* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: + Start a new proof from a given expression or symbol +* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a + given goal. The tactic is supplied as additional key-value pairs in one of the following formats: + - `{ "tactic": }`: Execute an ordinary tactic + - `{ "expr": }`: Assign the given proof term to the current goal + - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal + - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must + be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set + to the previous `rhs`. + - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of + exit, the goal id is ignored. +* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: + Execute continuation/resumption + - `{ "branch": }`: Continue on branch state. The current state must have no goals. + - `{ "goals": }`: Resume the given goals +* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list +* `goal.print {"stateId": }"`: Print a goal state +* `goal.save`{ id, path }, `env.load { path }`: Save/Load a goal state to/from a + file. The environment is not carried with the state. The user is responsible + to ensure the sender/receiver instances share the same environment. +* `frontend.process { ["fileName": ",] ["file": ], invocations: + , sorrys: }`: Executes the Lean frontend on a file, collecting + either the tactic invocations (`"invocations": true`) or the sorrys into goal + states (`"sorrys": true`) + +## Errors + +When an error pertaining to the execution of a command happens, the returning JSON structure is + +``` json +{ "error": "type", "desc": "description" } +``` +Common error forms: +* `command`: Indicates malformed command structure which results from either + invalid command or a malformed JSON structure that cannot be fed to an + individual command. +* `index`: Indicates an invariant maintained by the output of one command and + input of another is broken. For example, attempting to query a symbol not + existing in the library or indexing into a non-existent proof state. From bfdc7dd39ee008506dafb010725fc192ccbe5287 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 16:02:00 -0800 Subject: [PATCH 09/45] doc: Fix code environment --- doc/repl.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/repl.md b/doc/repl.md index a31db4f..978bad2 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -39,7 +39,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `{ "goals": }`: Resume the given goals * `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state -* `goal.save`{ id, path }, `env.load { path }`: Save/Load a goal state to/from a +* `goal.save{ id, path }`, `goal.load { path }`: Save/Load a goal state to/from a file. The environment is not carried with the state. The user is responsible to ensure the sender/receiver instances share the same environment. * `frontend.process { ["fileName": ",] ["file": ], invocations: From d00e3769430c1fe5df0c2528768738617a29efd2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 17:18:35 -0800 Subject: [PATCH 10/45] doc: Remove outdated documentation --- .gitignore | 6 ++---- README.md | 2 +- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index 21bcd46..53ec3bb 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,4 @@ .* !.gitignore - -*.olean -/build -/lake-packages +*.[io]lean +/result diff --git a/README.md b/README.md index 5fec564..47456ea 100644 --- a/README.md +++ b/README.md @@ -75,7 +75,7 @@ the environment might be setup like this: ``` sh LIB="../lib" -LIB_MATHLIB="$LIB/mathlib4/lake-packages" +LIB_MATHLIB="$LIB/mathlib4/.lake" export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ From 95408d1d523aa679b544568112da8535506d14e2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 17:21:06 -0800 Subject: [PATCH 11/45] doc: Unify types --- doc/repl.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/doc/repl.md b/doc/repl.md index 978bad2..464c7cc 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -11,8 +11,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va * `env.inspect {"name": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default only the values of definitions are printed. -* `env.save { path }`, `env.load { path }`: Save/Load the current environment - to/from a file +* `env.save { "path": }`, `env.load { "path": }`: Save/Load the + current environment to/from a file * `options.set { key: value, ... }`: Set one or more options (not Lean options; those have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` @@ -39,10 +39,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `{ "goals": }`: Resume the given goals * `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state -* `goal.save{ id, path }`, `goal.load { path }`: Save/Load a goal state to/from a - file. The environment is not carried with the state. The user is responsible - to ensure the sender/receiver instances share the same environment. -* `frontend.process { ["fileName": ",] ["file": ], invocations: +* `goal.save { "id": , "path": }`, `goal.load { "path": }`: + Save/Load a goal state to/from a file. The environment is not carried with the + state. The user is responsible to ensure the sender/receiver instances share + the same environment. +* `frontend.process { ["fileName": ,] ["file": ], invocations: , sorrys: }`: Executes the Lean frontend on a file, collecting either the tactic invocations (`"invocations": true`) or the sorrys into goal states (`"sorrys": true`) From 2e2658bde79aa02c6593371e098a924488ba98bf Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 21:35:37 -0800 Subject: [PATCH 12/45] test: Add test case for composite tactic --- Test/Proofs.lean | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 02c1bf6..8db8f19 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -14,10 +14,7 @@ inductive Start where | copy (name: String) -- Start from some name in the environment | expr (expr: String) -- Start from some expression -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) - -def addTest (test: LSpec.TestSeq): TestM Unit := do - set $ (← get) ++ test +abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM def startProof (start: Start): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv @@ -704,6 +701,25 @@ def test_nat_zero_add_alt: TestM Unit := do } ]) +def test_composite_tactic_failure: TestM Unit := do + let state? ← startProof (.expr "∀ (p : Prop), ∃ (x : Nat), p") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let tactic := "intro p" + let state1 ← match ← state0.tacticOn 0 tactic with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + let tactic := "exact ⟨0, by simp⟩" + let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" + checkEq tactic messages #["placeholder"] + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("identity", test_identity), @@ -716,6 +732,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("calc", test_calc), ("Nat.zero_add", test_nat_zero_add), ("Nat.zero_add alt", test_nat_zero_add_alt), + ("composite tactic failure", test_composite_tactic_failure), ] tests.map (fun (name, test) => (name, proofRunner env test)) From 7aafd6956fe71770a356f3d852edc4e91cd5696a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:07:21 -0800 Subject: [PATCH 13/45] fix: Capture composite tactic failure --- Pantograph/Goal.lean | 5 +++++ Test/Common.lean | 22 ++++++++++++++-------- Test/Proofs.lean | 4 ++-- 3 files changed, 21 insertions(+), 10 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 79e3004..be745f4 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -73,6 +73,8 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances } protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta +protected def GoalState.coreState (state: GoalState): Core.SavedState := + state.savedState.term.meta.core protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState @@ -207,6 +209,9 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E Elab.TermElabM TacticResult := do try let nextState ← state.step goal tacticM + let newMessages ← (← getThe Core.State).messages.toList.drop (state.coreState.messages.toList.length) |>.mapM λ m => m.toString + if ¬ newMessages.isEmpty then + return .failure newMessages.toArray return .success nextState catch exception => return .failure #[← exception.toMessageData.toString] diff --git a/Test/Common.lean b/Test/Common.lean index 0a0b44c..212e164 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -123,23 +123,29 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do -- Monadic testing -abbrev TestT := StateT LSpec.TestSeq +abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq -def addTest [Monad m] (test: LSpec.TestSeq) : TestT m Unit := do +section Monadic + +variable [Monad m] [MonadLiftT (ST IO.RealWorld) m] + +def addTest (test: LSpec.TestSeq) : TestT m Unit := do set $ (← get) ++ test -def checkEq [Monad m] [DecidableEq α] (desc : String) (lhs rhs : α) : TestT m Unit := do - addTest $ LSpec.check desc (lhs == rhs) -def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do +def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do + addTest $ LSpec.check desc (lhs = rhs) +def checkTrue (desc : String) (flag : Bool) : TestT m Unit := do addTest $ LSpec.check desc flag -def fail [Monad m] (desc : String) : TestT m Unit := do +def fail (desc : String) : TestT m Unit := do addTest $ LSpec.check desc false -def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := +def runTest (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done -def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := +def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) := t.run LSpec.TestSeq.done +end Monadic + def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := runTermElabMSeq env $ runTest t diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8db8f19..65f099f 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -702,7 +702,7 @@ def test_nat_zero_add_alt: TestM Unit := do ]) def test_composite_tactic_failure: TestM Unit := do - let state? ← startProof (.expr "∀ (p : Prop), ∃ (x : Nat), p") + let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)") let state0 ← match state? with | .some state => pure state | .none => do @@ -718,7 +718,7 @@ def test_composite_tactic_failure: TestM Unit := do let tactic := "exact ⟨0, by simp⟩" let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" - checkEq tactic messages #["placeholder"] + checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ From a62ac51c37ad5dde6c3e850aaaf1e9b9265ec652 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:11:37 -0800 Subject: [PATCH 14/45] chore: Remove all redundant filenames --- Pantograph/Goal.lean | 10 ++++------ Test/Common.lean | 6 +++--- Test/Tactic/MotivatedApply.lean | 6 +++--- Test/Tactic/NoConfuse.lean | 6 +++--- Test/Tactic/Prograde.lean | 2 +- 5 files changed, 14 insertions(+), 16 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index be745f4..8d29aa8 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -10,8 +10,6 @@ import Lean namespace Pantograph open Lean -def filename: String := "" - /-- Represents an interconnected set of metavariables, or a state in proof search -/ @@ -224,7 +222,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str (env := ← MonadEnv.getEnv) (catName := if state.isConv then `conv else `tactic) (input := tactic) - (fileName := filename) with + (fileName := ← getFileName) with | .ok stx => pure $ stx | .error error => return .parseError error state.tryTacticM goal $ Elab.Tactic.evalTactic tactic @@ -236,7 +234,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin (env := ← MonadEnv.getEnv) (catName := `term) (input := expr) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalAssign expr @@ -250,7 +248,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St (env := ← MonadEnv.getEnv) (catName := `term) (input := type) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalLet binderName.toName type @@ -337,7 +335,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) (env := state.env) (catName := `term) (input := pred) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error goal.checkNotAssigned `GoalState.tryCalc diff --git a/Test/Common.lean b/Test/Common.lean index 212e164..53adaa0 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -95,19 +95,19 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq) def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e -def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do +def strToTermSyntax (s: String): CoreM Syntax := do let .ok stx := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) | panic! s!"Failed to parse {s}" + (fileName := ← getFileName) | panic! s!"Failed to parse {s}" return stx def parseSentence (s: String): Elab.TermElabM Expr := do let stx ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" Elab.Term.elabTerm (stx := stx) .none diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 4fb05e3..61d7d6c 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -28,7 +28,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@List.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -74,7 +74,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" let expr ← parseSentence expr diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index ac277e2..93f0606 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -15,7 +15,7 @@ def test_nat : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -32,7 +32,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 132718a..b3347cb 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -15,7 +15,7 @@ def test_define : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "Or.inl h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic From 34a4bf5b7321f413e12c1c1cd814d0b0e1a52e29 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:12:04 -0800 Subject: [PATCH 15/45] feat: Export GoalState.tryTactic --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 8d29aa8..ac09109 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -215,6 +215,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E return .failure #[← exception.toMessageData.toString] /-- Execute a string tactic on given state. Restores TermElabM -/ +@[export pantograph_goal_state_try_tactic_m] protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String): Elab.TermElabM TacticResult := do state.restoreElabM From 0415baaaff3a55475cd532749c1fe9724a16fb43 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:16:20 -0800 Subject: [PATCH 16/45] chore: Cleanup old `TestM` --- Test/Metavar.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 506e963..c6fc4f0 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -8,10 +8,7 @@ namespace Pantograph.Test.Metavar open Pantograph open Lean -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) - -def addTest (test: LSpec.TestSeq): TestM Unit := do - set $ (← get) ++ test +abbrev TestM := TestT $ ReaderT Protocol.Options Elab.TermElabM -- Tests that all delay assigned mvars are instantiated def test_instantiate_mvar: TestM Unit := do @@ -32,8 +29,6 @@ def test_instantiate_mvar: TestM Unit := do "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))") return () - - def startProof (expr: String): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv let syn? := parseTerm env expr From 929311a0429c2fafb5533c8f44e326c6d66b4d9c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Dec 2024 00:08:20 -0800 Subject: [PATCH 17/45] fix: Only signal failure when there is error --- Pantograph/Goal.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index ac09109..e190d5d 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -202,12 +202,19 @@ inductive TacticResult where -- The given action cannot be executed in the state | invalidAction (message: String) -/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ +/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit): Elab.TermElabM TacticResult := do try let nextState ← state.step goal tacticM - let newMessages ← (← getThe Core.State).messages.toList.drop (state.coreState.messages.toList.length) |>.mapM λ m => m.toString + + -- Check if error messages have been generated in the core. + let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length + |>.filterMapM λ m => do + if m.severity == .error then + return .some $ ← m.toString + else + return .none if ¬ newMessages.isEmpty then return .failure newMessages.toArray return .success nextState @@ -357,7 +364,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" if let some prevRhs := calcPrevRhs? then unless ← Meta.isDefEqGuarded lhs prevRhs do - throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " + throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- Creates a mvar to represent the proof that the calc tactic solves the -- current branch From 9ede3cf7175db43e1e660f64e58eaac4251eed8b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Dec 2024 15:38:03 -0800 Subject: [PATCH 18/45] feat: InfoTree printing --- Pantograph/Frontend/InfoTree.lean | 73 ++++++++++++++++++++++++------- 1 file changed, 58 insertions(+), 15 deletions(-) diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index 4e60710..aa99db2 100644 --- a/Pantograph/Frontend/InfoTree.lean +++ b/Pantograph/Frontend/InfoTree.lean @@ -1,12 +1,19 @@ -/- Adapted from lean-training-data by semorrison -/ +/- Adapted from lean-training-data -/ import Lean.Elab.InfoTree import Lean.Parser.Term +import Lean.PrettyPrinter open Lean -namespace Lean.Elab.Info +namespace Lean.Elab + +private def elaboratorToString : Name → String + | .anonymous => "" + | n => s!"[{n}]" +private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .) + /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/ -protected def stx? : Info → Option Syntax +protected def Info.stx? : Info → Option Syntax | .ofTacticInfo info => info.stx | .ofTermInfo info => info.stx | .ofCommandInfo info => info.stx @@ -20,24 +27,35 @@ protected def stx? : Info → Option Syntax | .ofFieldRedeclInfo info => info.stx | .ofOmissionInfo info => info.stx /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/ -protected def isOriginal (i : Info) : Bool := +protected def Info.isOriginal (i : Info) : Bool := match i.stx? with | none => true -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative. | some stx => match stx.getHeadInfo with | .original .. => true | _ => false -end Lean.Elab.Info -namespace Lean.Elab.TacticInfo +def ContextInfo.ppExpr (ctx : ContextInfo) (lctx : LocalContext) (e : Expr) : IO Format := + ctx.runMetaM lctx (do Meta.ppExpr (← instantiateMVars e)) + +def CommandInfo.toString (info : CommandInfo) (ctx : ContextInfo) : IO String := do + let stx := (← ctx.ppSyntax {} info.stx).pretty + return s!"{stx}\n{elaboratorToString info.elaborator}" + +def TermInfo.toString (info : TermInfo) (ctx : ContextInfo) : IO String := do + let stx := (← ctx.ppSyntax info.lctx info.stx).pretty + let expectedType ← info.expectedType?.mapM fun ty => do + pure s!": {(← ctx.ppExpr info.lctx ty).pretty}" + let expr := (← ctx.ppExpr info.lctx info.expr).pretty + return s!"{stx}\n{elaboratorToString info.elaborator}{expr}{expectedType}" /-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/ -def name? (t : TacticInfo) : Option Name := +def TacticInfo.name? (t : TacticInfo) : Option Name := match t.stx with | Syntax.node _ n _ => some n | _ => none /-- Decide whether a tactic is "substantive", or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/ -def isSubstantive (t : TacticInfo) : Bool := +def TacticInfo.isSubstantive (t : TacticInfo) : Bool := match t.name? with | none => false | some `null => false @@ -49,17 +67,22 @@ def isSubstantive (t : TacticInfo) : Bool := | some ``Lean.Parser.Tactic.«tactic_<;>_» => false | some ``Lean.Parser.Tactic.paren => false | _ => true - -end Lean.Elab.TacticInfo - -namespace Lean.Elab.InfoTree +def TacticInfo.pp (info : TacticInfo) (ctx : ContextInfo) : IO Format := + ctx.runMetaM {} try + Lean.PrettyPrinter.ppTactic ⟨info.stx⟩ + catch _ => + pure "" +def TacticInfo.toString (i : TacticInfo) (ctx : ContextInfo) : IO String := do + let name := i.name? + let stx := Format.pretty (← i.pp ctx) + return s!"{stx}\n{name} {stx}" /-- Keep `.node` nodes and `.hole` nodes satisfying predicates. Returns a `List InfoTree`, although in most situations this will be a singleton. -/ -partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : +partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : InfoTree → List InfoTree | .context ctx tree => tree.filter p m |>.map (.context ctx) | .node info children => @@ -70,7 +93,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : | .hole mvar => if m mvar then [.hole mvar] else [] /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ -partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) : +partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) : List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) := match t with | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred @@ -78,4 +101,24 @@ partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) | _ => [] -end Lean.Elab.InfoTree +@[export pantograph_infotree_to_string_m] +partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo) : IO String := do + match t with + | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?) + | .node info children => + if let some ctx := ctx? then + let node : Option String ← match info with + | .ofTermInfo info => some <$> (do pure <| s!"[term] {(← info.toString ctx)}") + | .ofCommandInfo info => some <$> (do pure <| s!"[command] {(← info.toString ctx)}") + | .ofTacticInfo info => some <$> (do pure <| s!"[tactic] {(← info.toString ctx)}") + | _ => pure none + let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx) + return s!"{node}\n{children}" + else throw <| IO.userError "No `ContextInfo` available." + | .hole mvarId => + if let some ctx := ctx? then + let payload := (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty + return s!"[hole] {payload}" + else throw <| IO.userError "No `ContextInfo` available." + +end Lean.Elab From b950dc9b1a278aabfb7fb2a19be60d7b1e636494 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Dec 2024 22:51:55 -0800 Subject: [PATCH 19/45] fix: Verbose printing of infotree --- Pantograph/Frontend/InfoTree.lean | 32 +++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index aa99db2..3b57a54 100644 --- a/Pantograph/Frontend/InfoTree.lean +++ b/Pantograph/Frontend/InfoTree.lean @@ -9,7 +9,7 @@ namespace Lean.Elab private def elaboratorToString : Name → String | .anonymous => "" - | n => s!"[{n}]" + | n => s!"⟨{n}⟩ " private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .) /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/ @@ -39,14 +39,14 @@ def ContextInfo.ppExpr (ctx : ContextInfo) (lctx : LocalContext) (e : Expr) : IO def CommandInfo.toString (info : CommandInfo) (ctx : ContextInfo) : IO String := do let stx := (← ctx.ppSyntax {} info.stx).pretty - return s!"{stx}\n{elaboratorToString info.elaborator}" + return s!"{elaboratorToString info.elaborator}\n{stx}" def TermInfo.toString (info : TermInfo) (ctx : ContextInfo) : IO String := do let stx := (← ctx.ppSyntax info.lctx info.stx).pretty - let expectedType ← info.expectedType?.mapM fun ty => do - pure s!": {(← ctx.ppExpr info.lctx ty).pretty}" + let expectedType := (← info.expectedType?.mapM fun ty => do + pure s!": {(← ctx.ppExpr info.lctx ty).pretty}").getD "" let expr := (← ctx.ppExpr info.lctx info.expr).pretty - return s!"{stx}\n{elaboratorToString info.elaborator}{expr}{expectedType}" + return s!"{elaboratorToString info.elaborator}{expr}{expectedType}\n{stx}" /-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/ def TacticInfo.name? (t : TacticInfo) : Option Name := @@ -75,7 +75,7 @@ def TacticInfo.pp (info : TacticInfo) (ctx : ContextInfo) : IO Format := def TacticInfo.toString (i : TacticInfo) (ctx : ContextInfo) : IO String := do let name := i.name? let stx := Format.pretty (← i.pp ctx) - return s!"{stx}\n{name} {stx}" + return s!"{name}\n{stx}" /-- Keep `.node` nodes and `.hole` nodes satisfying predicates. @@ -102,16 +102,24 @@ partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextIn | _ => [] @[export pantograph_infotree_to_string_m] -partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo) : IO String := do +partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do match t with | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?) | .node info children => if let some ctx := ctx? then - let node : Option String ← match info with - | .ofTermInfo info => some <$> (do pure <| s!"[term] {(← info.toString ctx)}") - | .ofCommandInfo info => some <$> (do pure <| s!"[command] {(← info.toString ctx)}") - | .ofTacticInfo info => some <$> (do pure <| s!"[tactic] {(← info.toString ctx)}") - | _ => pure none + let node : String ← match info with + | .ofTermInfo info => pure s!"[term] {(← info.toString ctx)}" + | .ofCommandInfo info => pure s!"[command] {(← info.toString ctx)}" + | .ofTacticInfo info => pure s!"[tactic] {(← info.toString ctx)}" + | .ofMacroExpansionInfo _ => pure "[macro_exp]" + | .ofOptionInfo _ => pure "[option]" + | .ofFieldInfo _ => pure "[field]" + | .ofCompletionInfo _ => pure "[completion]" + | .ofUserWidgetInfo _ => pure "[user_widget]" + | .ofCustomInfo _ => pure "[custom]" + | .ofFVarAliasInfo _ => pure "[fvar]" + | .ofFieldRedeclInfo _ => pure "[field_redecl]" + | .ofOmissionInfo _ => pure "[omission]" let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx) return s!"{node}\n{children}" else throw <| IO.userError "No `ContextInfo` available." From ea813e5bc5d0116d09d9e8f43c3213fa33b2ae4d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Dec 2024 23:21:36 -0800 Subject: [PATCH 20/45] feat: Monadic info collection --- Pantograph/Frontend/Elab.lean | 26 ++++++++++++++++---------- Pantograph/Frontend/InfoTree.lean | 29 +++++++++++++++++++++++++---- Repl.lean | 4 ++-- Test/Frontend.lean | 12 +++++++++++- 4 files changed, 54 insertions(+), 17 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index b3173a7..6bc67f3 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -67,7 +67,7 @@ end TacticInvocation /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, each equipped with its relevant `ContextInfo`, and any children info trees. -/ private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation := - let infos := t.findAllInfo none fun i => match i with + let infos := t.findAllInfo none false fun i => match i with | .ofTacticInfo _ => true | _ => false infos.filterMap fun p => match p with @@ -101,21 +101,27 @@ structure InfoWithContext where info: Elab.Info context?: Option Elab.ContextInfo := .none -private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext := - let infos := t.findAllInfo none fun i => match i with - | .ofTermInfo { expectedType?, expr, stx, .. } => - expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry +private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do + let infos ← t.findAllInfoM none true fun i ctx? => match i with + | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do + let .some expectedType := expectedType? | return false + let .some ctx := ctx? | return false + if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then + return true + ctx.runMetaM lctx do + let type ← Meta.inferType expr + Bool.not <$> Meta.isDefEq type expectedType | .ofTacticInfo { stx, goalsBefore, .. } => -- The `sorry` term is distinct from the `sorry` tactic let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry - isSorry ∧ !goalsBefore.isEmpty - | _ => false - infos.map fun (info, context?, _) => { info, context? } + return isSorry ∧ !goalsBefore.isEmpty + | _ => return false + return infos.map fun (info, context?, _) => { info, context? } -- NOTE: Plural deliberately not spelled "sorries" @[export pantograph_frontend_collect_sorrys_m] -def collectSorrys (step: CompilationStep) : List InfoWithContext := - step.trees.bind collectSorrysInTree +def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do + return (← step.trees.mapM collectSorrysInTree).join diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index 3b57a54..c72dbe6 100644 --- a/Pantograph/Frontend/InfoTree.lean +++ b/Pantograph/Frontend/InfoTree.lean @@ -93,14 +93,35 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ => | .hole mvar => if m mvar then [.hole mvar] else [] /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ -partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) : - List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) := +partial def InfoTree.findAllInfo + (t : InfoTree) + (context?: Option Elab.ContextInfo) + (haltOnMatch : Bool := false) + (pred : Elab.Info → Bool) + : List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) := match t with - | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred + | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred | .node i children => - (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) + let head := if pred i then [(i, context?, children)] else [] + let tail := if haltOnMatch then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred) + head ++ tail | _ => [] +/-- Monadic analogue of `findAllInfo` -/ +partial def InfoTree.findAllInfoM [Monad m] + (t : InfoTree) + (context?: Option Elab.ContextInfo) + (haltOnMatch : Bool) + (pred : Elab.Info → Option Elab.ContextInfo → m Bool) + : m (List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree)) := do + match t with + | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred + | .node i children => + let head := if ← pred i context? then [(i, context?, children)] else [] + let tail := if haltOnMatch then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred) + return head ++ (← tail).join + | _ => return [] + @[export pantograph_infotree_to_string_m] partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do match t with diff --git a/Repl.lean b/Repl.lean index 3f8a3c6..f1c8f42 100644 --- a/Repl.lean +++ b/Repl.lean @@ -257,10 +257,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do pure $ .some invocations else pure .none - let sorrys := if args.sorrys then + let sorrys ← if args.sorrys then Frontend.collectSorrys step else - [] + pure [] let messages ← step.messageStrings return (step.before, boundary, invocations?, sorrys, messages) let li ← frontendM.run context |>.run' state diff --git a/Test/Frontend.lean b/Test/Frontend.lean index 015cfa8..a03b283 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -10,7 +10,9 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do let filename := "" let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} let m := Frontend.mapCompilationSteps λ step => do - return (step.before, Frontend.collectSorrys step) + for tree in step.trees do + IO.println s!"{← tree.toString}" + return (step.before, ← Frontend.collectSorrys step) let li ← m.run context |>.run' state let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do if sorrys.isEmpty then @@ -177,6 +179,13 @@ example (n: Nat) : mystery n + 1 = n + 2 := sorry } ]) +def test_capture_type_mismatch : TestT MetaM Unit := do + let input := " +def mystery : Nat := true + " + let goalStates ← (collectSorrysFromSource input).run' {} + let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" + def suite (env : Environment): List (String × IO LSpec.TestSeq) := let tests := [ @@ -185,6 +194,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) := ("sorry_in_induction", test_sorry_in_induction), ("sorry_in_coupled", test_sorry_in_coupled), ("environment_capture", test_environment_capture), + ("capture_type_mismatch", test_capture_type_mismatch), ] tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test)) From 17ab2eafd8868652d83072f074696413825ebab5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 00:03:53 -0800 Subject: [PATCH 21/45] fix: Halt on match guard --- Pantograph/Frontend/Elab.lean | 2 -- Pantograph/Frontend/InfoTree.lean | 4 ++-- Test/Frontend.lean | 2 -- 3 files changed, 2 insertions(+), 6 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 6bc67f3..d5af8b5 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -123,8 +123,6 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do return (← step.trees.mapM collectSorrysInTree).join - - /-- Since we cannot directly merge `MetavarContext`s, we have to get creative. This function duplicates frozen mvars in term and tactic info nodes, and add them to diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index c72dbe6..50b0965 100644 --- a/Pantograph/Frontend/InfoTree.lean +++ b/Pantograph/Frontend/InfoTree.lean @@ -103,7 +103,7 @@ partial def InfoTree.findAllInfo | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred | .node i children => let head := if pred i then [(i, context?, children)] else [] - let tail := if haltOnMatch then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred) + let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred) head ++ tail | _ => [] @@ -118,7 +118,7 @@ partial def InfoTree.findAllInfoM [Monad m] | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred | .node i children => let head := if ← pred i context? then [(i, context?, children)] else [] - let tail := if haltOnMatch then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred) + let tail := if haltOnMatch ∧ !head.isEmpty then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred) return head ++ (← tail).join | _ => return [] diff --git a/Test/Frontend.lean b/Test/Frontend.lean index a03b283..3b765fd 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -10,8 +10,6 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do let filename := "" let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} let m := Frontend.mapCompilationSteps λ step => do - for tree in step.trees do - IO.println s!"{← tree.toString}" return (step.before, ← Frontend.collectSorrys step) let li ← m.run context |>.run' state let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do From 2d068ecd5072386fd4043931b96e64fd47760aab Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 00:06:20 -0800 Subject: [PATCH 22/45] fix: Use guarded `isDefEq` --- Pantograph/Frontend/Elab.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index d5af8b5..c4704fc 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -110,7 +110,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) return true ctx.runMetaM lctx do let type ← Meta.inferType expr - Bool.not <$> Meta.isDefEq type expectedType + Bool.not <$> Meta.isExprDefEqGuarded type expectedType | .ofTacticInfo { stx, goalsBefore, .. } => -- The `sorry` term is distinct from the `sorry` tactic let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry From 7fc2bd0d0fc4901b7423782b6092518ac887e38b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 08:15:01 -0800 Subject: [PATCH 23/45] test: Tactic failure on synthesizing placeholder --- Test/Proofs.lean | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 65f099f..1903306 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -701,7 +701,7 @@ def test_nat_zero_add_alt: TestM Unit := do } ]) -def test_composite_tactic_failure: TestM Unit := do +def test_tactic_failure_unresolved_goals : TestM Unit := do let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)") let state0 ← match state? with | .some state => pure state @@ -720,6 +720,25 @@ def test_composite_tactic_failure: TestM Unit := do let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] +def test_tactic_failure_synthesize_placeholder : TestM Unit := do + let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let tactic := "intro p q r h" + let state1 ← match ← state0.tacticOn 0 tactic with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + let tactic := "simpa [h] using And.imp_left h _" + let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" + checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("identity", test_identity), @@ -732,7 +751,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("calc", test_calc), ("Nat.zero_add", test_nat_zero_add), ("Nat.zero_add alt", test_nat_zero_add_alt), - ("composite tactic failure", test_composite_tactic_failure), + ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals), + ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder), ] tests.map (fun (name, test) => (name, proofRunner env test)) From 47d26badc82e606972a1b8a5285b78197411e067 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 17:30:33 -0800 Subject: [PATCH 24/45] feat: Capture mvar errors --- Pantograph/Goal.lean | 6 +++++- Test/Proofs.lean | 4 +++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index e190d5d..4bb1afd 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -208,8 +208,12 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E try let nextState ← state.step goal tacticM + Elab.Term.synthesizeSyntheticMVarsNoPostponing + let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar goal) + let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants + -- Check if error messages have been generated in the core. - let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length + let newMessages ← (← Core.getMessageLog).toList --.drop state.coreState.messages.toList.length |>.filterMapM λ m => do if m.severity == .error then return .some $ ← m.toString diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 1903306..b48e3b0 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -720,6 +720,7 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] + def test_tactic_failure_synthesize_placeholder : TestM Unit := do let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r") let state0 ← match state? with @@ -737,7 +738,8 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do let tactic := "simpa [h] using And.imp_left h _" let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" - checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] + let message := s!":0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n" + checkEq s!"{tactic} fails" messages #[message] def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ From d040d2006c7332eee67b9a0b3d8558e18469386e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 17:58:08 -0800 Subject: [PATCH 25/45] fix: Do not guard mvar errors in other tactics --- Pantograph/Goal.lean | 37 +++++++++++++++++++++++++++---------- Test/Proofs.lean | 16 +++++++++++++--- 2 files changed, 40 insertions(+), 13 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 4bb1afd..51aed88 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -177,16 +177,37 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI --- Tactic execution functions --- -protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) +private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do + let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src) + (← getThe Elab.Term.State).mvarErrorInfos + |>.map (·.mvarId) + |>.filterM λ mvarId => + return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned) + +private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId := + let li2' := li2.filter (¬ li1.contains ·) + li1 ++ li2' + +/-- +Set `guardMVarErrors` to true to capture mvar errors. Lean will not +automatically collect mvars from text tactics (vide +`test_tactic_failure_synthesize_placeholder`) +-/ +protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false) : Elab.TermElabM GoalState := do unless (← getMCtx).decls.contains goal do throwError s!"Goal is not in context: {goal.name}" goal.checkNotAssigned `GoalState.step - let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } + let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } let nextElabState ← MonadBacktrack.saveState + + let goals ← if guardMVarErrors then + pure $ mergeMVarLists goals (← collectAllErroredMVars goal) + else + pure goals return { state with - savedState := { term := nextElabState, tactic := newGoals }, + savedState := { term := nextElabState, tactic := { goals }, }, parentMVar? := .some goal, calcPrevRhs? := .none, } @@ -203,14 +224,10 @@ inductive TacticResult where | invalidAction (message: String) /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/ -protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit): +protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false): Elab.TermElabM TacticResult := do try - let nextState ← state.step goal tacticM - - Elab.Term.synthesizeSyntheticMVarsNoPostponing - let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar goal) - let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants + let nextState ← state.step goal tacticM guardMVarErrors -- Check if error messages have been generated in the core. let newMessages ← (← Core.getMessageLog).toList --.drop state.coreState.messages.toList.length @@ -237,7 +254,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str (fileName := ← getFileName) with | .ok stx => pure $ stx | .error error => return .parseError error - state.tryTacticM goal $ Elab.Tactic.evalTactic tactic + state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do diff --git a/Test/Proofs.lean b/Test/Proofs.lean index b48e3b0..a6b5487 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -737,9 +737,19 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do return () let tactic := "simpa [h] using And.imp_left h _" - let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" - let message := s!":0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n" - checkEq s!"{tactic} fails" messages #[message] + let state2 ← match ← state1.tacticOn 0 tactic with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + checkEq tactic ((← state2.serializeGoals).map (·.devolatilize)) #[ + buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r" + ] + + --let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" + --let message := s!":0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n" + --checkEq s!"{tactic} fails" messages #[message] def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ From 5ef2b5c11840890471db123ecce3f26642e38478 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 19:40:00 -0800 Subject: [PATCH 26/45] feat: Collect newly defined constants --- Pantograph/Frontend/Elab.lean | 15 ++++++++++++++- Test/Frontend.lean | 27 +++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 1 deletion(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index c4704fc..4ace608 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -2,6 +2,7 @@ import Lean.Elab.Import import Lean.Elab.Command import Lean.Elab.InfoTree +import Lean.DeclarationRange import Pantograph.Frontend.Basic import Pantograph.Frontend.MetaTranslate @@ -128,7 +129,7 @@ Since we cannot directly merge `MetavarContext`s, we have to get creative. This function duplicates frozen mvars in term and tactic info nodes, and add them to the current `MetavarContext`. -/ -@[export pantograph_frontend_sorrys_to_goal_state] +@[export pantograph_frontend_sorrys_to_goal_state_m] def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do assert! !sorrys.isEmpty let goalsM := sorrys.mapM λ i => do @@ -147,5 +148,17 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do GoalState.createFromMVars goals root +@[export pantograph_frontend_collect_new_defined_constants_m] +def collectNewDefinedConstants (step : CompilationStep) : IO (List Name) := do + step.after.constants.map₂.foldlM (λ acc name _ => do + if step.before.contains name then + return acc + let coreM : CoreM Bool := Option.isSome <$> findDeclarationRanges? name + let hasRange ← coreM.run' { fileName := step.fileName, fileMap := step.fileMap } { env := step.after } |>.toBaseIO + match hasRange with + | .ok true => return name :: acc + | .ok false => return acc + | .error e => throw $ IO.userError (← e.toMessageData.toString) + ) [] end Pantograph.Frontend diff --git a/Test/Frontend.lean b/Test/Frontend.lean index 3b765fd..68aaf94 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -184,6 +184,31 @@ def mystery : Nat := true let goalStates ← (collectSorrysFromSource input).run' {} let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" +def collectNewConstants (source: String) : MetaM (List (List Name)) := do + let filename := "" + let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {} + let m := Frontend.mapCompilationSteps λ step => do + Frontend.collectNewDefinedConstants step + m.run context |>.run' state + +def test_collect_one_constant : TestT MetaM Unit := do + let input := " +def mystery : Nat := 123 + " + let names ← collectNewConstants input + checkEq "constants" names [[`mystery]] +def test_collect_one_theorem : TestT MetaM Unit := do + let input := " +theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by + match as, i with + | a::as, ⟨0, _⟩ => simp_arith [get] + | a::as, ⟨i+1, h⟩ => + have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩ + apply Nat.lt_trans ih + simp_arith + " + let names ← collectNewConstants input + checkEq "constants" names [[`mystery]] def suite (env : Environment): List (String × IO LSpec.TestSeq) := let tests := [ @@ -193,6 +218,8 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) := ("sorry_in_coupled", test_sorry_in_coupled), ("environment_capture", test_environment_capture), ("capture_type_mismatch", test_capture_type_mismatch), + ("collect_one_constant", test_collect_one_constant), + ("collect_one_theorem", test_collect_one_theorem), ] tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test)) From 0b4ded10493585aeba2e9b345ddc9ed81d4a02ad Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 20:15:53 -0800 Subject: [PATCH 27/45] fix: Collect sorrys and type mismatches --- Pantograph/Frontend/Elab.lean | 21 +++++++++++++-------- Pantograph/Frontend/InfoTree.lean | 12 ++++++------ Test/Frontend.lean | 11 ++++++++++- 3 files changed, 29 insertions(+), 15 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 4ace608..2eff084 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -103,20 +103,25 @@ structure InfoWithContext where context?: Option Elab.ContextInfo := .none private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do - let infos ← t.findAllInfoM none true fun i ctx? => match i with + let infos ← t.findAllInfoM none fun i ctx? => match i with | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do - let .some expectedType := expectedType? | return false - let .some ctx := ctx? | return false + let .some expectedType := expectedType? | return (false, true) + let .some ctx := ctx? | return (false, true) if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then - return true - ctx.runMetaM lctx do + return (true, false) + let typeMatch ← ctx.runMetaM lctx do let type ← Meta.inferType expr - Bool.not <$> Meta.isExprDefEqGuarded type expectedType + Meta.isExprDefEqGuarded type expectedType + return match typeMatch, expr.hasSorry with + | false, true => (true, false) -- Types mismatch but has sorry -> collect, halt + | false, false => (true, false) -- Types mistmatch but no sorry -> collect, halt + | true, true => (false, true) -- Types match but has sorry -> continue + | true, false => (false, false) -- Types match but no sorries -> halt | .ofTacticInfo { stx, goalsBefore, .. } => -- The `sorry` term is distinct from the `sorry` tactic let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry - return isSorry ∧ !goalsBefore.isEmpty - | _ => return false + return (isSorry ∧ !goalsBefore.isEmpty, ¬ isSorry) + | _ => return (false, true) return infos.map fun (info, context?, _) => { info, context? } -- NOTE: Plural deliberately not spelled "sorries" diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index 50b0965..cfef621 100644 --- a/Pantograph/Frontend/InfoTree.lean +++ b/Pantograph/Frontend/InfoTree.lean @@ -107,18 +107,18 @@ partial def InfoTree.findAllInfo head ++ tail | _ => [] -/-- Monadic analogue of `findAllInfo` -/ +/-- Monadic analogue of `findAllInfo`, but predicate controls whether to recurse. -/ partial def InfoTree.findAllInfoM [Monad m] (t : InfoTree) (context?: Option Elab.ContextInfo) - (haltOnMatch : Bool) - (pred : Elab.Info → Option Elab.ContextInfo → m Bool) + (pred : Elab.Info → Option Elab.ContextInfo → m (Bool × Bool)) : m (List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree)) := do match t with - | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred + | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) pred | .node i children => - let head := if ← pred i context? then [(i, context?, children)] else [] - let tail := if haltOnMatch ∧ !head.isEmpty then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred) + let (flagCollect, flagRecurse) ← pred i context? + let head := if flagCollect then [(i, context?, children)] else [] + let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred) return head ++ (← tail).join | _ => return [] diff --git a/Test/Frontend.lean b/Test/Frontend.lean index 68aaf94..2259029 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -179,10 +179,19 @@ example (n: Nat) : mystery n + 1 = n + 2 := sorry def test_capture_type_mismatch : TestT MetaM Unit := do let input := " -def mystery : Nat := true +def mystery (k: Nat) : Nat := true " let goalStates ← (collectSorrysFromSource input).run' {} let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}" + checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[ + { + target := { pp? := "Nat" }, + vars := #[{ + userName := "k", + type? := .some { pp? := "Nat" }, + }], + } + ] def collectNewConstants (source: String) : MetaM (List (List Name)) := do let filename := "" From e9cbc6eab37a81e527b8d9b220a47ec1cf8debee Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 20:17:55 -0800 Subject: [PATCH 28/45] chore: Update version --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 2decbc1..81dceee 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.2.19" +def version := "0.2.22" end Pantograph From dd00d803d1fe500f46710bb32bfcc9eeeb2d8062 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 20:38:27 -0800 Subject: [PATCH 29/45] feat: Collect sorry/elab failure boundaries --- Pantograph/Frontend/Basic.lean | 7 +++++++ Pantograph/Frontend/Elab.lean | 19 ++++++++++++++----- Pantograph/Protocol.lean | 2 ++ Repl.lean | 13 +++++++------ Test/Frontend.lean | 4 ++-- 5 files changed, 32 insertions(+), 13 deletions(-) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 1074a94..87decd4 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -30,6 +30,13 @@ end Lean.PersistentArray namespace Pantograph.Frontend +@[export pantograph_frontend_stx_byte_range] +def stxByteRange (stx : Syntax) : String.Pos × String.Pos := + let pos := stx.getPos?.getD 0 + let endPos := stx.getTailPos?.getD 0 + (pos, endPos) + + abbrev FrontendM := Elab.Frontend.FrontendM structure CompilationStep where diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 2eff084..a33fbef 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -129,28 +129,37 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do return (← step.trees.mapM collectSorrysInTree).join +structure AnnotatedGoalState where + state : GoalState + srcBoundaries : List (String.Pos × String.Pos) + /-- Since we cannot directly merge `MetavarContext`s, we have to get creative. This function duplicates frozen mvars in term and tactic info nodes, and add them to the current `MetavarContext`. -/ @[export pantograph_frontend_sorrys_to_goal_state_m] -def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do +def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do assert! !sorrys.isEmpty let goalsM := sorrys.mapM λ i => do match i.info with | .ofTermInfo termInfo => do let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context? - return [mvarId] + return [(mvarId, stxByteRange termInfo.stx)] | .ofTacticInfo tacticInfo => do - MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context? + let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context? + let range := stxByteRange tacticInfo.stx + return mvarIds.map (·, range) | _ => panic! "Invalid info" - let goals := List.join (← goalsM.run {} |>.run' {}) + let annotatedGoals := List.join (← goalsM.run {} |>.run' {}) + let goals := annotatedGoals.map Prod.fst + let srcBoundaries := annotatedGoals.map Prod.snd let root := match goals with | [] => panic! "No MVars generated" | [g] => g | _ => { name := .anonymous } - GoalState.createFromMVars goals root + let state ← GoalState.createFromMVars goals root + return { state, srcBoundaries } @[export pantograph_frontend_collect_new_defined_constants_m] diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 0cb6cac..5cb24e8 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -329,6 +329,8 @@ structure CompilationUnit where invocations?: Option (List InvokedTactic) := .none goalStateId?: Option Nat := .none goals: Array Goal := #[] + -- Code segments which generated the goals + goalSrcBoundaries: Array (Nat × Nat) := #[] messages: Array String := #[] deriving Lean.ToJson structure FrontendProcessResult where diff --git a/Repl.lean b/Repl.lean index f1c8f42..201a841 100644 --- a/Repl.lean +++ b/Repl.lean @@ -265,18 +265,19 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return (step.before, boundary, invocations?, sorrys, messages) let li ← frontendM.run context |>.run' state let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do - let (goalStateId?, goals) ← if sorrys.isEmpty then do - pure (.none, #[]) + let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do + pure (.none, #[], #[]) else do - let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys - let stateId ← newGoalState goalState - let goals ← goalSerialize goalState options - pure (.some stateId, goals) + let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys + let stateId ← newGoalState state + let goals ← goalSerialize state options + pure (.some stateId, goals, srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))) return { boundary, invocations?, goalStateId?, goals, + goalSrcBoundaries, messages, } return .ok { units } diff --git a/Test/Frontend.lean b/Test/Frontend.lean index 2259029..a3b73ae 100644 --- a/Test/Frontend.lean +++ b/Test/Frontend.lean @@ -15,8 +15,8 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do if sorrys.isEmpty then return .none - let goalState ← Frontend.sorrysToGoalState sorrys - return .some goalState + let { state, .. } ← Frontend.sorrysToGoalState sorrys + return .some state return goalStates def test_multiple_sorrys_in_proof : TestT MetaM Unit := do From 9a69c48cb23f313e5986e87a8867eaf3d9b6528e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 20:42:05 -0800 Subject: [PATCH 30/45] fix: Integration test failure --- Test/Integration.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Test/Integration.lean b/Test/Integration.lean index 9fb86b7..171bc91 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -222,6 +222,7 @@ def test_frontend_process_sorry : Test := boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize), goalStateId? := .some 0, goals := #[goal1], + goalSrcBoundaries := #[(57, 62)], messages := #[":2:0: warning: declaration uses 'sorry'\n"], }], }: Protocol.FrontendProcessResult), From eb0374dfb3cd73df86bfcfe5a0ed1f5d03d37cce Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 20:57:25 -0800 Subject: [PATCH 31/45] feat: Collect new constants in repl --- Pantograph/Protocol.lean | 3 +++ Repl.lean | 13 +++++++++++-- Test/Integration.lean | 2 ++ 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 5cb24e8..d80c761 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -312,6 +312,8 @@ structure FrontendProcess where invocations: Bool := false -- If set to true, collect `sorry`s sorrys: Bool := false + -- If set to true, extract new constants + newConstants: Bool := false deriving Lean.FromJson structure InvokedTactic where goalBefore: String @@ -332,6 +334,7 @@ structure CompilationUnit where -- Code segments which generated the goals goalSrcBoundaries: Array (Nat × Nat) := #[] messages: Array String := #[] + newConstants: Option (Array String) := .none deriving Lean.ToJson structure FrontendProcessResult where units: List CompilationUnit diff --git a/Repl.lean b/Repl.lean index 201a841..710b132 100644 --- a/Repl.lean +++ b/Repl.lean @@ -262,9 +262,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do else pure [] let messages ← step.messageStrings - return (step.before, boundary, invocations?, sorrys, messages) + let newConstants ← if args.newConstants then + Frontend.collectNewDefinedConstants step + else + pure [] + return (step.before, boundary, invocations?, sorrys, messages, newConstants) let li ← frontendM.run context |>.run' state - let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do + let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do + let newConstants := if args.newConstants then + .some $ newConstants.toArray.map λ name => name.toString + else + .none let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do pure (.none, #[], #[]) else do @@ -279,6 +287,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goals, goalSrcBoundaries, messages, + newConstants, } return .ok { units } catch e => diff --git a/Test/Integration.lean b/Test/Integration.lean index 171bc91..8d53168 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -174,6 +174,7 @@ def test_frontend_process : Test := ("file", .str file), ("invocations", .bool true), ("sorrys", .bool false), + ("newConstants", .bool false), ] ({ units := [{ @@ -214,6 +215,7 @@ def test_frontend_process_sorry : Test := ("file", .str file), ("invocations", .bool false), ("sorrys", .bool true), + ("newConstants", .bool false), ] ({ units := [{ From 1527743900b2af65514be9cf6a3d9f18b818874a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 21:00:33 -0800 Subject: [PATCH 32/45] refactor: Optionalize CompilationUnit --- Pantograph/Protocol.lean | 10 ++++++---- Repl.lean | 17 +++++++++-------- Test/Integration.lean | 4 ++-- 3 files changed, 17 insertions(+), 14 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index d80c761..f232d9e 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -327,14 +327,16 @@ structure InvokedTactic where structure CompilationUnit where -- String boundaries of compilation units boundary: (Nat × Nat) + messages: Array String := #[] -- Tactic invocations invocations?: Option (List InvokedTactic) := .none goalStateId?: Option Nat := .none - goals: Array Goal := #[] + goals?: Option (Array Goal) := .none -- Code segments which generated the goals - goalSrcBoundaries: Array (Nat × Nat) := #[] - messages: Array String := #[] - newConstants: Option (Array String) := .none + goalSrcBoundaries?: Option (Array (Nat × Nat)) := .none + + -- New constants defined in compilation unit + newConstants?: Option (Array String) := .none deriving Lean.ToJson structure FrontendProcessResult where units: List CompilationUnit diff --git a/Repl.lean b/Repl.lean index 710b132..283bcf3 100644 --- a/Repl.lean +++ b/Repl.lean @@ -269,25 +269,26 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return (step.before, boundary, invocations?, sorrys, messages, newConstants) let li ← frontendM.run context |>.run' state let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do - let newConstants := if args.newConstants then + let newConstants? := if args.newConstants then .some $ newConstants.toArray.map λ name => name.toString else .none - let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do - pure (.none, #[], #[]) + let (goalStateId?, goals?, goalSrcBoundaries?) ← if sorrys.isEmpty then do + pure (.none, .none, .none) else do let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys let stateId ← newGoalState state let goals ← goalSerialize state options - pure (.some stateId, goals, srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))) + let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx)) + pure (.some stateId, .some goals, .some srcBoundaries) return { boundary, + messages, invocations?, goalStateId?, - goals, - goalSrcBoundaries, - messages, - newConstants, + goals?, + goalSrcBoundaries?, + newConstants?, } return .ok { units } catch e => diff --git a/Test/Integration.lean b/Test/Integration.lean index 8d53168..3e9bed2 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -223,8 +223,8 @@ def test_frontend_process_sorry : Test := }, { boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize), goalStateId? := .some 0, - goals := #[goal1], - goalSrcBoundaries := #[(57, 62)], + goals? := .some #[goal1], + goalSrcBoundaries? := .some #[(57, 62)], messages := #[":2:0: warning: declaration uses 'sorry'\n"], }], }: Protocol.FrontendProcessResult), From 37a5884be40790a946e0b8e26879ed3bbf509077 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 21:39:33 -0800 Subject: [PATCH 33/45] fix: Use `ppSyntax` instead of `ppTactic` --- Pantograph/Frontend/Elab.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index a33fbef..d9480f0 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -87,9 +87,11 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc tactics.mapM λ invocation => do let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty - let tactic ← invocation.ctx.runMetaM {} do - let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ - return t.pretty + let tactic ← invocation.ctx.runMetaM {} <| Meta.withMCtx invocation.info.mctxBefore do + return (← invocation.ctx.ppSyntax {} invocation.info.stx).pretty + -- FIXME: Why does this not work? There are problems with `term.pseudo.antiquot` + --PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ + --return t.pretty let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString return { goalBefore, From 681c3fb78d2055e4d8dbe1fcd2ef5c66d28b6469 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 12:21:56 -0800 Subject: [PATCH 34/45] fix: Disallow indeterminant type `sorry` --- Pantograph/Frontend/Elab.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index d9480f0..3da5fca 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -1,4 +1,3 @@ -/- Adapted from https://github.com/semorrison/lean-training-data -/ import Lean.Elab.Import import Lean.Elab.Command import Lean.Elab.InfoTree @@ -16,6 +15,7 @@ namespace Pantograph.Frontend -- Info tree filtering functions +/- Adapted from lean-training-data -/ structure TacticInvocation where info : Elab.TacticInfo ctx : Elab.ContextInfo @@ -107,10 +107,12 @@ structure InfoWithContext where private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do let infos ← t.findAllInfoM none fun i ctx? => match i with | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do - let .some expectedType := expectedType? | return (false, true) let .some ctx := ctx? | return (false, true) if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then + if expectedType?.isNone then + throw $ .userError "Sorry of indeterminant type is not allowed" return (true, false) + let .some expectedType := expectedType? | return (false, true) let typeMatch ← ctx.runMetaM lctx do let type ← Meta.inferType expr Meta.isExprDefEqGuarded type expectedType From 95503c45e4ac6217889cd21d63672d58768835f1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 21:45:57 -0800 Subject: [PATCH 35/45] doc: frontend.process newConstants --- doc/repl.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/doc/repl.md b/doc/repl.md index 464c7cc..d332986 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -44,9 +44,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va state. The user is responsible to ensure the sender/receiver instances share the same environment. * `frontend.process { ["fileName": ,] ["file": ], invocations: - , sorrys: }`: Executes the Lean frontend on a file, collecting - either the tactic invocations (`"invocations": true`) or the sorrys into goal - states (`"sorrys": true`) + , sorrys: , newConstants: }`: Executes the Lean frontend on + a file, collecting the tactic invocations (`"invocations": true`), the + sorrys and type errors into goal states (`"sorrys": true`), and new constants + (`"newConstants": true`). In the case of `sorrys`, this command additionally + outputs the position of each captured `sorry`. ## Errors From 1d10cd2b205f8baf172384733793cd2a55a1f5d8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 23:16:33 -0800 Subject: [PATCH 36/45] fix: Collect errored mvars by iterating errorInfo --- Pantograph/Goal.lean | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 51aed88..f2eb25a 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -177,12 +177,25 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI --- Tactic execution functions --- +-- Mimics `Elab.Term.logUnassignedUsingErrorInfos` private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src) - (← getThe Elab.Term.State).mvarErrorInfos - |>.map (·.mvarId) - |>.filterM λ mvarId => - return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned) + let mut alreadyVisited : MVarIdSet := {} + let mut result : MVarIdSet := {} + for mvarErrorInfo in (← get).mvarErrorInfos do + let mvarId := mvarErrorInfo.mvarId + unless alreadyVisited.contains mvarId do + alreadyVisited := alreadyVisited.insert mvarId + /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or + delayed assigned to another metavariable that is unassigned. -/ + let mvarDeps ← Meta.getMVars (mkMVar mvarId) + if mvarDeps.any descendants.contains then do + result := result.insert mvarId + return result.toList + --(← getThe Elab.Term.State).mvarErrorInfos + -- |>.map (·.mvarId) + -- |>.filterM λ mvarId => + -- return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned) private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId := let li2' := li2.filter (¬ li1.contains ·) From 755ba13c1b8f92d91dea492d4b8106a90f68e295 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 23:48:46 -0800 Subject: [PATCH 37/45] fix: Set `synthesizeSyntheticMVarsNoPostponing` --- Pantograph/Goal.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index f2eb25a..3a6e97a 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -179,6 +179,10 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI -- Mimics `Elab.Term.logUnassignedUsingErrorInfos` private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do + -- These descendants serve as "seed" mvars. If a MVarError's mvar is related + -- to one of these seed mvars, it means an error has occurred when a tactic + -- was executing on `src`. `evalTactic`, will not capture these mvars, so we + -- need to manually find them and save them into the goal list. let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src) let mut alreadyVisited : MVarIdSet := {} let mut result : MVarIdSet := {} @@ -213,6 +217,7 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta goal.checkNotAssigned `GoalState.step let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } let nextElabState ← MonadBacktrack.saveState + Elab.Term.synthesizeSyntheticMVarsNoPostponing let goals ← if guardMVarErrors then pure $ mergeMVarLists goals (← collectAllErroredMVars goal) From e0e5c9ec681d0423a12a0c0278fef38cd8c5af80 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 23:51:47 -0800 Subject: [PATCH 38/45] chore: Code cleanup --- Pantograph/Goal.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 3a6e97a..7a09435 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -186,8 +186,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src) let mut alreadyVisited : MVarIdSet := {} let mut result : MVarIdSet := {} - for mvarErrorInfo in (← get).mvarErrorInfos do - let mvarId := mvarErrorInfo.mvarId + for { mvarId, .. } in (← get).mvarErrorInfos do unless alreadyVisited.contains mvarId do alreadyVisited := alreadyVisited.insert mvarId /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or @@ -196,10 +195,6 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) if mvarDeps.any descendants.contains then do result := result.insert mvarId return result.toList - --(← getThe Elab.Term.State).mvarErrorInfos - -- |>.map (·.mvarId) - -- |>.filterM λ mvarId => - -- return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned) private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId := let li2' := li2.filter (¬ li1.contains ·) From cb87fcd9dd89fdeaaaad49f0dd0111b4e7416c49 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:16:52 -0800 Subject: [PATCH 39/45] fix: Insert `mvarDeps` --- Pantograph/Goal.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7a09435..52562e7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -184,6 +184,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) -- was executing on `src`. `evalTactic`, will not capture these mvars, so we -- need to manually find them and save them into the goal list. let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src) + --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants let mut alreadyVisited : MVarIdSet := {} let mut result : MVarIdSet := {} for { mvarId, .. } in (← get).mvarErrorInfos do @@ -191,9 +192,9 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) alreadyVisited := alreadyVisited.insert mvarId /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or delayed assigned to another metavariable that is unassigned. -/ - let mvarDeps ← Meta.getMVars (mkMVar mvarId) + let mvarDeps ← Meta.getMVars (.mvar mvarId) if mvarDeps.any descendants.contains then do - result := result.insert mvarId + result := mvarDeps.foldl (·.insert ·) result return result.toList private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId := From 58956d33fe25069c708213ccb625ac88c8f04a47 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:21:26 -0800 Subject: [PATCH 40/45] doc: Update behaviour rationale --- doc/rationale.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/doc/rationale.md b/doc/rationale.md index 87c1606..4209474 100644 --- a/doc/rationale.md +++ b/doc/rationale.md @@ -24,6 +24,22 @@ The name Pantograph is a pun. It means two things a locomotive. In comparison the (relatively) simple Pantograph software powers theorem proving projects. +## Caveats + +Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the +flexibility it offers. To support tree search means Pantograph has to act +differently from Lean in some times, but never at the sacrifice of soundness. + +- When Lean LSP says "don't know how to synthesize placeholder", this indicates + the human operator needs to manually move the cursor to the placeholder and + type in the correct expression. This error therefore should not halt the proof + process, and the placeholder should be turned into a goal. +- When Lean LSP says "unresolved goals", that means a proof cannot finish where + it is supposed to finish at the end of a `by` block. Pantograph will raise the + error in this case, since it indicates the termination of a proof search branch. +- `pick_goal` or `swap` will not work since they run contrary to tree search + paradigms. + ## References * [Pantograph Paper](https://arxiv.org/abs/2410.16429) From aa122b2bb904e6cd757c1b5e0b75113510c1efaa Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:24:56 -0800 Subject: [PATCH 41/45] doc: Update rationale link --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index e070fff..02de68c 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ A Machine-to-Machine interaction system for Lean 4. Pantograph provides interfaces to execute proofs, construct expressions, and examine the symbol list of a Lean project for machine learning. -See [documentations](doc/) for design rationale and references. +See [documentations](doc/rationale.md) for design rationale and references. ## Installation From c96df2ed1cd834f3a04374f60c852ed8a2253e8f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:29:29 -0800 Subject: [PATCH 42/45] chore: Add `aarch64` build targets to flake --- flake.nix | 2 ++ 1 file changed, 2 insertions(+) diff --git a/flake.nix b/flake.nix index 91901d8..f49a331 100644 --- a/flake.nix +++ b/flake.nix @@ -22,6 +22,8 @@ flake = { }; systems = [ + "aarch64-linux" + "aarch64-darwin" "x86_64-linux" "x86_64-darwin" ]; From f2f71a60281f66d78687128b8fb879e0f7a11fe0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 09:01:57 -0800 Subject: [PATCH 43/45] fix: Reset core message log --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 52562e7..b140ee7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -250,6 +250,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E return .some $ ← m.toString else return .none + Core.resetMessageLog if ¬ newMessages.isEmpty then return .failure newMessages.toArray return .success nextState From ab77418e242d81e502f4ae7a88ab7decf8d6b1a6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 09:05:47 -0800 Subject: [PATCH 44/45] fix: Drop previous message lists --- Pantograph/Goal.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b140ee7..6ff14d2 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -244,7 +244,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E let nextState ← state.step goal tacticM guardMVarErrors -- Check if error messages have been generated in the core. - let newMessages ← (← Core.getMessageLog).toList --.drop state.coreState.messages.toList.length + let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length |>.filterMapM λ m => do if m.severity == .error then return .some $ ← m.toString From 396a787771909d722e531acf2c11ffec2dd11900 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 09:06:42 -0800 Subject: [PATCH 45/45] feat: Reset message log in MainM --- Repl.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Repl.lean b/Repl.lean index 283bcf3..2060061 100644 --- a/Repl.lean +++ b/Repl.lean @@ -79,6 +79,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let nGoals := state.goalStates.size set { state with nextId := 0, goalStates := .empty } + Lean.Core.resetMessageLog return .ok { nGoals } stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do let state ← get