VS Code syntax highlighting

Stream: lean4

[Heather Macbeth]

@Trebor Huang Thanks! I tried this, VS Code is insisting that it's displaying green text (#008000) despite the evidence of my eyes.
Screen-Shot-2022-12-08-at-6.35.23-PM.png

[Matej Penciak]

I can confirm that this is also happening for me:

image.png

(#7B9246 is the usual Green for comments)

[Matej Penciak]

Interestingly, it doesn't happen on other repositories I'm working on (which are, unsurprisingly, a lot smaller than Mathlib4)

image.png

[Kevin Buzzard]

I'm pretty sure it doesn't happen with mathlib3, or else we would have noticed this long ago!

[Mario Carneiro]

I'm pretty sure that's caused by an out of date semantic highlighting cache

[Mario Carneiro]

That is, lean sent some semantic highlighting spans saying import should be blue, and then you commented out the import and for whatever reason the re-elaboration job got delayed or lost and the server never sent an update saying that it shouldn't be blue anymore because it's in a comment. You still get the comment in green because the standard regex highlighter is being run by vscode directly, but it's just doing it's best to preserve the semantic highlighting spans until it hears back from lean

[Mario Carneiro]

As a test, next time it happens try commenting out a whole block of text, not just the import line. I would predict that all the variables and theorem names are still colored

[Mario Carneiro]

even in normal operation this persists for a few seconds

[Heather Macbeth]

Thanks Mario, that's very instructive.

If the server's updates about semantic highlighting are buggy in this way, would it be worth using only the regex highlighter run by vscode directly? What features would I lose?

[Mario Carneiro]

The semantic highlighting is super useful in lean 4, because the set of keywords and tactics is user-extensible

[Mario Carneiro]

semantic highlighting enables the following:

• Highlighting linear_combination like a keyword
• Highlighting local variables
  • Highlighting auto-bound variables (really important for bug catching!)
• highlighting variables inside interpolated strings like s!"{foo} + {bar}" (which is helpful if you write "{foo} + {bar}" instead and notice it's not highlighted)

[Heather Macbeth]

Thanks to this conversation I'm reading the Lean 4 manual section on semantic highlighting for the first time. I was going to object to this part of your comment
Mario Carneiro said:

semantic highlighting enables the following:

• Highlighting local variables

until I saw from the manual that

this may be insufficient if your color theme does not distinguish enough syntax categories or distinguishes them very subtly. For instance the default Light+ theme uses color #001080 for variables. This is awfully close to #000000 that is used as the default text color. This makes it very easy to miss an accidental use of auto bound implicit arguments. For instance in

def my_id (n : nat) := n

maybe nat is a typo and Nat was intended. If your color theme is good enough then you should see that n and nat have the same color since they are both marked as variables by semantic highlighting.

[Heather Macbeth]

Can someone recommend a VS Code light theme for Lean 4 which has all syntax categories unambiguous?

[Mario Carneiro]

the best one among the light themes I have installed is Solarized Light

[Mario Carneiro]

the dark themes have much clearer coloration it seems

[Heather Macbeth]

Thanks!

[Heather Macbeth]

Now that I see what semantic highlighting can do for me I am less enthused about the simple solution of throwing it out the window :)

[Mario Carneiro]

I think that lean might just be using the wrong textmate scopes here. Many themes have pictures that clearly indicate some good highlighting and then when you try them the highlighting is much more subtle

[Heather Macbeth]

Mario Carneiro said:

I'm pretty sure that's caused by an out of date semantic highlighting cache

for whatever reason the re-elaboration job got delayed or lost and the server never sent an update saying that it shouldn't be blue anymore

Back to the original question, is there any hope of making this server interaction more robust? It seems like it would be very hard to debug.

[Mario Carneiro]

it needs a repro

[Mario Carneiro]

Apparently you have to semantic highlighting is opt in by custom themes, so you have to set

  "editor.semanticTokenColorCustomizations": { "enabled": true },

in your settings.json to turn it on if the theme doesn't turn it on themselves

[Mario Carneiro]

Atom One Light looks pretty good, the variables are bright red which should help

[Heather Macbeth]

This one looks pretty good, tagline "VS Code's default theme, but just a little bit better."

[Matej Penciak]

For a little bit of shameless self promotion: While I was getting over a bad cold, I actually made my own VSCode theme that matched my terminal theme:
image.png
In the process I discovered that there were a few semantic tokens the Lean LSP provides that weren't differentiated by the VS Code Dark+ theme, and adjusted them. Unfortunately it's a dark mode theme only :(

It works best with Lean 4 because that's what I use the most, but it also works with Lean 3 as well.
It also supports Python, Rust, C/C++, JS/TS, Haskell, JSON, YAML, TOML, CSS, HTML, LaTeX (probably others I forgot) with varying degrees of polish, but it's really easy to fix when I notice anything that doesn't look quite right.

Bonus: I also added an icon theme for .lean files and lean-toolchain with little copies of @Arthur Paulino's Lean logo from this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Is.20lean's.20logo.20here.3F/near/268144940 (also a little lake emoji for the lakefile)

image.png

[Arthur Paulino]

How can I get it? :eyes:

[Matej Penciak]

Arthur Paulino said:

How can I get it? :eyes:

I made the repo public: https://github.com/mpenciak/afterglow

All you have to do is run code --install-extension afterglow-0.0.1.vsix in the folder

Alternatively, if you don't feel comfortable installing a random package found online then you can build it from source by running vsce package in the folder (You'll need to install vsce from npm npm install -g @vscode/vsce) and then install the resulting .vsix file