From 8d3be9602470449daa1fd4e580207bf33eeac880 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 12 Jun 2024 16:59:24 +0200
Subject: [PATCH] fix: tactics in terms in tactics may break incremental
 reporting (#4436)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A pending tactic mvar managed to escape into an unexpected context in
specific circumstances.

```lean
example : True := by
  · rw [show 0 = 0 by rfl]
```
* Term elaboration of the `show` creates a pending mvar for the `by rfl`
proof
* `rw` fails with an exception because the pattern does not occur in the
target
* `cdot` catches the exception and admits the goal
* `Term.runTactic` [synthesizes all pending mvars from the tactic's
execution](https://github.com/leanprover/lean4/blob/5f9dedfe5ee9972acdebd669f228f487844a6156/src/Lean/Elab/SyntheticMVars.lean#L350),
including the `by rfl` proof. But this would not have happened without
`cdot` as the exception would have skipped that invocation!
* Now incrementality is confused because the nested `by rfl` proof is
unexpectedly run in the same context as the top-level proof, writing to
the wrong promise, and the error message is lost

Solution: disable incrementality for these pending mvars
---
 src/Lean/Elab/SyntheticMVars.lean                    |  5 ++++-
 tests/lean/interactive/incrementalTactic.lean        |  9 +++++++++
 .../interactive/incrementalTactic.lean.expected.out  | 12 ++++++++++++
 3 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 322bfcb859..52b497d09e 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -347,7 +347,10 @@ mutual
               -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
               withTacticInfoContext tacticCode[0] do
                 withNarrowedArgTacticReuse (argIdx := 1) (evalTactic ·) tacticCode
-            synthesizeSyntheticMVars (postpone := .no)
+            -- Pending tactic mvars may escape from `evalTactic` to here (#4436), so make sure
+            -- incrementality is disabled so they cannot be confused for top-level tactic blocks
+            withoutTacticIncrementality true do
+              synthesizeSyntheticMVars (postpone := .no)
           unless remainingGoals.isEmpty do
             if report then
               reportUnsolvedGoals remainingGoals
diff --git a/tests/lean/interactive/incrementalTactic.lean b/tests/lean/interactive/incrementalTactic.lean
index 25aa68e46e..a1783204ff 100644
--- a/tests/lean/interactive/incrementalTactic.lean
+++ b/tests/lean/interactive/incrementalTactic.lean
@@ -71,3 +71,12 @@ def dup_goals : True := by
 --^ goals
 -- (note that request positions are computed relative to the original document, so the checks above
 -- will point at a `show` at run time)
+
+/-!
+A tactic mvar may sometimes escape the term elaboration it was created from and should not break
+incremental reporting in this case.
+-/
+-- RESET
+def tacInTermInTac : True := by
+  · rw [show 0 = 0 by rfl]
+--^ collectDiagnostics
diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out
index 9417b2fa17..1b64ca06ef 100644
--- a/tests/lean/interactive/incrementalTactic.lean.expected.out
+++ b/tests/lean/interactive/incrementalTactic.lean.expected.out
@@ -62,3 +62,15 @@ s
                isRemoved? := none,
                hyps := #[] }] }
 
+{"version": 1,
+ "uri": "file:///incrementalTactic.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 2, "character": 8}, "end": {"line": 2, "character": 25}},
+   "message":
+   "tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n  0\n⊢ True",
+   "fullRange":
+   {"start": {"line": 2, "character": 8},
+    "end": {"line": 2, "character": 25}}}]}