Semantic highlighting limit reached?

Stream: lean4

[Mario Carneiro]

Could someone else confirm that syntax highlighting stops about here when you open Std.Data.List.Lemmas?

[Mario Carneiro]

I suspect the issue is that an upper bound on the number of tokens is being reached

[Mario Carneiro]

it's on line 1523, which is big but not that big, so I think we might need to bump the limit if that is the issue

[Mario Carneiro]

there are 75 files in mathlib which are longer than that

[Mario Carneiro]

for a mathlib example, highlighting peters out on line 1833 of Mathlib.Data.Fin.Basic. (mathlib uses its tokens a bit more sparingly than std because of the #align lines)

[Kyle Miller]

I see most syntax highlighting still, but around that line I can confirm that variables stop being blue (and deleting declarations to move things earlier causes their variables to become blue).

[Mario Carneiro]

right, that's the semantic highlighting

[Mario Carneiro]

the basic syntax highlighting is regex based and not supplied by the lean server

[Mario Carneiro]

I tried stressing the semantic highlighting by making many copies of

example (x : Nat) := [x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x,x]

(which should have 40 tokens if I counted correctly) but I was able to make over 4000 lines of that without losing semantic highlighting, so maybe something else is at work

[Gabriel Ebner]

Can repro in both vscode and neovim.

[Gabriel Ebner]

65 kilobytes should be enough for everyone.

def handleSemanticTokensFull (_ : SemanticTokensParams)
    : RequestM (RequestTask SemanticTokens) := do
  handleSemanticTokens 0 ⟨1 <<< 16⟩

[Sebastian Ullrich]

Now with special extended support for up to 2GB

[Max Nowak 🐉]

Yeah just changing that value to something bigger fixes it.

[Max Nowak 🐉]

I... may have gotten carried away at one point and improved the semantic highlighting (I know, should have asked whether a PR is desired first..). You can easily add more cases in the code for handleSemanticTokens, and you can distinguish propositions from types, check whether something is structure-like or a projection function or not, etc etc etc.

[Max Nowak 🐉]

Also whenever you add/remove imports, the semantic highlighting just stops and you have to close&open the vscode tab.