Recommended colors

Stream: general

[Martin Dvořák]

@Arthur Paulino pointed out that a good way to deal with characters that are hard to distinguish from each other is to change their color in VS Code. I could start developing a custom color scheme from scratch; however, before I do so, I would like to ask if somebody has already done the job.

Do you have a good color scheme for Lean in VS Code you would like to share?

[Arthur Paulino]

This would add extra steps to the Lean 4 setup: download extension X; download color scheme Y; set color scheme Y

If this is to become a community thing, it would be better if it were implemented in the lean4 VS Code extension, with a default color scheme coming out of the box.

Not to put your good intentions down @Martin Dvořák. I'm just coming up with an explanation as to why ppl might not have engaged with your proposal.

[Moritz Doll]

I have no specific color palette in mind, but some of the ones that are designed with colorblindness in mind look really good (imo better than more standard color schemes)

[Martin Dvořák]

I believe that a middle ground exists. Somebody can share their color scheme. Then a few Lean users (who care a lot about visual discernibility of characters, like I do) use it. I didn't expect the color scheme to go into the official installation instructions.

[Max Nowak 🐉]

Let me use this occasion to shill my improved semantic highlighting RFC :).

[Martin Dvořák]

I created a simple color settings for Lean 4 in VS Code:
https://github.com/madvorak/vscode-lean4-colors/blob/main/settings.json
It requires this extension:
https://marketplace.visualstudio.com/items?itemName=fabiospampinato.vscode-highlight
It is supposed to look nice only with dark color themes such as Monokai.

It works for me; however, it is very messy (horribly written).
Using it is not recommended, but improvements are welcome!

[Martin Dvořák]

image.png

[Jireh Loreaux]

It seems like there is less semantic distinction with this theme than with the default VS Code theme. Is there a reason?

[Eric Wieser]

I can tell you that these lines make that happen, but I can't tell you why that's useful

[Martin Dvořák]

Jireh Loreaux said:

It seems like there is less semantic distinction with this theme than with the default VS Code theme. Is there a reason?

I didn't like it colorful.

[Eric Wieser]

It would be cool if the semantic highlighter could attach scopes to notation based on the head symbol

[Eric Wieser]

That way you wouldn't have to resort to regex to do what you did there

[Alex J. Best]

I'm not sure if this is what you are saying, but you can get e.g. a red sorry with the following in your settings.json

    "editor.semanticTokenColorCustomizations": {
        "enabled": true,
        "rules": {"leanSorryLike": "#FF0000"},
    },

[Eric Wieser]

That's exactly what I meant; and I was suggesting that you could have some generated leanNotation.{headSymbolname} tokens to do things like highlight ands/ors/iffs as Martin does above

[Scott Morrison]

While people are thinking about colours, does anyone know the quickest route to having VSCode render
X says Y with Y in a faint grey? Semantic highlighting is not something I've learnt about yet!

[Martin Dvořák]

I find it pretty interesting how our deeply our preferences about code coloring differ.
(1) Some people (like me) want lexical highlighting only.
(2) Most people use syntactic highlighting.
(3) Some people want semantic highlighting (I totally support you; I just want it simple).

[Kevin Buzzard]

I feel like I'm missing out somehow because I have no idea what any of these options even mean and I suspect I pay no attention to what colour things are.

[Martin Dvořák]

Kevin Buzzard said:

I feel like I'm missing out somehow because I have no idea what any of these options even mean and I suspect I pay no attention to what colour things are.

Would you feel more comfortable with no coloring at all? I forgot to add option (0).

[Kevin Buzzard]

I don't care what the colours are

[Kevin Buzzard]

All I'm observing is that the fact that I'm not looking at the colours might mean I'm missing out on something, but I don't know what

[Martin Dvořák]

This question is more technical:
Does the lean4 extension in VS Code distinguish between keywords and tactics?
If I understand what I am looking at, both keywords and tactics have keyword.other as their semantic token type.

[Martin Dvořák]

Kevin Buzzard said:

All I'm observing is that the fact that I'm not looking at the colours might mean I'm missing out on something, but I don't know what

I wouldn't worry about it.

[Damiano Testa]

The colours definitely help me, since I find typing code in comments much harder than outside of comments, but I would not really know what kind of colouring I prefer. I am fairly happy with the status quo, but would likely also be happy with a different one!

[Martin Dvořák]

BTW, I have just learnt that displaying variables in italics is a bad idea because a and α look almost identical in italics [I am using JetBrains Mono; if you have a different experience with a different font, I might change my mind].

[Julian Berman]

There is a paper I saw somewhere where they investigated how coloring affected readability but I can't seem to find it in searching again.

But I think it boils down to "do you like looking at a screen that seems to have 4-6 colors going on, or one where there are >10 and barely any of the 10 colors is dominant"

[Julian Berman]

(The former being more like traditional syntax highlighting, and the latter is semantic highlighting giving lots more ability to differentiate between what kind of element a thing is and then people love making those super colorful)

[Martin Dvořák]

Julian Berman said:

do you like looking at a screen that seems to have 4-6 colors

I am definitely here.

[Julian Berman]

I actually also prefer the first and yet have semantic highlighting enabled because you can then tweak your own color scheme so that the 10+ colors are quite close to each other, such that they don't distract you, but if you have doubts, they're indeed slightly differing so you can then stare closely when needed

[Mario Carneiro]

Scott Morrison said:

While people are thinking about colours, does anyone know the quickest route to having VSCode render
X says Y with Y in a faint grey? Semantic highlighting is not something I've learnt about yet!

Yes, if you use the same semantic highlight used for "unused variables" then it will gray the text (and this works even if the text has other colors, it dims whatever it is)

[Scott Morrison]

I don't even know which repository I would be looking at to start making says Y highlight differently...

[Mario Carneiro]

unfortunately semantic highlighting is not user-extensible right now, so in order to do what I said you would have to emit a message data to which MessageData.isUnusedVariableWarning returns true (i.e. faking an output of the unusedVariables linter), and even if you do you will have to put a diagnostic over the span, so you get your choice of a red, yellow, or blue/green squiggle in addition to the faded text

[Mario Carneiro]

to do this properly you would need to PR to lean4 core

[Scott Morrison]

Okay. In that case I think it can be safely left until after we start using says!

[Johan Commelin]

How hard would it be to add the choice of "no squiggle"?

[Mario Carneiro]

the hard part would be making it sufficiently extensible that you don't need to define says in core to get any highlighting at all

[Max Nowak 🐉]

I wasn’t aware of a “says” tactic. I’m guessing it’s supposed to simply repeat the type of a variable in order to make tactic scripts more legible. In that case, just be aware we could go with inlay type hints similar to how rust-analyzer does it. This would come with problems though, such as those type hints not being in the actual code, so they wouldn’t show up on GitHub. But users could customize which hints they want to show. I haven’t looked into this.

[Julian Berman]

neovim recently got support for inlay hints (and emacs has them too IIRC). But yeah that would be quite nice to start taking advantage of for some sort of use

[Sebastian Ullrich]

Max Nowak 🐺 said:

I’m guessing it’s supposed to simply repeat the type of a variable in order to make tactic scripts more legible

No, the intention is to run the fast, verbose version while keeping the original version around for re-generation. See #5980 for details.

[Eric Wieser]

Mario Carneiro said:

the hard part would be making it sufficiently extensible that you don't need to define says in core to get any highlighting at all

Presumably we could have some kind of generated syntax marker (that core knows about) that the says notation attaches to the RHS?

[Martin Dvořák]

Level up!
image.png
I am pretty sure some of the lines in
https://github.com/madvorak/vscode-lean4-colors/blob/main/settings.json
are redundant; however, I am loo lazy to refactor it.

[Martin Dvořák]

FYI, I updated my color settings:
https://github.com/madvorak/vscode-lean4-colors

Even if you don't like my esthetic preferences, you might find it useful because it shows how to override the defaults.