Zulip Chat Archive

Stream: general

Topic: widget rendering bug


view this post on Zulip 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).

view this post on Zulip Edward Ayers (Sep 24 2020 at 07:16):

Oof. I'll have a look

view this post on Zulip Edward Ayers (Sep 24 2020 at 07:19):

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

view this post on Zulip Edward Ayers (Sep 24 2020 at 07:22):

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

view this post on Zulip Edward Ayers (Sep 24 2020 at 07:23):

I've seen this failure mode before though

view this post on Zulip Kenny Lau (Sep 24 2020 at 07:23):

I've seen this bug too

view this post on Zulip 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

view this post on Zulip Edward Ayers (Sep 24 2020 at 07:25):

Maybe it only happens for certain fonts

view this post on Zulip Edward Ayers (Sep 24 2020 at 07:25):

What fonts are you guys using?

view this post on Zulip 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.

view this post on Zulip 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: May 09 2021 at 18:17 UTC