## Stream: general

#### 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?

#### Rob Lewis (Oct 01 2020 at 16:48):

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

#### Kevin Buzzard (Oct 01 2020 at 17:43):

This would make my life a lot easier

#### 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.

#### Eric Wieser (Oct 01 2020 at 17:48):

Looks a bit wacky on mobile:

image.png

#### 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

#### Gabriel Ebner (Oct 01 2020 at 17:57):

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

#### Gabriel Ebner (Oct 01 2020 at 17:58):

Dropdowns are not an option on desktop, though.

#### Gabriel Ebner (Oct 01 2020 at 17:58):

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

#### 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

#### Rob Lewis (Oct 01 2020 at 18:09):

I just updated it

#### Gabriel Ebner (Oct 01 2020 at 18:16):

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

#### 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?

#### 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.

#### Gabriel Ebner (Oct 01 2020 at 18:18):

No it should be exactly the same.

#### Rob Lewis (Oct 01 2020 at 18:19):

Hmm, let me check again.

#### Gabriel Ebner (Oct 01 2020 at 18:19):

Maybe the font sizes are different.

#### Rob Lewis (Oct 01 2020 at 18:21):

Site with css tweaks: image.png

Docs: image.png

#### Gabriel Ebner (Oct 01 2020 at 18:23):

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

Yes, of course

#### Rob Lewis (Oct 01 2020 at 18:25):

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

#### Rob Lewis (Oct 01 2020 at 18:26):

Resetting to dd6577c : image.png

#### Gabriel Ebner (Oct 01 2020 at 18:27):

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

#### 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

#### Rob Lewis (Oct 01 2020 at 18:30):

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

Ok, merged.

#### 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.

#### Gabriel Ebner (Oct 01 2020 at 18:31):

Let's see how this looks like when uploaded.

works_for_me.png

#### Rob Lewis (Oct 01 2020 at 18:34):

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

image.png

#### Rob Lewis (Oct 01 2020 at 18:36):

What do others see?

#### Bryan Gin-ge Chen (Oct 01 2020 at 18:40):

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

#### 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.

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

#### Rob Lewis (Oct 01 2020 at 18:59):

It works! (demo updated)

#### 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.

#### 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.

#### 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!

#### Kevin Buzzard (Oct 01 2020 at 19:56):

I just type mathlib into my browser search bar

#### Rob Lewis (Oct 02 2020 at 14:32):

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

#### 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.

#### 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?

#### Johan Commelin (Oct 02 2020 at 14:34):

layout looks good.

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

#### 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.

#### Eric Wieser (Oct 02 2020 at 14:52):

Agreed that the sidebar indent is weird

#### Gabriel Ebner (Oct 02 2020 at 15:13):

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

#### Patrick Massot (Oct 02 2020 at 15:18):

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

#### 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

#### 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.

#### 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.

Lovely :)

#### 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.

#### Rob Lewis (Oct 02 2020 at 16:12):

Is it possible to force them both to the bottom?

#### Gabriel Ebner (Oct 02 2020 at 16:41):

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

#### 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

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

#### 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.

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

#### Rob Lewis (Oct 03 2020 at 11:49):

This is live now!

Last updated: May 13 2021 at 16:25 UTC