Zulip Chat Archive

Stream: general

Topic: Documentation style change proposal discussion thread

Gabriel Ebner (Aug 02 2020 at 17:42):

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 (Aug 02 2020 at 18:01):

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 (Aug 02 2020 at 18:03):

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 (Aug 02 2020 at 18:40):

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

Gabriel Ebner (Aug 02 2020 at 18:42):

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

Gabriel Ebner (Aug 02 2020 at 18:43):

@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 (Aug 02 2020 at 18:45):

Awesome, you added syntax highlighting!

Gabriel Ebner (Aug 02 2020 at 18:47):

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

Rob Lewis (Aug 02 2020 at 18:58):

Wow, so beautiful!

Rob Lewis (Aug 02 2020 at 19:01):

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 (Aug 02 2020 at 19:01):

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 (Aug 02 2020 at 19:04):

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

Gabriel Ebner (Aug 02 2020 at 19:04):

Do you have a link to Patrick's version?

Rob Lewis (Aug 02 2020 at 19:08):


Gabriel Ebner (Aug 02 2020 at 19:12):

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

Anatole Dedecker (Aug 02 2020 at 19:15):

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 (Aug 02 2020 at 19:20):

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 (Aug 02 2020 at 19:22):

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 (Aug 02 2020 at 20:25):

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

Gabriel Ebner (Aug 03 2020 at 18:10):

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 (Aug 03 2020 at 19:11):

Is the freeze because of suggestions ?

Gabriel Ebner (Aug 03 2020 at 19:23):

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 (Aug 04 2020 at 14:32):

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


Gabriel Ebner (Aug 04 2020 at 14:36):

Oops, the shuffling was not intentional.

Utensil Song (Aug 08 2020 at 10:23):

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 (Aug 08 2020 at 11:20):

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")

Last updated: Aug 03 2023 at 10:10 UTC