Zulip Chat Archive

Stream: general

Topic: VSCode highlighting stopped


Horatiu Cheval (May 29 2021 at 06:31):

Suddenly, VSCode highlights selectively only some of the keywords. Restarting doesn't work, and it happens only in this project.
highlight-broken.png
Has anyone seen this or knows how could I fix it?

Eric Wieser (May 29 2021 at 06:34):

This could easily be my fault

Eric Wieser (May 29 2021 at 06:34):

Can you create a mwe?

Horatiu Cheval (May 29 2021 at 06:36):

I'll try to

Horatiu Cheval (May 29 2021 at 07:05):

Ok, so I managed to reduce to this file:

inductive type
| zero : type
| arrow : type  type  type

namespace type

  infixl `↣` : 50 := arrow

  @[simp]
  def interpret : type  Type
  | zero := 
  | (σ  τ) := σ.interpret  τ.interpret

  notation `∥` σ `∥` := σ.interpret

end type

inductive formula
| prime (p : Prop) [decidable p] : formula
| universal {σ : type} : (σ  formula)  formula

namespace formula

  notation `∀∀` binders `;` r:(scoped A, universal A) := r

  -- removing `eqext` fixes the highlighting following it
  def eqext : Π {σ : type}, σ  σ  formula
  | type.zero x y := prime $ x = y
  | (σ  τ) x y := ∀∀ (z : σ) ; (eqext (x z) (y z))

  def def_no_highlight : formula  Prop := sorry

  section section_no_highlight

  end section_no_highlight

end formula

Horatiu Cheval (May 29 2021 at 07:06):

Which on my computer looks like this:
highlight-broken-mwe.png

Horatiu Cheval (May 29 2021 at 07:07):

The eqext function seems to be the culprit here

Eric Wieser (May 29 2021 at 07:37):

Ah, the highlighting is being confused by \forall\forall, and looking for a trailing comma

Eric Wieser (May 29 2021 at 07:40):

Which would be fixable by changing the highlighter to only recognize forall if followed by a space (even though the space is not strictly required)

Eric Wieser (May 29 2021 at 07:40):

(deleted)

Eric Wieser (May 29 2021 at 07:42):

Is this a deal breaker for the new highlighter? Essentially, by using heuristics for better highlighting, there will always be user-defined syntax that will make those heuristics misfire.

Horatiu Cheval (May 29 2021 at 07:59):

Thank you for looking into it. For one, I am happy to workaround this by replacing the semicolon with a comma in this notation. (off-topic: which seems to work better anyway. ∀∀ z : ∥σ∥ , (eqext (x z) (y z)) works but
∀∀ (z : ∥σ∥) ; (eqext (x z) (y z)) needs those parentheses around the typing statement in order to parse, if someone is willing to shed some light on this behaviour)

Horatiu Cheval (May 29 2021 at 08:01):

I'm probably not the right person at all to discuss these design decisions, but wouldn't it be weird if \forall followed immediately by a ( or a { wouldn't be recognized?

Eric Wieser (May 29 2021 at 08:02):

Mathlib style is to write it with a space anyway

Horatiu Cheval (May 29 2021 at 08:05):

Right, it's not a big deal

Bhavik Mehta (May 29 2021 at 18:17):

Another example (distinct from Horatiu's and the other one I've mentioned) happens in data/list/defs from line 386 down, I think the issue is section forall₂

Eric Wieser (May 29 2021 at 19:28):

\b is evidently meaningless in regexes when this much unicode is used

Bhavik Mehta (May 30 2021 at 18:04):

Is this intended to be fixed? Or do we have to live with the fact that mathlib lists don't highlight correctly

Eric Wieser (May 30 2021 at 18:10):

Forall2 should be another easy fix, but not from mobile, which is all I have available till Tuesday

Eric Wieser (Jun 01 2021 at 11:28):

Fixed in https://github.com/leanprover/vscode-lean/pull/272

Eric Wieser (Jun 01 2021 at 12:32):

It's a shame github just updated linguist with the previous version

Eric Wieser (Jun 01 2021 at 18:12):

Nothing is ever easy - github interprets the syntax file in a different way to how vscode does...

Gabriel Ebner (Jun 01 2021 at 18:14):

There's also the growing issue of support for Lean 4 in the github syntax highlighting: https://github.com/leanprover/lean4/issues/377

Eric Wieser (Jun 01 2021 at 21:18):

Github linguist lets you override syntax in .gitattributes - so I don't think we need to support a polyglot grammar.

Floris van Doorn (Jun 01 2021 at 22:46):

I noticed a couple other places where highlighting stopped:
core.init.meta.simp_tactic
image.png

core.init.meta.smt.rsimp
image.png

Floris van Doorn (Jun 01 2021 at 22:49):

Also meta def is not highlighted for most of core.init.meta.tactic.

Eric Wieser (Jun 01 2021 at 22:52):

Which extension version?

Eric Wieser (Jun 01 2021 at 22:52):

Thanks for the report

Floris van Doorn (Jun 01 2021 at 22:55):

lean 0.16.34

Eric Wieser (Jun 01 2021 at 23:01):

I'll look at this again tomorrow.

Floris van Doorn (Jun 02 2021 at 01:53):

Here is another one where highlighting fails on 0.16.34:

/- @[simps]: -/

def foo := 1

Yaël Dillies (Jun 02 2021 at 05:25):

Another bug I just found. It doesn't detect the dot at the end of lines (order/bounded_lattice):

@[simp] theorem top_ne_coe {a : α} :   (a : with_top α) .
@[simp] theorem coe_ne_top {a : α} : (a : with_top α)   .

@[priority 10]
instance has_lt [has_lt α] : has_lt (with_top α) :=
{ lt := λ o₁ o₂ : option α,  b  o₁,  a  o₂, b < a }

yet another bug

Eric Wieser (Jun 02 2021 at 06:30):

I think the @[simps] one has always been broken

Eric Wieser (Jun 02 2021 at 06:48):

The other bug is the `name parser not knowing when to stop and eating the )

Yaël Dillies (Jun 02 2021 at 07:48):

At that point, is it worth spending too much time on fixing all of that? You said that the lean4 highlighting uses directly Lean's parsing, right?

Eric Wieser (Jun 02 2021 at 07:59):

Fixes were easy: https://github.com/leanprover/vscode-lean/pull/273

Eric Wieser (Jun 02 2021 at 08:00):

I have no idea what lean4 highlighting looks like, I don't have it installed

Eric Wieser (Jun 02 2021 at 08:06):

I've left the simps one alone as it's a problem with the markdown parser, and I don't want to open that can of worms too

Marc Huisinga (Jun 02 2021 at 09:00):

Yaël Dillies said:

At that point, is it worth spending too much time on fixing all of that? You said that the lean4 highlighting uses directly Lean's parsing, right?

Lean 4 uses both the VSCode syntax highlighting and semantic highlighting (which happens on the server side). The downside of semantic highlighting is that the code needs to be elaborated to display the highlighting, so it's always good to have something like the VSCode highlighting as a backup.

Eric Wieser (Jun 02 2021 at 09:08):

@Marc Huisinga, can you paste a screenshot of what the highlighting looks like for a typical lean4 definition?

Eric Wieser (Jun 02 2021 at 09:08):

(preferably one that leverages the semantic highlighting)

Marc Huisinga (Jun 02 2021 at 09:09):

Eric Wieser said:

Marc Huisinga, can you paste a screenshot of what the highlighting looks like for a typical lean4 definition?

Stolen from the Lean 4 course at KIT:
image.png

Marc Huisinga (Jun 02 2021 at 09:09):

note that all tactics are highlighted, variables etc.

Eric Wieser (Jun 02 2021 at 09:11):

Odd that count_erase is highlighted but not the other lemmas in simp

Marc Huisinga (Jun 02 2021 at 09:12):

maybe because that's the induction hypothesis

Eric Wieser (Jun 02 2021 at 09:12):

But at any rate, the fact that {as : ...} in the argument is in a pale blue is consistent with the new lean3 vscode syntax, which is nice

Sebastian Ullrich (Jun 02 2021 at 09:15):

Eric Wieser said:

Odd that count_erase is highlighted but not the other lemmas in simp

It's telling you "why are you using recursion in a tactic proof"

Marc Huisinga (Jun 02 2021 at 09:15):

Here's an example from a macro declaration where the keywords in the macro are highlighted in the macro_rules command:
image.png

Marc Huisinga (Jun 02 2021 at 09:15):

I guess the sepBy highlighting might be a bug

Sebastian Ullrich (Jun 02 2021 at 09:17):

Well, that is the token :) . Not sure if we should add some heuristics to terminate highlighting before the (, or add some annotation in the parser for that.

Marc Huisinga (Jun 02 2021 at 09:22):

One more example with string interpolation:
image.png

Mario Carneiro (Jun 02 2021 at 09:37):

is it possible to revert the coloring of regular text inside the interpolation? like that <- shouldn't be brown

Sebastian Ullrich (Jun 02 2021 at 09:40):

I don't think LSP has an appropriate token kind for that. But it lets us invent our own.

Eric Wieser (Jun 02 2021 at 11:09):

Floris van Doorn said:

Here is another one where highlighting fails on 0.16.34:

/- @[simps]: -/

def foo := 1

Filed as https://github.com/leanprover/vscode-lean/issues/274, this has probably been around as long as we've highlighted markdown comments.

Gabriel Ebner (Jun 02 2021 at 16:27):

Mario Carneiro said:

is it possible to revert the coloring of regular text inside the interpolation? like that <- shouldn't be brown

The vim syntax highlighting does that for all strings by default, and I believe we could do that in vscode as well. It works mostly fine, except for syntax "{" term "}" : term, where " term " is highlighted as a string. There was some talk of enabling interpolation by default for all strings, then we'd just need to write "\{" instead.

Mario Carneiro (Jun 02 2021 at 16:29):

wait, why isn't that interpreted as an interpolated string by lean? Is it because syntax is magic?

Mario Carneiro (Jun 02 2021 at 16:30):

It would be nice if we could escape braces today, even if it's not necessary. It might help with these things

Yaël Dillies (Jun 21 2021 at 14:06):

In data.list.rotate, probably because of exists
image.png

Gabriel Ebner (Jun 21 2021 at 14:42):

Honestly, I'm beginning to feel that highlighting the argument names brought more issues than it's worth because the failure mode is so extreme. (Looking though the screenshot, the λ ⟨n, hn⟩, ... is also highlighted incorrectly.)

Kevin Buzzard (Jun 21 2021 at 14:44):

I agree with Gabriel. I never noticed any issues with highlighting for years, because I wasn't observant enough to spot any of the subtleties which people would occasionally spot, but now I'm noticing issues all the time which are really easy to spot, like the above.

Yaël Dillies (Jun 21 2021 at 15:07):

There was a really long and obvious in subgroup, and it didn't have anything to do with the new highlighting, but yeah I agree that this seems to have introduced lots.

Eric Wieser (Jun 21 2021 at 15:48):

The change that fixed subgroup was independent of the change that introduced the binder names

Eric Wieser (Jun 21 2021 at 15:52):

I'll put together a patch to fix the above two bugs, even if we do eventually decide to revert the feature entirely

Eric Wieser (Jun 21 2021 at 16:09):

Yaël Dillies said:

In data.list.rotate, probably because of exists
image.png

Fixed in https://github.com/leanprover/vscode-lean/pull/276

Eric Wieser (Jun 21 2021 at 16:13):

Well, almost...

Eric Wieser (Jun 21 2021 at 16:24):

Ok, fixed properly and updated with a fix for λ ⟨n, hn⟩, ... too:

image.png

Eric Wieser (Jun 21 2021 at 16:30):

Highlighting the contents of the⟨⟩ as a parameter is the wrong thing to do anyway, as you can have all sorts of weird things in there:

#check (λ .((1, unit.star).snd), (y, (z : ))⟩, 1 : unit ×  ×   )

Bhavik Mehta (Jun 25 2021 at 03:52):

import algebra.ring.basic

example {R : Type*} [ring (R : Type*)] : false :=
sorry

highlights in unexpected ways:
image.png

Eric Wieser (Jun 25 2021 at 17:22):

I'm not so worried about the parameter highlighting occasionally being suboptimal - it's the cases where it breaks things that worked before I added it that I'm most worried about. Thanks for the report anyway, I'll have a go at fixing that one once the other PR is merged.

Floris van Doorn (Jun 29 2021 at 14:38):

I don't know if this one is already reported:
listΠ
https://github.com/leanprover-community/mathlib/blob/master/src/tactic/rcases.lean#L426
image.png

Gabriel Ebner (Jun 29 2021 at 15:05):

It pains me a bit given how much work went into it, but I've now removed the binder highlighting completely.

Marc Huisinga (Jun 29 2021 at 15:09):

Removing it from vscode-lean4 might also be the right call. I had originally removed it in the first iteration of the syntax highlighting for the same reasons (and the fact that Lean 4 was expected to have semantic highlighting).

Gabriel Ebner (Jun 29 2021 at 15:11):

I don't think we ever had it in vscode-lean4 (or at least I can't find it right now).

Marc Huisinga (Jun 29 2021 at 15:11):

You're right, I was thinking of definition name highlighting! Sorry.

Gabriel Ebner (Jun 29 2021 at 15:14):

Definition name highlighting is much less tricky, since it can't go on forever (at some point there's going to be whitespace). Highlighting binder names can go wrong much more easily, since you need to keep track of nested parentheses, etc. (And god forbid somebody declares noooo( as a prefix notation.)

Marc Huisinga (Jun 29 2021 at 15:23):

TextMate grammars are spooky

Eric Wieser (Jun 29 2021 at 15:26):

Right, the binder hightlighting never had a chance if faced with nooo(. listΠ would be straighforward to add another fix for.

Eric Wieser (Jun 29 2021 at 15:27):

Ah, actually listΠ would be impossible to handle, since it's notation defined as local notation `listΠ` := list_Pi

Eric Wieser (Jun 29 2021 at 15:27):

And there's no way for the textmate grammar to know when someone has stolen its binder syntax to use for something else - this is exactly like the nooo( case, and would require heuristics based on what someone would "reasonably want to do"

Bhavik Mehta (Jun 29 2021 at 20:23):

It looks like highlighting for lambdas has gone too - is it my imagination or was that there before the binder highlighting?

Eric Wieser (Jun 29 2021 at 20:53):

That was part of the binder highlighting

Eric Wieser (Jun 29 2021 at 21:19):

Maybe we can ship a second "Lean (with binders)" syntax file and let users choose between them?

Eric Wieser (Jun 29 2021 at 21:20):

Even though lean 4 has semantic highlighting, it won't work on github where a (modified) TextMate engine is used

Bhavik Mehta (Jun 29 2021 at 22:51):

Eric Wieser said:

That was part of the binder highlighting

Hmm I'm fairly sure that in examples like
image.png
the λ was highlighted before the binders change...

Bhavik Mehta (Jun 29 2021 at 22:57):

I went looking for some old screenshots to double check: image.png

Bhavik Mehta (Jun 29 2021 at 22:57):

(from the discord, posted in May)

Bhavik Mehta (Jul 03 2021 at 16:50):

Could we have this feature back? It would be a shame for this to disappear in favour of seemingly nothing

Eric Wieser (Jul 03 2021 at 17:06):

The whole feature or just blue λ?

Bhavik Mehta (Jul 03 2021 at 18:57):

Blue λ

Bhavik Mehta (Jul 03 2021 at 18:57):

Essentially just how it was before the binders change


Last updated: Dec 20 2023 at 11:08 UTC