Documentation style change proposal discussion thread

Stream: general

[Gabriel Ebner]

For some inexplicable reason I forgot about spring cleaning this year. So with a bit of delay, I've finally freshened up the style sheet of the documentation page a bit. https://github.com/leanprover-community/doc-gen/pull/31 Opinions?
Before: https://leanprover-community.github.io/mathlib_docs/tactic/linarith/frontend.html
After: https://gebner.github.io/mathlib_docs/tactic/linarith/frontend.html

[Anatole Dedecker]

Capture-du-2020-08-02-19-56-31.png I'm being picky, but the different padding for directory and files is a little perturbing to me. In this picture, I first thought that add_torsor was in the ring directory, although it isn't. But big thanks anyway the new look is awesome !

[Gabriel Ebner]

My ratio was that the arrow is not part of the label, and that the labels should line up. But I'll change if it confuses too many people.

[Jalex Stark]

I think the issue Anatole brings up is dissolved as soon as you click on any of the arrows?

[Gabriel Ebner]

Another interesting page to look at: https://gebner.github.io/mathlib_docs/tactics.html#abel

[Gabriel Ebner]

@Anatole Dedecker I have changed the nav tree so that the triangles line up with the files. I've reduced the triangle size a bit so that it looks less confusing to me.

[Bryan Gin-ge Chen]

Awesome, you added syntax highlighting!

[Gabriel Ebner]

I only had to install pygments (and add the css).

[Rob Lewis]

Wow, so beautiful!

[Rob Lewis]

The proportions on mobile look slightly more of of whack than the current version. Which isn't that big a problem since the current version doesn't look great. But it's more reason to work on a real mobile version at some point.

[Rob Lewis]

Patrick had a stylesheet at some point that iirc improved things on mobile but looked worse on the desktop. Maybe we can adapt that.

[Gabriel Ebner]

Ah, I think I messed up something there. It looked better at noon.

[Gabriel Ebner]

Do you have a link to Patrick's version?

[Rob Lewis]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/markdown.20module.20docstrings/near/184347341

[Gabriel Ebner]

Ah, I understand what @Patrick Massot did there. That's easy enough to do.

[Anatole Dedecker]

I'm testing what it looks like using Firefox's "Adaptative View", and it seems like there is a problem with long statements, e.g https://gebner.github.io/mathlib_docs/analysis/specific_limits.html#dist_le_of_le_geometric_two_of_tendsto%E2%82%80 On smaller screens, the statement goes out of the box and continues under the lemma list

[Gabriel Ebner]

Ah, so that's what the scroll bars were for... Ok, I'll put them back until we have a better solution for the arguments.

[Anatole Dedecker]

I agree it doesn't really look good, but yeah currently it is needed if we want the site to be at least usable on mobile

[Gabriel Ebner]

Mobile mode shamelessly stolen from Patrick. That's it for tonight.

[Gabriel Ebner]

Dear obsessive mathlib documentation readers,
Some under-the-hood changes to the documentation were merged today. It is quite likely that some things are broken now. Also if your browser freezes for a few seconds when you type in the search box, that's perfectly normal and expected. Feel free to post other complaints to https://github.com/leanprover-community/doc-gen/issues/new
Have a nice week!

[Anatole Dedecker]

Is the freeze because of suggestions ?

[Gabriel Ebner]

Yes, this happens when building the index for the first time. The addAllAsync method is actually supposed to yield to the browser in regular intervals, but something doesn't quite work as expected there.

[Shing Tak Lam]

Is the tactics docs in a random order for anyone else?

image.png

[Gabriel Ebner]

Oops, the shuffling was not intentional.

[Utensil Song]

Is making the tags clickable an idea worth pursuing? (i.e. click at a tag of a tactic, then it will show only tactics in that tag while keeping the current tactic at the same place of the screen)

I wrote a one-liner javascript as a POC:

document.querySelectorAll('.tags li').forEach(item => item.addEventListener('click', (e) => {
  document.querySelector('.tagfilter-div .tagfilter[name="' + e.target.innerText.replace(/ /g, '-') + '"]').click();
} ) );

which makes clicking the tags the same as toggling the corresponding tag filter(but didn't make it to select "only" that tag because I only fiddled with the page and didn't look at the source).

[Utensil Song]

The script works but to fully consider UX, maybe some more work is needed:

• Change the title to "Mathlib tactics: {{tag_name}}" (as a visual hint for that some changes have happened)
• Change the hover cursor to a hand (i.e. pointer)
• Change the hover tip to something like "show only {{tag_name}} tactics"
• ......(Further changes would require some changes to the current UX of "Filter by tag")