Zulip Chat Archive

Stream: general

Topic: Mathlib docs le vs lt


view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:26):

I use often mathlib docs and found really difficult to read le vs lt theorems, due to the fact they're most of the time links themselves, so they get underlined and it can get confusing with the "underline" of le ≤

Would it be interesting I do a PR to the CSS of doc-gen so we can get rid of this? Or is there a better alternative?

view this post on Zulip Johan Commelin (Mar 23 2020 at 19:27):

Hmm, yeah, that sounds like it's worth a PR

view this post on Zulip Johan Commelin (Mar 23 2020 at 19:27):

Maybe only underline on hover...

view this post on Zulip Alex J. Best (Mar 23 2020 at 19:30):

Or a lighter underline colour?

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:32):

Guess it depends, those links are not even redirecting to some page, they're only anchor so we can refer to the location of something. But, we can also just use theorem as anchors and not part of the theorem as anchors, right?

view this post on Zulip Johan Commelin (Mar 23 2020 at 19:35):

Yeah, makes sense.

view this post on Zulip Johan Commelin (Mar 23 2020 at 19:36):

But @Rob Lewis is the boss of the docs pages (-;

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:40):

I've done it locally using Stylish and local CSS for me. Here's it looks like. DeepinScreenshot_select-area_20200323204032.png

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:42):

It's hacky and dirty but can be reproduced with those rules injected in the stylesheet:

.decl_type a:link, .structure_field a:link {
    text-decoration: none !important;
}

.decl_type a:hover, .structure_field a:hover {
    text-decoration: underline !important;
}

view this post on Zulip Patrick Massot (Mar 23 2020 at 19:46):

I always said there are too many underlines in this CSS. Basically every word is underlined, this is clearly pointless.

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 19:50):

Patrick Massot said:

I always said there are too many underlines in this CSS. Basically every word is underlined, this is clearly pointless.

Definitely, the only underline which "makes sense" to me is when we underline theorem or lemmas names so we can refer to them easily and pass a link. Otherwise, it's killing my eyes each time I try to find out if this is a ≤ or < especially in structure fields.

view this post on Zulip Rob Lewis (Mar 23 2020 at 21:50):

Ryan Lahfa said:

Guess it depends, those links are not even redirecting to some page, they're only anchor so we can refer to the location of something. But, we can also just use theorem as anchors and not part of the theorem as anchors, right?

I'm not sure I follow. Clicking on < should direct you to the entry for has_lt.lt. In general, clicking on any name (or notation) that appears in a type should direct you to the entry for that name. I don't like removing the underlines entirely, since then it's not clear that things are clickable at all.

view this post on Zulip Rob Lewis (Mar 23 2020 at 21:51):

That said, I see that < and are hard to distinguish.

view this post on Zulip Rob Lewis (Mar 23 2020 at 21:51):

Maybe changing the color or weight of the underline would help.

view this post on Zulip Patrick Massot (Mar 23 2020 at 21:59):

I think we can clearly explain once and for all that everything is clickable.

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 22:02):

Patrick Massot said:

I think we can clearly explain once and for all that everything is clickable.

I agree with this solution rather, when I hover on it, I can see it being underlined and I understand I can click it.
But I spend too much time trying to distinguish between < and ≤ in theorems involving those two at multiple places…

view this post on Zulip Ryan Lahfa (Mar 23 2020 at 22:05):

Rob Lewis said:

Ryan Lahfa said:

Guess it depends, those links are not even redirecting to some page, they're only anchor so we can refer to the location of something. But, we can also just use theorem as anchors and not part of the theorem as anchors, right?

I'm not sure I follow. Clicking on < should direct you to the entry for has_lt.lt. In general, clicking on any name (or notation) that appears in a type should direct you to the entry for that name. I don't like removing the underlines entirely, since then it's not clear that things are clickable at all.

Indeed, I misunderstood something.

The code I provided make them appear on hover, but even if we change the color, it's going to be the same thing, it'll pollute the visual overview of a theorem :/.

I think it'd be better to adopt another way, but it cannot be at foreground, it must be at background so it does not collision with mathematical symbols, e.g. = becomes \equiv visually with underlines.


Last updated: May 08 2021 at 20:11 UTC