fix: incremental goal state requests select incomplete snapshot #6887
Conversation
| inner? := some { range?, task := inner.result } | ||
| finished := { range?, task := finished.result } | ||
| next := #[{ range? := stxs.getRange?, task := next.result }] | ||
| inner? := some { stx? := tac, reportingRange? := range?, task := inner.result } |
There was a problem hiding this comment.
range? should be unnecessary now, right? findInfoTreeAtPos/findGoalsAt? doesn't use it anymore
There was a problem hiding this comment.
I've removed the range hack.
| stx? := mkNullNode altStxs | ||
| reportingRange? := none |
There was a problem hiding this comment.
This special case seems worthy of a comment
There was a problem hiding this comment.
(We discussed this and came to the conclusion that it's not a special case)
| match cmdParsed.nextCmdSnap? with | ||
| | some next => next.task.bind (sync := true) go | ||
| | none => .pure none |
There was a problem hiding this comment.
We can return early if hoverPos is before cmdParsed
src/Lean/Server/Requests.lean
Outdated
| Task (Option CommandParsedSnapshot) := Id.run do | ||
| /-- Finds the first `CommandParsedSnapshot` containing `hoverPos`, asynchronously. -/ | ||
| partial def findCmdParsedSnap (doc : EditableDocument) (hoverPos : String.Pos) | ||
| (config : Language.SnapSelectionConfig) : Task (Option CommandParsedSnapshot) := Id.run do |
There was a problem hiding this comment.
What is an example where we do not want to include stop/trailing in findCmdParsedSnap? Isn't this only relevant when we get to nesting, i.e. in the info tree?
There was a problem hiding this comment.
I've adjusted the command snapshot selection logic so that it doesn't need a config.
- Get rid of command snap selection config - Remove tactic reporting range hack
This PR fixes a bug where the goal state selection would sometimes select incomplete incremental snapshots on whitespace, leading to an incorrect "no goals" response. Fixes #6594, a regression that was originally introduced in 4.11.0 by #4727.
The fundamental cause of #6594 was that the snapshot selection would always select the first snapshot with a range that contains the cursor position. For tactics, whitespace had to be included in this range. However, in the test case of #6594, this meant that the snapshot selection would also sometimes pick a snapshot before the cursor that still contains the cursor in its whitespace, but which also does not necessarily contain all the information needed to produce a correct goal state. Specifically, at the
InfoTree-level, when the cursor is in whitespace, we distinguish competing goal states by their level of indentation. The snapshot selection did not have access to this information, so it necessarily had to do the wrong thing in some cases.This PR fixes the issue by adjusting the snapshot selection for goals to explicitly account for whitespace and indentation, and refactoring the language processor architecture to thread enough information through to the snapshot selection so that it can decide which snapshots to use without having to force too many tasks, which would destroy incrementality in goal state requests.
Specifically, this PR makes the following adjustments:
SnapshotTaskto contain both aSyntaxand aRange. Before,SnapshotTasks had a single range that was used both for displaying file progress information and for selecting snapshots in server requests. For most snapshots, this range did not include whitespace, though for tactics it did. Now, thereportingRangefield ofSnapshotTaskis intended exclusively for reporting file progress information, and theSyntaxis used for selecting snapshots in server requests. Importantly, theSyntaxcontains the full range information of the snapshot, i.e. its regular range and its range including whitespace.SnapshotTaskto produce a reasonableSyntax.InfoTreegoal selection does.Infoof a snapshot at the wrong location whentrace.Elab.infowas also set.This PR is based on #6329.