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 by by

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