From c032af2f515c00426cb37066f89c0dba3d3605f3 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 24 Feb 2026 17:59:50 -0800
Subject: [PATCH] fix: make `tactic .. at *` save info contexts (#12607)

This PR fixes an issue where `withLocation` wasn't saving the info
context, which meant that tactics that use `at *` location syntax and do
term elaboration would save infotrees but revert the metacontext,
leading to Infoview messages like "Error updating: Error fetching goals:
Rpc error: InternalError: unknown metavariable" if the tactic failed at
some locations but succeeded at others.

Closes #10898
---
 src/Lean/Elab/Tactic/Location.lean             | 4 ++--
 tests/lean/interactive/10898.lean              | 9 +++++++++
 tests/lean/interactive/10898.lean.expected.out | 9 +++++++++
 3 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/interactive/10898.lean
 create mode 100644 tests/lean/interactive/10898.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index d6ce56fb8d..695a471d8b 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/src/Lean/Elab/Tactic/Location.lean
@@ -64,7 +64,7 @@ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget
     if type then
       withMainContext atTarget
   | Location.wildcard =>
-    let worked ← tryTactic <| withMainContext <| atTarget
+    let worked ← tryTactic <| withSaveInfoContext <| withMainContext <| atTarget
     let g ← try getMainGoal catch _ => return () -- atTarget closed the goal
     g.withContext do
       let mut worked := worked
@@ -72,7 +72,7 @@ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget
       for fvarId in (← getLCtx).getFVarIds.reverse do
         if (← fvarId.getDecl).isImplementationDetail then
           continue
-        worked := worked || (← tryTactic <| withMainContext <| atLocal fvarId)
+        worked := worked || (← tryTactic <| withSaveInfoContext <| withMainContext <| atLocal fvarId)
       unless worked do
         failed (← getMainGoal)
 
diff --git a/tests/lean/interactive/10898.lean b/tests/lean/interactive/10898.lean
new file mode 100644
index 0000000000..47cbe1f79e
--- /dev/null
+++ b/tests/lean/interactive/10898.lean
@@ -0,0 +1,9 @@
+/-!
+# `rw .. at *` should save metacontext
+-/
+
+example (h : 1 + 2 = 3) : True := by
+  rewrite [Nat.add_comm _] at *
+                      --^ $/lean/plainGoal
+                      --^ $/lean/plainTermGoal
+  trivial
diff --git a/tests/lean/interactive/10898.lean.expected.out b/tests/lean/interactive/10898.lean.expected.out
new file mode 100644
index 0000000000..c17c9bd661
--- /dev/null
+++ b/tests/lean/interactive/10898.lean.expected.out
@@ -0,0 +1,9 @@
+{"textDocument": {"uri": "file:///10898.lean"},
+ "position": {"line": 5, "character": 24}}
+{"rendered": "```lean\nh : 2 + 1 = 3\n⊢ True\n```",
+ "goals": ["h : 2 + 1 = 3\n⊢ True"]}
+{"textDocument": {"uri": "file:///10898.lean"},
+ "position": {"line": 5, "character": 24}}
+{"range":
+ {"start": {"line": 5, "character": 24}, "end": {"line": 5, "character": 25}},
+ "goal": "h : 1 + 2 = 3\n⊢ Nat"}