VS Code hover issue

Stream: general

[Kevin Buzzard]

example (A C D : Type) (zzz : A → C) (g : C → C → D) (a : A) : D :=
begin
  apply g (zzz a) (zzz a),
end

If I try this in VS Code (on Ubuntu) and hover over the two zzzs in the apply tactic line, the first one doesn't give me a little transient window saying zzz : A \to C but the second one does. Can someone else reproduce? Should I expect the window to pop up for the first zzz as well?

[Reid Barton]

I get the corresponding behavior in emacs too, so I guess it is an issue with Lean itself

[Kenny Lau]

reproduced (Windows, VS Code)

[Kevin Buzzard]

by exact g (zzz a) (zzz a) has the issue, but just giving the term mode proof makes things work again.

[Kenny Lau]

reproduced all three behaviours

[Chris Hughes]

This is actually quite annoying whenever I do a by haveI := _; exact _ proof

[Kevin Buzzard]

So it's the Lean server which ships these little windows out?

[Kenny Lau]

can we have the complicated diagram again?

[Kevin Buzzard]

Line 240 of ring_theory.integral_closure is

  have := fg_mul _ _ (fg_adjoin_singleton_of_integral x hx) (fg_adjoin_singleton_of_integral y hy),

and I'm surprised to note that in VS Code if I hover over the first fg_adjoin_singleton_of_integral then nothing happens, but if I hover over the second one I see the type as expected. Is this a bug?

[Bryan Gin-ge Chen]

This looks more like a problem with Lean rather than with VS Code or the extension. It might be good to collect examples like this in an issue here: https://github.com/leanprover-community/lean/issues

[Kevin Buzzard]

I'll try to minimise before I open an issue.

[Kenny Lau]

@Kevin Buzzard is it intentional that you extended an older thread?

[Kevin Buzzard]

No, it was a coincidence that the older thread had the same name.

[Kenny Lau]

I guess you haven't changed in 1 year and 10 months

[Kevin Buzzard]

In fact I hadn't even noticed that I was extending an older thread of my own until you just pointed it out.

[Sorawee Porncharoenwase]

I have a distantly related issue. VS Code seems to highlight incorrectly in the following case:

Screen-Shot-2020-11-14-at-16.26.38.png

Screen-Shot-2020-11-14-at-16.26.48.png

Is this a Lean issue or VS Code?

[Bryan Gin-ge Chen]

This is probably an issue with the widget. Where did you put your mouse cursor in the two cases?

cc: @Edward Ayers

[Sorawee Porncharoenwase]

\forall and \wedge.

[Edward Ayers]

Yeah this is caused by the linebreaking

[Edward Ayers]

I think that the second screenshot is correct behaviour

[Edward Ayers]

the first screenshot is an issue caused by the way the CSS linebreaking currently works. It's a tricky one to fix because it's caused by some wacky CSS behaviour. :'(