Zulip Chat Archive

Stream: general

Topic: widget rendering bug

Scott Morrison (Sep 24 2020 at 06:36):

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 (Sep 24 2020 at 07:16):

Oof. I'll have a look

Edward Ayers (Sep 24 2020 at 07:19):

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

Edward Ayers (Sep 24 2020 at 07:22):

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

Edward Ayers (Sep 24 2020 at 07:23):

I've seen this failure mode before though

Kenny Lau (Sep 24 2020 at 07:23):

I've seen this bug too

Edward Ayers (Sep 24 2020 at 07:25):

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 (Sep 24 2020 at 07:25):

Maybe it only happens for certain fonts

Edward Ayers (Sep 24 2020 at 07:25):

What fonts are you guys using?

Edward Ayers (Sep 24 2020 at 07:43):

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 (Sep 24 2020 at 08:03):

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

Last updated: Dec 20 2023 at 11:08 UTC