fix: calculate error suppression per snapshot (leanprover#4657)

Generalizes leanprover#3556 to not suppressing errors in tactic steps either when
the parse error is in a later step, as otherwise changes to the end of a
proof would affect (correctness or effectiveness of) incrementality of
preceding steps.

Fixes leanprover#4623, in combination with leanprover#4643

src/Lean/Elab/MutualDef.lean

@@ -168,13 +168,8 @@ private def elabHeaders (views : Array DefView)
           reuseBody := false
 
       let mut (newHeader, newState) ← withRestoreOrSaveFull reusableResult? none do
-        withRef view.headerRef do
-        addDeclarationRanges declName view.ref  -- NOTE: this should be the full `ref`
+        withReuseContext view.headerRef do
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
-        -- do not hide header errors on partial body syntax as these two elaboration parts are
-        -- sufficiently independent
-        withTheReader Core.Context ({ · with suppressElabErrors :=
-          view.headerRef.hasMissing && !Command.showPartialSyntaxErrors.get (← getOptions) }) do
         withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
             let refForElabFunType := view.value
@@ -340,6 +335,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
           reusableResult? := some (old.value, old.state)
 
     let (val, state) ← withRestoreOrSaveFull reusableResult? header.tacSnap? do
+      withReuseContext header.value do
       withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← liftMacroM <| declValToTerm header.value
       forallBoundedTelescope header.type header.numParams fun xs type => do
@@ -933,6 +929,11 @@ where
           checkForHiddenUnivLevels allUserLevelNames preDefs
           addPreDefinitions preDefs
           processDeriving headers
+      for view in views, header in headers do
+        -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
+        -- that depends only on a part of the ref
+        addDeclarationRanges header.declName view.ref
+
 
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -93,7 +93,8 @@ where
             let (_, state) ← withRestoreOrSaveFull reusableResult?
                 -- set up nested reuse; `evalTactic` will check for `isIncrementalElab`
                 (tacSnap? := some { old? := oldInner?, new := inner }) do
-              evalTactic tac
+              Term.withReuseContext tac do
+                evalTactic tac
             finished.resolve { state? := state }
 
         withTheReader Term.Context ({ · with tacSnap? := some {

src/Lean/Elab/Term.lean

@@ -360,21 +360,39 @@ instance : MonadBacktrack SavedState TermElabM where
   saveState      := Term.saveState
   restoreState b := b.restore
 
+/--
+Incremental elaboration helper. Avoids leakage of data from outside syntax via the monadic context
+when running `act` on `stx` by
+* setting `stx` as the `ref` and
+* deactivating `suppressElabErrors` if `stx` is `missing`-free, which also helps with not hiding
+  useful errors in this part of the input. Note that if `stx` has `missing`, this should always be
+  true for the outer syntax as well, so taking the old value of `suppressElabErrors` into account
+  should not introduce data leakage.
+
+This combinator should always be used when narrowing reuse to a syntax subtree, usually (in the case
+of tactics, to be generalized) via `withNarrowed(Arg)TacticReuse`.
+-/
+def withReuseContext [Monad m] [MonadWithReaderOf Core.Context m] (stx : Syntax) (act : m α) :
+    m α := do
+  withTheReader Core.Context (fun ctx => { ctx with
+      ref := stx
+      suppressElabErrors := ctx.suppressElabErrors && stx.hasMissing }) act
+
 /--
 Manages reuse information for nested tactics by `split`ting given syntax into an outer and inner
 part. `act` is then run on the inner part but with reuse information adjusted as following:
 * If the old (from `tacSnap?`'s `SyntaxGuarded.stx`) and new (from `stx`) outer syntax are not
   identical according to `Syntax.eqWithInfo`, reuse is disabled.
 * Otherwise, the old syntax as stored in `tacSnap?` is updated to the old *inner* syntax.
-* In any case, we also use `withRef` on the inner syntax to avoid leakage of the outer syntax into
-  `act` via this route.
+* In any case, `withReuseContext` is used on the new inner syntax to further prepare the monadic
+  context.
 
 For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
 tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts.
 -/
-def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
-    [MonadOptions m] [MonadRef m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α)
-    (stx : Syntax) : m α := do
+def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Core.Context m]
+    [MonadWithReaderOf Context m] [MonadOptions m] (split : Syntax → Syntax × Syntax)
+    (act : Syntax → m α) (stx : Syntax) : m α := do
   let (outer, inner) := split stx
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
@@ -384,8 +402,7 @@ def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
       return { old with stx := oldInner }
     }
   }) do
-    withRef inner do
-      act inner
+    withReuseContext inner (act inner)
 
 /--
 A variant of `withNarrowedTacticReuse` that uses `stx[argIdx]` as the inner syntax and all `stx`
@@ -396,8 +413,8 @@ NOTE: child nodes after `argIdx` are not tested (which would almost always disab
 necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
 depend on them (i.e. they should not be inspected beforehand).
 -/
-def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Context m]
-    [MonadOptions m] [MonadRef m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
+def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Core.Context m] [MonadWithReaderOf Context m]
+    [MonadOptions m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
   withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
 
 /--

tests/lean/interactive/incrementalMutual.lean

@@ -64,3 +64,15 @@ def so : Nat := by
                --^ sync
                --^ insert: ".5"
   exact 0
+
+/-!
+Incomplete syntax should not suppress errors in previous definitions as that would prevent reuse.
+-/
+-- RESET
+mutual
+def e0 : Nat := doesNotExist
+def e1 : Nat := doesNotExist
+en
+--^ sync
+--^ insert: "d"
+--^ collectDiagnostics

tests/lean/interactive/incrementalMutual.lean.expected.out

@@ -29,3 +29,22 @@ nt 1
 so 0
 so 1
 so 1.5
+{"version": 2,
+ "uri": "file:///incrementalMutual.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 2, "character": 16}, "end": {"line": 2, "character": 28}},
+   "message": "unknown identifier 'doesNotExist'",
+   "fullRange":
+   {"start": {"line": 2, "character": 16},
+    "end": {"line": 2, "character": 28}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 3, "character": 16}, "end": {"line": 3, "character": 28}},
+   "message": "unknown identifier 'doesNotExist'",
+   "fullRange":
+   {"start": {"line": 3, "character": 16},
+    "end": {"line": 3, "character": 28}}}]}

tests/lean/interactive/incrementalTactic.lean

@@ -105,3 +105,16 @@ example : True := by
       --^ sync
       --^ insert: " "
       --^ collectDiagnostics
+
+/-!
+Incomplete syntax should not suppress errors in previous steps as that would prevent reuse.
+-/
+-- RESET
+---set_option trace.Elab.info true
+example : True := by
+  exact noSuchTheorem
+  skip
+  d
+--^ sync
+--^ delete: "d"
+--^ collectDiagnostics

tests/lean/interactive/incrementalTactic.lean.expected.out

@@ -109,3 +109,14 @@ s
    "message": "no goals to be solved",
    "fullRange":
    {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 8}}}]}
+{"version": 2,
+ "uri": "file:///incrementalTactic.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 21}},
+   "message": "unknown identifier 'noSuchTheorem'",
+   "fullRange":
+   {"start": {"line": 3, "character": 8},
+    "end": {"line": 3, "character": 21}}}]}