can't read "popup boxes" sometimes

Stream: lean4

[Kevin Buzzard]

I'm sorry, I don't know the proper name for these things. If I hover over something in the infoview then there's a transient pop-up displaying helpful information. Sometimes the pop-up goes up above the "top" of the window and I can't read the relevant bit. This has been a problem for me for ages and I'm slightly surprised it hasn't come up before (or maybe I missed it, or failed to notice it was talking about the same question). Example: right now I'm trying to deal with an error in an auto-ported mathlib file and I want to see the precise type of Sum.rec so I hover over it and it's at the top of the pop-up which seems to be above the top of the window and I don't know how to see it.

sum.rec.png

What's the trick?

[Mario Carneiro]

I imagine triple-click and paste in a new file will work to show the hidden text as a workaround

[Kevin Buzzard]

woo there is triple-click?

[Kevin Buzzard]

Oh this is just "select all"?

[Mario Carneiro]

yeah it works in most browsers

[Mario Carneiro]

select current <div> I think? Not sure exactly what the algorithm is

[Kevin Buzzard]

it doesn't select all for me, it just selects the line in the pop-up.

[Mario Carneiro]

ctrl-A should actually "select all", which will include the popup in addition to a bunch of other stuff

[Kevin Buzzard]

and I can't long-hold and select all because the pop-up won't scroll upwards.

[Kevin Buzzard]

ctrl-A is horrible because it selects all the infoview which is right now displaying a horribly gone-wrong proof

[Mario Carneiro]

hopefully if you scroll around in the paste result you can find your popup

[Kevin Buzzard]

Yeah but this does work -- the information I want is at the bottom of a large text file now. Thanks for the workaround.

[Gabriel Ebner]

@Kevin Buzzard can you tell me how to reproduce this huge popup? We've been wanting to add scrolling to the popup for ages, but it would be great to make sure scrolling would fix your issue.

[Kevin Buzzard]

I take back my claim that ctrl-A and pasting into a text file works: even though the pop-up gets highlighted it does not get pasted.

Gabriel, one way to reproduce it is to design Lean 4 so that @[simp] on a definition makes the definition unfold whenever you apply simp to a term mentioning the definition (as opposed to in Lean 3 when it just marked the equation lemmas with @[simp]). Is this intentional? Should I open an issue about this? We've just been working around it in the port but it occurs to me now that perhaps this was not intentional and is actually a regression (I just wrote four equation lemmas which weren't present in mathlib3 and tagged them simp because of this issue)

I tend to have my font size quite big because I'm in my 50s. I would imagine that just pressing ctrl-+ a few times and then hovering over any pop-up will demonstrate the issue. In fact sometimes I've been able to solve the problem by pressing ctrl-(minus sign) and hoping that the pop-up decides to appear under the cursor instead of over it (or vice-versa).

[Kevin Buzzard]

First attempt ended in failure:

def N : Nat := 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1

/-
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
-/

[Kevin Buzzard]

This works:

def N : Nat := Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $ Nat.succ $
  37

example : N ≠ N := by
  unfold N
  /-
  ⊢ Nat.succ
    (Nat.succ
    ...

  Put cursor on first `Nat.succ` in infoview
  -/
  sorry

[Gabriel Ebner]

https://github.com/leanprover/lean4/issues/2052

[Gabriel Ebner]

https://github.com/leanprover/vscode-lean4/issues/210

[Gabriel Ebner]

https://github.com/leanprover/vscode-lean4/issues/280

[Gabriel Ebner]

https://github.com/leanprover/vscode-lean4/issues/281

[Kevin Buzzard]

Oh thanks! I wasn't even looking in the issues for the right repo it seems ;-) (clueless about how all the infrastructure works)

[Wojciech Nawrocki]

Also previously discussed here.

[Eric Wieser]

Gabriel, one way to reproduce it is to design Lean 4 so that @[simp] on a definition makes the definition unfold whenever you apply simp to a term mentioning the definition (as opposed to in Lean 3 when it just marked the equation lemmas with @[simp]). Is this intentional? Should I open an issue about this? We've just been working around it in the port but it occurs to me now that perhaps this was not intentional and is actually a regression (I just wrote four equation lemmas which weren't present in mathlib3 and tagged them simp because of this issue)

This is related to https://github.com/leanprover/lean4/issues/2042, which links a related zulip thread

[Wojciech Nawrocki]

@Kevin Buzzard could you try the new release? Popups should now always fit within the infoview overall, and are limited to a fixed max height of 300px. Note that they may still not show within the active viewport, i.e. you may have to scroll the infoview up/down to see the popup (this is vscode-lean4#281), but this should always be possible. We moved to a different JS library to do this so it may be buggy and testing is appreciated.