Restore fullRange handling
#392
Labels
bug
Something isn't working
Comments
|
Hah, so that's what that field was for! This is technically documented here, but I had no idea what it meant operationally until seeing the explanation above. |
This was referenced Mar 5, 2024
github-merge-queue bot
pushed a commit
to leanprover/lean4
that referenced
this issue
Mar 5, 2024
This bug is the real cause of leanprover/vscode-lean4#392. At the end of a tactic state, the client calls `getInteractiveDiagnostics` with a range `[last line of proof, last line of proof + 1)`. The `fullRange` span of the `unresolved goals` error however is something like `[(first line of proof, start character), (last line of proof, nonzero end character)). Since it operates on line numbers, `getInteractiveDiagnostics` would then check whether `[last line of proof, last line of proof + 1)` and `[first line of proof, last line of proof)` intersect, which is false because of the excluded upper bound on the latter interval, despite the fact that the end character in the last line may be nonzero. This fix adjusts the intersection logic to use `[first line of proof, last line of proof]` if the end character is nonzero. Closes leanprover/vscode-lean4#392.
tydeu
pushed a commit
to tydeu/lean4
that referenced
this issue
Mar 11, 2024
This bug is the real cause of leanprover/vscode-lean4#392. At the end of a tactic state, the client calls `getInteractiveDiagnostics` with a range `[last line of proof, last line of proof + 1)`. The `fullRange` span of the `unresolved goals` error however is something like `[(first line of proof, start character), (last line of proof, nonzero end character)). Since it operates on line numbers, `getInteractiveDiagnostics` would then check whether `[last line of proof, last line of proof + 1)` and `[first line of proof, last line of proof)` intersect, which is false because of the excluded upper bound on the latter interval, despite the fact that the end character in the last line may be nonzero. This fix adjusts the intersection logic to use `[first line of proof, last line of proof]` if the end character is nonzero. Closes leanprover/vscode-lean4#392.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The language server reports diagnostics with a custom
fullRangefield that defines an extended range where the message should be considered "active" by the info view without being highlighted in the editor. This is absolutely crucial for e.g. working with indentation-based tactics. Unfortunately, the handling code seems to have been lost in a refactoring:before: https://github.com/leanprover/vscode-lean4/pull/30/files#diff-a5cd783b2942aa4bce645a2be9e41bbdbc782a2a545d5523046ef4889333b19cL73 (unfold
infoview/messages.ts)after: https://github.com/leanprover/vscode-lean4/pull/30/files#diff-f3205301d3c8487365c663b3f0147c3cb14360f4d68f4409554ad27328c56025R118
Broken example:
(not sure why it works on the first
apply, might be a off-by-one in either the server or the client)The text was updated successfully, but these errors were encountered: