fix: tactics in terms in tactics may break incremental reporting (#4436)

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](5f9dedfe5e/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

@@ -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

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

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}}}]}