aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

fix: Tactic failure on synthesizing placeholder #139

Merged
aniva merged 10 commits from bug/tactic-failure-placeholder into dev 2024-12-11 01:13:15 -08:00
Conversation 4 Commits 10 Files Changed 4 +5
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 755ba13c1b - Show all commits

5
Pantograph/Goal.lean
View File

@ -179,6 +179,10 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
-- Mimics `Elab.Term.logUnassignedUsingErrorInfos` -- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do 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 descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src)
let mut alreadyVisited : MVarIdSet := {} let mut alreadyVisited : MVarIdSet := {}
let mut result : MVarIdSet := {} let mut result : MVarIdSet := {}
@ -213,6 +217,7 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
goal.checkNotAssigned `GoalState.step goal.checkNotAssigned `GoalState.step
let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
let nextElabState ← MonadBacktrack.saveState let nextElabState ← MonadBacktrack.saveState
Elab.Term.synthesizeSyntheticMVarsNoPostponing
let goals ← if guardMVarErrors then let goals ← if guardMVarErrors then
pure $ mergeMVarLists goals (← collectAllErroredMVars goal) pure $ mergeMVarLists goals (← collectAllErroredMVars goal)