From 7fc2bd0d0fc4901b7423782b6092518ac887e38b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 08:15:01 -0800 Subject: [PATCH 1/9] 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)) -- 2.44.1 From 47d26badc82e606972a1b8a5285b78197411e067 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 17:30:33 -0800 Subject: [PATCH 2/9] 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 := [ -- 2.44.1 From d040d2006c7332eee67b9a0b3d8558e18469386e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 17:58:08 -0800 Subject: [PATCH 3/9] 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 := [ -- 2.44.1 From 1d10cd2b205f8baf172384733793cd2a55a1f5d8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 23:16:33 -0800 Subject: [PATCH 4/9] 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 ·) -- 2.44.1 From 755ba13c1b8f92d91dea492d4b8106a90f68e295 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 23:48:46 -0800 Subject: [PATCH 5/9] 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) -- 2.44.1 From e0e5c9ec681d0423a12a0c0278fef38cd8c5af80 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 10 Dec 2024 23:51:47 -0800 Subject: [PATCH 6/9] 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 ·) -- 2.44.1 From cb87fcd9dd89fdeaaaad49f0dd0111b4e7416c49 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:16:52 -0800 Subject: [PATCH 7/9] 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 := -- 2.44.1 From 58956d33fe25069c708213ccb625ac88c8f04a47 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:21:26 -0800 Subject: [PATCH 8/9] 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) -- 2.44.1 From aa122b2bb904e6cd757c1b5e0b75113510c1efaa Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 00:24:56 -0800 Subject: [PATCH 9/9] 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 -- 2.44.1