From 7b3c64fc85ebfb2bb0f9a583c7a4cb854f1be856 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 24 Jul 2024 15:08:01 +0200 Subject: [PATCH] feat: trailing whitespace changes should not invalidate imports (#4580) Thus, starting to type the first declaration after the imports should not make them reload --- src/Init/Meta.lean | 9 ++++- src/Lean/Language/Lean.lean | 40 +++++++++++-------- .../lean/interactive/incrementalCommand.lean | 12 ++++++ .../incrementalCommand.lean.expected.out | 20 ++++++++++ 4 files changed, 63 insertions(+), 18 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 1749f13274c9..a94567095a01 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -399,9 +399,16 @@ def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax := | some stx => stx | none => stx +/-- +Replaces the trailing whitespace in `stx`, if any, with an empty substring. + +The trailing substring's `startPos` and `str` are preserved in order to ensure that the result could +have been produced by the parser, in case any syntax consumers rely on such an assumption. +-/ def unsetTrailing (stx : Syntax) : Syntax := match stx.getTailInfo with - | SourceInfo.original lead pos _ endPos => stx.setTailInfo (SourceInfo.original lead pos "".toSubstring endPos) + | SourceInfo.original lead pos trail endPos => + stx.setTailInfo (SourceInfo.original lead pos { trail with stopPos := trail.startPos } endPos) | _ => stx @[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) := diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 355d45545bcb..c1b4375a769f 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -362,16 +362,16 @@ where parseHeader (old? : Option HeaderParsedSnapshot) : LeanProcessingM HeaderParsedSnapshot := do let ctx ← read let ictx := ctx.toInputContext - let unchanged old newParserState := + let unchanged old newStx newParserState := -- when header syntax is unchanged, reuse import processing task as is and continue with -- parsing the first command, synchronously if possible - -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still - -- have changed because of trailing whitespace and comments etc., so it is passed separately - -- from `old` + -- NOTE: even if the syntax tree is functionally unchanged, its concrete structure and the new + -- parser state may still have changed because of trailing whitespace and comments etc., so + -- they are passed separately from `old` if let some oldSuccess := old.result? then return { ictx - stx := old.stx + stx := newStx diagnostics := old.diagnostics cancelTk? := ctx.newCancelTk result? := some { oldSuccess with @@ -394,7 +394,7 @@ where if let some nextCom ← processed.firstCmdSnap.get? then if (← isBeforeEditPos nextCom.data.parserState.pos) then -- ...go immediately to next snapshot - return (← unchanged old oldSuccess.parserState) + return (← unchanged old old.stx oldSuccess.parserState) withHeaderExceptions ({ · with ictx, stx := .missing, result? := none, cancelTk? := none }) do @@ -408,16 +408,19 @@ where cancelTk? := none } - -- semi-fast path: go to next snapshot if syntax tree is unchanged AND we're still in front - -- of the edit location - -- TODO: dropping the second condition would require adjusting positions in the state - -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if - -- only that whitespace changes, which is wasteful but still necessary because it may - -- influence the range of error messages such as from a trailing `exact` + let trimmedStx := stx.unsetTrailing + -- semi-fast path: go to next snapshot if syntax tree is unchanged + -- NOTE: We compare modulo `unsetTrailing` in order to ensure that changes in trailing + -- whitespace do not invalidate the header. This is safe because we only pass the trimmed + -- syntax tree to `processHeader` below, so there cannot be any references to the trailing + -- whitespace in its result. We still store the untrimmed syntax tree in the snapshot in order + -- to uphold the invariant that concatenating all top-level snapshots' syntax trees results in + -- the original file. if let some old := old? then - if (← isBeforeEditPos parserState.pos) && old.stx == stx then - -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged` - return (← unchanged old parserState) + if trimmedStx.eqWithInfo old.stx.unsetTrailing then + -- Here we must make sure to pass the *new* syntax and parser state; see NOTE in + -- `unchanged` + return (← unchanged old stx parserState) -- on first change, make sure to cancel old invocation if let some tk := ctx.oldCancelTk? then tk.set @@ -426,7 +429,7 @@ where diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog) result? := some { parserState - processedSnap := (← processHeader stx parserState) + processedSnap := (← processHeader trimmedStx parserState) } cancelTk? := ctx.newCancelTk } @@ -523,7 +526,10 @@ where -- semi-fast path if let some old := old? then - if (← isBeforeEditPos parserState.pos ctx) && old.data.stx == stx then + -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if + -- only that whitespace changes, which is wasteful but still necessary because it may + -- influence the range of error messages such as from a trailing `exact` + if stx.eqWithInfo old.data.stx then -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged` return (← unchanged old parserState) -- on first change, make sure to cancel old invocation diff --git a/tests/lean/interactive/incrementalCommand.lean b/tests/lean/interactive/incrementalCommand.lean index 80073dfc0ad1..b760906119a3 100644 --- a/tests/lean/interactive/incrementalCommand.lean +++ b/tests/lean/interactive/incrementalCommand.lean @@ -55,3 +55,15 @@ example : False := by interrupt simp --^ collectDiagnostics + +/-! +Trailing whitespace should not invalidate the module header. Note that in case of a regression, this +test case will currently deadlock. In any case, it should not succeed as interactive tests +communicate with one worker process only. +-/ +-- RESET +import Init.Prelude + --^ collectDiagnostics + --^ insert: " " + --^ collectDiagnostics +#eval "import" diff --git a/tests/lean/interactive/incrementalCommand.lean.expected.out b/tests/lean/interactive/incrementalCommand.lean.expected.out index 58fc2d238b16..4ad2601d9b98 100644 --- a/tests/lean/interactive/incrementalCommand.lean.expected.out +++ b/tests/lean/interactive/incrementalCommand.lean.expected.out @@ -3,3 +3,23 @@ w w {"version": 1, "uri": "file:///incrementalCommand.lean", "diagnostics": []} +{"version": 1, + "uri": "file:///incrementalCommand.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}, + "message": "\"import\"\n", + "fullRange": + {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]} +{"version": 2, + "uri": "file:///incrementalCommand.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 3, + "range": + {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}, + "message": "\"import\"\n", + "fullRange": + {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]}