From adfd438164579eec66a885182b436a052df88e53 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 8 Jun 2024 17:08:14 +0200 Subject: [PATCH] fix: incremental reuse leading to goals in front of the text cursor being 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 | 2 +- src/Lean/Elab/MutualDef.lean | 4 +-- src/Lean/Elab/Term.lean | 4 +-- src/Lean/Syntax.lean | 34 +++++++++++++++++-- tests/lean/interactive/incrementalTactic.lean | 20 +++++++++++ .../incrementalTactic.lean.expected.out | 8 +++++ 6 files changed, 64 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index fb0f5b8151..aa2b5a9d2f 100644 --- a/src/Lean/Elab/Command.lean +++ b/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 | _ => diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index ffc333adf5..b59cc73330 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 317a9f749e..4bbdb2757e 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 06c09e16d2..a64999dd0b 100644 --- a/src/Lean/Syntax.lean +++ b/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 | _ => "" diff --git a/tests/lean/interactive/incrementalTactic.lean b/tests/lean/interactive/incrementalTactic.lean index e5e153eeed..25aa68e46e 100644 --- a/tests/lean/interactive/incrementalTactic.lean +++ b/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) diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out index 6b79256e2c..9417b2fa17 100644 --- a/tests/lean/interactive/incrementalTactic.lean.expected.out +++ b/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 := #[] }] } +