Better semantic highlighting

Stream: lean4

[Max Nowak 🐉]

I have experimented a little bit with improving semantic highlighting,
and before I continue working on this: Would a PR be appreciated?
I understand if there are other priorities at the moment, I have read the contributing guidelines;
worst case this was some fun Lean practice for myself :).
If a PR is desired, I can clean up the code and improve things further.

This is what I have so far.

image.png
image.png
image.png

It's less about the color choice, and more about the semantic tokens that you can use to
customize your editor to your liking.
The LSP allows tokens to have exactly one token type, and any amount of token modifiers,
written tokentype.mod₁.mod₂.mod₃, which can be easily customized in your VSCode settings.json.
It is possible to introduce new token types and modifiers.

All the information is already there, I didn't do much other than add some extra cases.
You can very easily check whether a constant is a typeclass by reading the Environment.
Even invoking typeclass synthesis to check whether a type is a monad didn't immediately
destroy performance, which surprised me, but I didn't measure timings.

[Mario Carneiro]

My main concern would be that it will be a lot harder to get a good out of the box experience with standard themes. Most themes are already not suitable because they don't differentiate the 'variable' semantic token, which is critical for finding autoimplicits

[Mario Carneiro]

It's way too much to expect end users to customize all those types to a variety of colors

[Max Nowak 🐉]

That is my concern as well. Re-using as many of the existing token types and modifiers is one (bad, imo) solution. I think the simplest and easiest solution would be to provide a fork of the standard VSCode theme(s) that has been adapted to Lean?

[Max Nowak 🐉]

That way you can tell busy users to "just quickly install this theme, or you can copy-paste this json snippet into your settings.json".

[Mac Malone]

Max Nowak 🐺 said:

That is my concern as well. Re-using as many of the existing token types and modifiers is one (bad, imo) solution. I think the simplest and easiest solution would be to provide a fork of the standard VSCode theme(s) that has been adapted to Lean?

Re-using existing token types and modifiers is the heavily recommended standard practice it comes to LSP and VSCode. When customization is necessary, custom modifiers are much more acceptable than custom token types (as a custom token type gives basic themes and LSP clients no reasonable defaulting for highlighting).

[Mac Malone]

As for forking themes, that seems impractical as the variety of themes used in the community almost certainly far exceeds the ability to maintain forks.

[Mac Malone]

However, if this was togglable or if the improvements just relied on custom modifiers then it would be possible to support standard usage while still providing something nicer for power users. So, that may be an option.

[Max Nowak 🐉]

Yeah, I will try to reuse as many token types and modifiers as possible. Problem is that the LSP was not architected with functional languages in mind, so often there just aren't suitable token types. Currently Person is marked up as type.type.struct, but it would be possible to instead mark it up as struct.type. Similar for types which are typeclasses, which would get the existing interface token type. I'll play around with this, but I'm open to suggestions of course.

I was thinking of only forking one theme, like the default VSCode theme, for users who want to get started with Lean. From what I see, a lot of people simply use the default VSCode theme and are happy with it.

The existing semantic highlighting is very bare-bones, this would be a superset of what we have now.

[Mario Carneiro]

You shouldn't get too hung up on the names like interface et al. Just look at how the token types are used in common themes

[Mario Carneiro]

Theming is a many-to-many synchronization problem (between many LSP servers / languages and many themes), so the common interface is obviously not going to be a great semantic fit for everyone

[Reid Barton]

Is there a token type for "variable introduced by autoImplicit"?

[Mario Carneiro]

you can query the token scopes explicitly using "Developer: Inspect Editor Tokens and Scopes"

[Mario Carneiro]

the answer appears to be no, both x and y are described as variable.other.readwrite here:

def foo (x : Nat) : x = y := sorry

[Sebastian Ullrich]

Reid Barton said:

Is there a token type for "variable introduced by autoImplicit"?

Needs more testing: https://github.com/Kha/lean4/commit/923a1488efd302c0118545493bc91d9060ffddbf

[Max Nowak 🐉]

I haven't had time to work further on this, but I may have some time this week. This would be my first contribution to the Lean itself. Should I make an RFC as outlined in the contributing guidelines first, before I polish up the code? Sorry for necro.