Website navigation bar

Stream: general

[Gabriel Ebner]

I found it very hard to find certain pages on the website, such as the style guidelines, the theorem lists, or really anything that doesn't have a prominent link on the first page. If I didn't know that we had these pages, I would never find them.
Therefore I'm proposing to add a navigation bar to the website: leanprover-community/leanprover-community.github.io#138
Opinions?

[Rob Lewis]

http://robertylewis.com/mathlib/ if you want to try it out

[Kevin Buzzard]

This would make my life a lot easier

[Kevin Buzzard]

I almost always go to the website now knowing exactly what I want but not always how to get there.

[Eric Wieser]

Looks a bit wacky on mobile:

image.png

[Eric Wieser]

IMO even just updating the existing dropdowns to contain the new information would be a big improvement, and bootstrap will keep doing something sensible with that on mobile

[Gabriel Ebner]

Do you object to the wonderful flexbox layout of the navigation? :smile:

[Gabriel Ebner]

Dropdowns are not an option on desktop, though.

[Gabriel Ebner]

Would you prefer a top-down list on mobile instead of the flexbox?

[Eric Wieser]

I think the hosted version is behind the PR, so it may not look as bad on mobile as I thought

[Rob Lewis]

I just updated it

[Gabriel Ebner]

Should I merge the CSS tweaks into the branch so that people can test them?

[Rob Lewis]

Oh, I forgot to leave a comment there. The new header font isn't the same as the one in the docs pages, is it? Sans serif vs serif?

[Rob Lewis]

Not that it's worse, just that we should make them the same. Maybe we should change the docs.

[Gabriel Ebner]

No it should be exactly the same.

[Rob Lewis]

Hmm, let me check again.

[Gabriel Ebner]

Maybe the font sizes are different.

[Rob Lewis]

Site with css tweaks: image.png

Docs: image.png

[Gabriel Ebner]

That's not how it should look like. Did you run make_site.py again?

[Rob Lewis]

Yes, of course

[Rob Lewis]

Hmm, the "set bootstrap variables" commit seems to have changed the font

[Rob Lewis]

Resetting to dd6577c : image.png

[Gabriel Ebner]

Resolution is a bit low, but that's how it should look like.

[Rob Lewis]

In any case, let's merge the CSS tweaks into the other branch and upload a demo, see if others see what I see

[Rob Lewis]

It's not a Chrome thing, I see the same fonts in Firefox

[Gabriel Ebner]

Ok, merged.

[Gabriel Ebner]

Oh wait, the new one just has the correct serif/sans-serif choice. But the fonts are still wrong? This is weird.

[Gabriel Ebner]

Let's see how this looks like when uploaded.

[Rob Lewis]

It's uploaded

[Gabriel Ebner]

works_for_me.png

[Rob Lewis]

http://robertylewis.com/mathlib/ built with 2fd553539d3001d079c45a866bbd3eb14920984e

[Rob Lewis]

image.png

[Rob Lewis]

What do others see?

[Bryan Gin-ge Chen]

Firefox on macOS:
Screen-Shot-2020-10-01-at-2.40.06-PM.png

[Gabriel Ebner]

Oh wait, there's something fishy going on. I have Merriweather installed locally, so I didn't notice this. Wait a minute.

[Gabriel Ebner]

Fixed. Apparently if you ask google for the wrong font weight, then you get neither the font nor an error. :shrug:

[Rob Lewis]

It works! (demo updated)

[Patrick Massot]

I don't understand why you put all this in a side bar instead of simply adding to the existing menu.

[Gabriel Ebner]

Patrick Massot said:

I don't understand why you put all this in a side bar instead of simply adding to the existing menu.

• The visibility and discoverability is higher than in a dropdown. As I've written above, there are many pages on our wonderful website that I didn't know about. There is enough screen real estate, so let's use it.
• A permanent sidebar is easier to search than a dropdown, both by just skimming over it with your eyes as well as using the browser's search functionality. Maybe this is just me, but I heavily use the search function to navigate web sites.

[Adam Topaz]

Can we put a giant cat/octopus thing somewhere on the front page with a link to mathlib on github? I always have a hard time just finding the link to the github repo!

[Kevin Buzzard]

I just type mathlib into my browser search bar

[Rob Lewis]

I've updated https://robertylewis.com/mathlib/

[Rob Lewis]

In particular, the menu items are shifted around a bunch, and there are now links to Zulip and GitHub at the very top.

[Rob Lewis]

I'm with Gabriel in preferring the nav bar (on non-mobile) to menus, how do others feel?

[Johan Commelin]

layout looks good.

should "leanproject" and "how pieces fit together" move to installation?

[Patrick Massot]

I definitely prefer menus but I won't fight about this. However I very strongly feel the proposal currently doesn't work on mobile. Side note: I also think the indentation of section headings in the side bar is weird.

[Eric Wieser]

Agreed that the sidebar indent is weird

[Gabriel Ebner]

What is wrong with the mobile version? It works nicely here with Firefox on android.

[Patrick Massot]

It displays the pseudo-menu on two columns of very difficult to click items

[Eric Wieser]

For an easier before / after comparison, does it make sense to split into two PRs?

• One that updates the heading structure but doesn't touch the style or dropdowns
• One that does the style changes present here

We can then merge the first one which I don't think anyone would argue is a step back, and compare the second one

[Gabriel Ebner]

Patrick Massot said:

It displays the pseudo-menu on two columns of very difficult to click items

Thanks for pointing this out, clickability is an important objective. I've increased the vertical spacing between the links and added horizontal lines between them so that they're easier to tell apart.

[Gabriel Ebner]

I've also removed the indentation of the category headers in the side bar. This looks better, thanks for the suggestion.

[Rob Lewis]

Lovely :)

[Rob Lewis]

Sorry to keep nitpicking about the grey bar, it really doesn't matter... but now in a window taller than the page, the footer and end of the nav bar are in the middle of the page and there's white space at the end.

[Rob Lewis]

Is it possible to force them both to the bottom?

[Gabriel Ebner]

Oops, this got lost in the refactoring. Put back in.

[Bryan Gin-ge Chen]

Not sure if Rob's test site is fully updated and this has been fixed, but it's a bit hard to tell where one link in the sidebar starts and the next ends. Could we add bullets or some indentation for links that are longer than one line? Screen-Shot-2020-10-02-at-12.43.35-PM.png

[Gabriel Ebner]

Added indentation.

[Rob Lewis]

I'm offline for a while now, but I just uploaded the latest version, which looks perfect to my eye! Thank you for putting up with all the nitpicking, Gabriel :)

[Bryan Gin-ge Chen]

When the window is narrow, the sidebar on https://robertylewis.com/mathlib/100.html gets cut off. It doesn't seem to be happening on any other pages I've looked at yet.

[Gabriel Ebner]

The issue was that I told the browser to shrink the main content as the window gets smaller, but you can't shrink dist_square_eq_dist_square_add_dist_square_sub_two_mul_dist_mul_dist_mul_cos_angle. Luckily this problem only happens with flex-direction: row-reverse and not flex-direction: row. :sweat_smile:

[Rob Lewis]

This is live now!