From d040d2006c7332eee67b9a0b3d8558e18469386e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 17:58:08 -0800
Subject: [PATCH] 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!"<Pantograph>: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!"<Pantograph>: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 := [