widget rendering bug

Stream: general

[Scott Morrison]

Hi @Edward Ayers, just letting you know about a widget rendering bug:
If you look at the (wildly in progress) opens_le_cover branch, on commit 0c329591c6a20ebd252df92966ba94af88a1129b, line 135 of category_theory.limits.cofinal, the goal displays as

⊢ 𝟭 (cocone (F ⋙ G)  ≅ extend_cocone ⋙ cocones.whiskering F
     )

(the close parenthesis has gone stray).

[Edward Ayers]

Oof. I'll have a look

[Edward Ayers]

Does it change if you make the window bigger and smaller?

[Edward Ayers]

It's rendering ok for me :/ maybe I'm missing something?
image.png
image.png

[Edward Ayers]

I've seen this failure mode before though

[Kenny Lau]

I've seen this bug too

[Edward Ayers]

Whats happening is the (cocone (F ⋙ G)) element is wrapped in an inline-block to get the pretty linebreaking to work, but sometimes the layout maths is off and it linebreaks in this block before the outer one linebreaks

[Edward Ayers]

Maybe it only happens for certain fonts

[Edward Ayers]

What fonts are you guys using?

[Edward Ayers]

Ok I've tried changing the fonts etc and I can't get this theorem to exhibit this bug, so I'll keep programming until I find an example of the bug and then try to diagnose it. Hopefully the bug doesn't arise too frequently to be a massive issue in the mean time.

[Gabriel Ebner]

Another funny rendering bug is that λ (n : ℕ), n > n breaks like this:

λ (n : ℕ)
  , n > n

In the API documentation we solve these issues by post-processing the formatted expression a little bit, i.e. move parenthesis inside: https://github.com/leanprover-community/doc-gen/blob/fe4f42fdda23b690695b40d353e5da6d49cf9d65/src/export_json.lean#L70-L126