fix: incremental reuse leading to goals in front of the text cursor b…

…eing shown (#4395)

As [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/maybe.20a.20cache.20bug.3F).

We expected that for sound reuse of elaboration results, it is
sufficient to compare the old and new syntax tree's structure and atoms
including position info, but not the whitespace in between them.
However, we have at least one request handler, the goal view, that
inspects the whitespace after a tactic and thus could return incorrect
results on reuse. For now we implement the straightforward fix of
checking the whitespace as well. Alternatives like updating the
whitespace stored in the reused info tree are tbd.

This has the slight disadvantage that adding whitespace at the end of a
tactic will re-execute it (or the entire body, but not the header, if
the body is not a tactic block), but only up to typing the first
character of the next tactic or command.

src/Lean/Elab/Command.lean

@@ -420,7 +420,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                         return { stx := (← oldCmd?), val := (← old.next[i]?) }
                     } }) do
                       elabCommand cmd
-                    reusedCmds := reusedCmds && oldCmd?.any (·.structRangeEqWithTraceReuse opts cmd)
+                    reusedCmds := reusedCmds && oldCmd?.any (·.eqWithInfoAndTraceReuse opts cmd)
               else
                 elabCommand stxNew
         | _ =>

src/Lean/Elab/MutualDef.lean

@@ -155,7 +155,7 @@ private def elabHeaders (views : Array DefView)
           -- headers and all previous bodies could be reused and this body syntax is unchanged, then
           -- we can reuse the result
           reuseBody := reuseBody &&
-            view.value.structRangeEqWithTraceReuse (← getOptions) old.bodyStx
+            view.value.eqWithInfoAndTraceReuse (← getOptions) old.bodyStx
           -- no syntax guard to store, we already did the necessary checks
           oldBodySnap? := guard reuseBody *> pure ⟨.missing, old.bodySnap⟩
           oldTacSnap? := do
@@ -977,7 +977,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
             -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick
             let old ← old.val.get.toTyped? DefsParsedSnapshot
             let oldParsed ← old.defs[i]?
-            guard <| fullHeaderRef.structRangeEqWithTraceReuse opts oldParsed.fullHeaderRef
+            guard <| fullHeaderRef.eqWithInfoAndTraceReuse opts oldParsed.fullHeaderRef
             -- no syntax guard to store, we already did the necessary checks
             return ⟨.missing, oldParsed.headerProcessedSnap⟩
           new := headerPromise

src/Lean/Elab/Term.lean

@@ -333,7 +333,7 @@ instance : MonadBacktrack SavedState TermElabM where
 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.structRangeEq`, reuse is disabled.
+  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.
@@ -349,7 +349,7 @@ def withNarrowedTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithRead
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
     { tacSnap with old? := tacSnap.old?.bind fun old => do
       let (oldOuter, oldInner) := split old.stx
-      guard <| outer.structRangeEqWithTraceReuse opts oldOuter
+      guard <| outer.eqWithInfoAndTraceReuse opts oldOuter
       return { old with stx := oldInner }
     }
   }) do

src/Lean/Syntax.lean

@@ -33,6 +33,8 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
 def SourceInfo.getRange? (canonicalOnly := false) (info : SourceInfo) : Option String.Range :=
   return ⟨(← info.getPos? canonicalOnly), (← info.getTailPos? canonicalOnly)⟩
 
+deriving instance BEq for SourceInfo
+
 /-! # Syntax AST -/
 
 inductive IsNode : Syntax → Prop where
@@ -84,9 +86,11 @@ end SyntaxNode
 namespace Syntax
 
 /--
-Compare syntax structures and position ranges, but not whitespace.
-We generally assume that if syntax trees equal in this way generate the same elaboration output,
-including positions contained in e.g. diagnostics and the info tree.
+Compares syntax structures and position ranges, but not whitespace. We generally assume that if
+syntax trees equal in this way generate the same elaboration output, including positions contained
+in e.g. diagnostics and the info tree. However, as we have a few request handlers such as `goalsAt?`
+that are sensitive to whitespace information in the info tree, we currently use `eqWithInfo` instead
+for reuse checks.
 -/
 partial def structRangeEq : Syntax → Syntax → Bool
   | .missing, .missing => true
@@ -111,6 +115,30 @@ def structRangeEqWithTraceReuse (opts : Options) (stx1 stx2 : Syntax) : Bool :=
     else
       false
 
+
+/-- Full comparison of syntax structures and source infos.  -/
+partial def eqWithInfo : Syntax → Syntax → Bool
+  | .missing, .missing => true
+  | .node info k args, .node info' k' args' =>
+    info == info' && k == k' && args.isEqv args' eqWithInfo
+  | .atom info val, .atom info' val' => info == info' && val == val'
+  | .ident info rawVal val preresolved, .ident info' rawVal' val' preresolved' =>
+    info == info' && rawVal == rawVal' && val == val' && preresolved == preresolved'
+  | _, _ => false
+
+/-- Like `eqWithInfo` but prints trace on failure if `trace.Elab.reuse` is activated. -/
+def eqWithInfoAndTraceReuse (opts : Options) (stx1 stx2 : Syntax) : Bool :=
+  if stx1.eqWithInfo stx2 then
+    true
+  else
+    if opts.getBool `trace.Elab.reuse then
+      dbg_trace "reuse stopped:
+{stx1.formatStx (showInfo := true)} !=
+{stx2.formatStx (showInfo := true)}"
+      false
+    else
+      false
+
 def getAtomVal : Syntax → String
   | atom _ val => val
   | _          => ""

tests/lean/interactive/incrementalTactic.lean

@@ -11,6 +11,10 @@ def basic : True := by
               --^ sync
               --^ insert: ".5"
 
+/-!
+Ideally trailing whitespace should be ignored. CURRENTLY NOT WORKING as we use `Syntax.eqWithInfo`;
+we will need to patch old syntax info stored in the info tree to go back to `Syntax.structRangeEq`.
+-/
 -- RESET
 def trailingWhitespace : True := by
   dbg_trace "t 0"
@@ -51,3 +55,19 @@ def strayToken : True := by
   unfold f
         --^ sync
         --^ insert: " -"
+
+/-!
+Insufficient reuse checking of trailing whitespace info in the info tree led to the goal view
+showing multiple tactics as they all claimed to be at the end of the file (which they were in prior
+versions).
+-/
+-- RESET
+def dup_goals : True := by
+  show True
+--^ sync
+--^ insert: "show True\n  show True\n  show True\n  show True\n  "
+
+--^ sync
+--^ goals
+-- (note that request positions are computed relative to the original document, so the checks above
+-- will point at a `show` at run time)

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

@@ -5,6 +5,7 @@ b 2.5
 t 0
 t 1
 t 2
+t 2
 {"version": 3,
  "uri": "file:///incrementalTactic.lean",
  "diagnostics":
@@ -54,3 +55,10 @@ t 2
    {"start": {"line": 3, "character": 9},
     "end": {"line": 3, "character": 16}}}]}
 s
+{ goals := #[{ type := Lean.Widget.TaggedText.tag
+                         { subexprPos := "/", diffStatus? := none }
+                         (Lean.Widget.TaggedText.text "True"),
+               isInserted? := some false,
+               isRemoved? := none,
+               hyps := #[] }] }
+