VS Code color scheme

Stream: general

[Martin Dvořák]

Do you have a recommendation for a good color scheme for Lean in VS Code?

About a month ago, my VS Code spontaneously decided to color pairs of brackets in addition to highlighting the keywords by colors. It is a bit distracting for me since it is too much colors. What is your preferred setting?

[Julian Berman]

I'm no expert but I think VS Code changed the default for bracket pair colorization. If it's just that that bothers you, the setting is Preferences > Settings > Bracket Pair Colorization (and untick the box)

[Martin Dvořák]

I'm considering keeping the bracket pair colorization but turning off the keyword colorization. However, I would then like to change the color scheme so that all bracket pairs are noticeably different from black. Currently, the brown color doesn't do for me.

[Martin Dvořák]

Will anyone share what their favorite color scheme is? I have some ideas about what I might like but I don't know whether it will be good for my productivity in the long term.

[Alex J. Best]

Well this is very personal, and I don't know if it actually changes productivity but I use Jellybeams from "Jellybeams Theme" in the extensions tab, gerane.Theme-Jellybeams.
I also have it set up in the settings json file to make sorry a very bright red with the following:

    "editor.tokenColorCustomizations" : {
        "textMateRules": [                {
                    "scope": "invalid.illegal.lean",
                    "settings": {
                        "foreground": "#FF0000"
                    }
                }, ],
    },

[Gabriel Ebner]

I think the best choice for productivity is "Light+ (default light)". The less time you spend choosing a color, the more time you can spend on Lean! :smile:

[Yaël Dillies]

Personally I like Quiet Light (also because I'm colorblind).

[Anne Baanen]

My default colourscheme is Solarized light, although I agree with Gabriel that productivity generally doesn't involve choosing the colour of a bike shed :)

[Eric Rodriguez]

I use "Dark+", but that's just because I personally tend to find light-themes eye burning

[Martin Dvořák]

Thanks for your answers!

[Martin Dvořák]

I believe that the color scheme influences my productivity because most of the working time is spent on reading the code. And if colors hint meaningful information, I can skip over the unimportant parts faster.

[Martin Dvořák]

Eric Rodriguez said:

I use "Dark+", but that's just because I personally tend to find light-themes eye burning

Oh. I wasn't talking about Color themes originally. I was interested in configuring the syntax highlighter.

[Eric Wieser]

The syntax highlighting unfortunately doesn't have access to much semantic information in lean3; it's all heuristic, and since lean lets you define arbitrary syntax every heuristic is guaranteed to fail somewhere

[Eric Wieser]

Lean 4's language server has a fundamentally different design that largely avoids this issue

[Sebastian Ullrich]

In fact, @Leonardo de Moura found out that many color schemes more or less ignore the semantic information sent from the Lean 4 language server. So there the choice becomes more meaningful again.

[Patrick Massot]

How can we check whether our theme is affected?

[Eric Wieser]

I think there's a similar problem with C++ in vscode, where they ship special C++ versions of color schemes (in a separate extension) because the built-in ones don't respect that info.

Edit: https://marketplace.visualstudio.com/items?itemName=ms-vscode.cpptools-themes

[Leonardo de Moura]

Correct. The good news is that we can provide our own customization for an existing color scheme.
Here is the configuration I use:

    "workbench.colorTheme": "Solarized Light",
    "editor.semanticHighlighting.enabled": true,
    "workbench.colorCustomizations": {
      "[Solarized Light]": {"editor.selectionHighlightBackground": "#e9dcc5"}
    },
    "editor.semanticTokenColorCustomizations": {
      "[Solarized Light]": {"rules": {"function": "#c1892f"}}
    },

[Martin Dvořák]

Eric Wieser said:

The syntax highlighting unfortunately doesn't have access to much semantic information in lean3; it's all heuristic, and since lean lets you define arbitrary syntax every heuristic is guaranteed to fail somewhere

Yes but I doubt we will redefine which bracket closes which bracket. Hence this type of syntax coloring might be still useful.

[Eric Wieser]

It's not too uncommon to write $[0, 1)$ on paper...

[Martin Dvořák]

True. Is it idiomatic in Lean/mathlib as well?

[Yaël Dillies]

No, we write out Ico.

[Sebastian Ullrich]

It would be possible to robustly define this notation using whitespace sensitivity in Lean 4, but it's probably still a very bad idea because it will definitely confuse editors

[Martin Dvořák]

Does "editor.semanticHighlighting.enabled": true do anything for Lean?