VSCode highlighting stopped

Stream: general

[Horatiu Cheval]

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]

This could easily be my fault

[Eric Wieser]

Can you create a mwe?

[Horatiu Cheval]

I'll try to

[Horatiu Cheval]

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]

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

[Horatiu Cheval]

The eqext function seems to be the culprit here

[Eric Wieser]

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

[Eric Wieser]

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]

(deleted)

[Eric Wieser]

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]

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]

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]

Mathlib style is to write it with a space anyway

[Horatiu Cheval]

Right, it's not a big deal

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Gabriel Ebner]

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]

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

[Floris van Doorn]

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]

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

[Eric Wieser]

Which extension version?

[Eric Wieser]

Thanks for the report

[Floris van Doorn]

lean 0.16.34

[Eric Wieser]

I'll look at this again tomorrow.

[Floris van Doorn]

Here is another one where highlighting fails on 0.16.34:

/- @[simps]: -/

def foo := 1

[Yaël Dillies]

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]

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

[Eric Wieser]

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

[Yaël Dillies]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

(preferably one that leverages the semantic highlighting)

[Marc Huisinga]

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]

note that all tactics are highlighted, variables etc.

[Eric Wieser]

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

[Marc Huisinga]

maybe because that's the induction hypothesis

[Eric Wieser]

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]

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]

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]

I guess the sepBy highlighting might be a bug

[Sebastian Ullrich]

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]

One more example with string interpolation:
image.png

[Mario Carneiro]

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

[Sebastian Ullrich]

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

[Eric Wieser]

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]

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]

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

[Mario Carneiro]

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]

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

[Gabriel Ebner]

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]

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]

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]

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

[Eric Wieser]

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]

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]

Well, almost...

[Eric Wieser]

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

image.png

[Eric Wieser]

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]

import algebra.ring.basic

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

highlights in unexpected ways:
image.png

[Eric Wieser]

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]

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]

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

[Marc Huisinga]

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]

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

[Marc Huisinga]

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

[Gabriel Ebner]

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]

TextMate grammars are spooky

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Eric Wieser]

That was part of the binder highlighting

[Eric Wieser]

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

[Eric Wieser]

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

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

(from the discord, posted in May)

[Bhavik Mehta]

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

[Eric Wieser]

The whole feature or just blue λ?

[Bhavik Mehta]

Blue λ

[Bhavik Mehta]

Essentially just how it was before the binders change