Zulip Chat Archive

Stream: lean4

Topic: VS Code syntax highlighting


Heather Macbeth (Dec 08 2022 at 17:36):

@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 (Dec 08 2022 at 17:48):

I can confirm that this is also happening for me:

image.png

(#7B9246 is the usual Green for comments)

Matej Penciak (Dec 08 2022 at 17:54):

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

image.png

Kevin Buzzard (Dec 08 2022 at 19:30):

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

Mario Carneiro (Dec 08 2022 at 21:12):

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

Mario Carneiro (Dec 08 2022 at 21:15):

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 (Dec 08 2022 at 21:17):

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 (Dec 08 2022 at 21:17):

even in normal operation this persists for a few seconds

Heather Macbeth (Dec 08 2022 at 21:37):

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 (Dec 08 2022 at 21:39):

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

Mario Carneiro (Dec 08 2022 at 21:42):

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 (Dec 08 2022 at 21:55):

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 (Dec 08 2022 at 21:56):

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

Mario Carneiro (Dec 08 2022 at 21:57):

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

Mario Carneiro (Dec 08 2022 at 21:58):

the dark themes have much clearer coloration it seems

Heather Macbeth (Dec 08 2022 at 21:59):

Thanks!

Heather Macbeth (Dec 08 2022 at 22:00):

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 (Dec 08 2022 at 22:01):

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 (Dec 08 2022 at 22:04):

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 (Dec 08 2022 at 22:14):

it needs a repro

Mario Carneiro (Dec 08 2022 at 22:16):

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 (Dec 08 2022 at 22:16):

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

Heather Macbeth (Dec 08 2022 at 22:38):

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

Matej Penciak (Dec 09 2022 at 03:01):

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 (Dec 09 2022 at 03:21):

How can I get it? :eyes:

Matej Penciak (Dec 11 2022 at 02:38):

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


Last updated: Dec 20 2023 at 11:08 UTC