Zulip Chat Archive

Stream: general

Topic: Website navigation bar


view this post on Zulip Gabriel Ebner (Oct 01 2020 at 16:28):

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?

view this post on Zulip Rob Lewis (Oct 01 2020 at 16:48):

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

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 17:43):

This would make my life a lot easier

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 17:43):

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

view this post on Zulip Eric Wieser (Oct 01 2020 at 17:48):

Looks a bit wacky on mobile:

image.png

view this post on Zulip Eric Wieser (Oct 01 2020 at 17:49):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 17:57):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 17:58):

Dropdowns are not an option on desktop, though.

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 17:58):

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

view this post on Zulip Eric Wieser (Oct 01 2020 at 18:06):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:09):

I just updated it

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:16):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:18):

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?

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:18):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:18):

No it should be exactly the same.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:19):

Hmm, let me check again.

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:19):

Maybe the font sizes are different.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:21):

Site with css tweaks: image.png

Docs: image.png

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:23):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:24):

Yes, of course

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:25):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:26):

Resetting to dd6577c : image.png

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:27):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:29):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:30):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:30):

Ok, merged.

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:31):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:31):

Let's see how this looks like when uploaded.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:33):

It's uploaded

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:34):

works_for_me.png

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:34):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:35):

image.png

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:36):

What do others see?

view this post on Zulip Bryan Gin-ge Chen (Oct 01 2020 at 18:40):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:43):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 18:55):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:59):

It works! (demo updated)

view this post on Zulip Patrick Massot (Oct 01 2020 at 19:02):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 19:21):

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.

view this post on Zulip Adam Topaz (Oct 01 2020 at 19:29):

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!

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 19:56):

I just type mathlib into my browser search bar

view this post on Zulip Rob Lewis (Oct 02 2020 at 14:32):

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

view this post on Zulip Rob Lewis (Oct 02 2020 at 14:32):

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

view this post on Zulip Rob Lewis (Oct 02 2020 at 14:33):

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

view this post on Zulip Johan Commelin (Oct 02 2020 at 14:34):

layout looks good.

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

view this post on Zulip Patrick Massot (Oct 02 2020 at 14:51):

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.

view this post on Zulip Eric Wieser (Oct 02 2020 at 14:52):

Agreed that the sidebar indent is weird

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 15:13):

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

view this post on Zulip Patrick Massot (Oct 02 2020 at 15:18):

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

view this post on Zulip Eric Wieser (Oct 02 2020 at 15:20):

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

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 15:55):

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.

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 15:56):

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

view this post on Zulip Rob Lewis (Oct 02 2020 at 16:00):

Lovely :)

view this post on Zulip Rob Lewis (Oct 02 2020 at 16:11):

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.

view this post on Zulip Rob Lewis (Oct 02 2020 at 16:12):

Is it possible to force them both to the bottom?

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 16:41):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2020 at 16:45):

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

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 16:56):

Added indentation.

view this post on Zulip Rob Lewis (Oct 02 2020 at 17:22):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2020 at 18:30):

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.

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 19:08):

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:

view this post on Zulip Rob Lewis (Oct 03 2020 at 11:49):

This is live now!


Last updated: May 13 2021 at 16:25 UTC