Zulip Chat Archive
Stream: lean4
Topic: Language Server: leanSorryLike not found in ":= sorry"
Oliver Dressler (Dec 22 2024 at 10:55):
I am working on interfacing with the language server and have a question about leanSorryLike:
Requesting "textDocument/semanticTokens/full" from the following single line file:
theorem add_zero_custom (n : Nat) : n + 0 = n := sorry
I get the following tokens:
[[0, 0, 7, 'keyword', []],
[0, 25, 1, 'variable', []],
[0, 36, 1, 'variable', []],
[0, 44, 1, 'variable', []]]
However, using "by sorry" detects a leanSorryLike token:
theorem add_zero_custom (n : Nat) : n + 0 = n := by sorry
[[0, 0, 7, 'keyword', []],
[0, 25, 1, 'variable', []],
[0, 36, 1, 'variable', []],
[0, 44, 1, 'variable', []],
[0, 49, 2, 'keyword', []],
[0, 52, 5, 'leanSorryLike', []]]
Is this expected behavior?
In mathlib 4.14 there are 58 occurences of ":= sorry" vs 12 ":= by sorry".
UPDATE: It seems the difference is between sorry
as:
- Lean.ParserTerm.sorry
sorry
used in a tactic block opened byby
The former is excluded from Syntax Hightlighting at
https://github.com/leanprover/lean4/blob/410fab7284703f41660ca2454218dcca9b2ec896/src/Lean/Server/FileWorker/RequestHandling.lean#L430
However, it would still be nice to have both reported as leanSorryLike, since they seem to be used interchangeably.
Last updated: May 02 2025 at 03:31 UTC