Zulip Chat Archive

Stream: general

Topic: website


view this post on Zulip Patrick Massot (Jun 28 2020 at 09:38):

Jasmin Blanchette said:

"Lots of wonderful things on the community web site, all hidden under two layers of links." -- Anonymous (Gabriel E.)

I took time to map the website (using a small python script) links.pdf. I'm sure this will motivate people to work on this issue.

view this post on Zulip Rob Lewis (Jun 28 2020 at 09:59):

For indexing purposes, we should also generate a sitemap and file it with the relevant search engines, e.g. https://leanprover-community.github.io/mathlib_docs/sitemap.txt

view this post on Zulip Patrick Massot (Jun 28 2020 at 10:00):

Yes, but first we need a cleaner structure.

view this post on Zulip Patrick Massot (Jun 28 2020 at 10:01):

In particular decide something about https://leanprover-community.github.io/theories.html which is currently very hard to find

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 10:01):

I think improving the links in the header (maybe including more and organizing them into menus?) will make a big difference.

view this post on Zulip Patrick Massot (Jun 28 2020 at 10:02):

Actually it looks like there are bugs in my script

view this post on Zulip Patrick Massot (Jun 28 2020 at 10:03):

There should be more links coming out of mathlib-overview

view this post on Zulip Patrick Massot (Jun 28 2020 at 10:07):

But I need to go for family chore now. I'll be back tonight.

view this post on Zulip Mario Carneiro (Jun 28 2020 at 10:09):

I assume the links aren't actually a tree?

view this post on Zulip Mario Carneiro (Jun 28 2020 at 10:09):

because that would be really weird

view this post on Zulip Patrick Massot (Jun 28 2020 at 20:14):

I'm back with a less bad approximation: links.pdf

view this post on Zulip Patrick Massot (Jun 28 2020 at 20:15):

The trouble is I reused an old script whose purpose was to detect dead links without rechecking multiple times the same file, so I ended up with a covering tree.

view this post on Zulip Patrick Massot (Jun 28 2020 at 20:16):

This graph really makes me wonder how people can still fail to meet https://leanprover-community.github.io/install/project.html

view this post on Zulip Patrick Massot (Jun 28 2020 at 20:16):

Maybe we should tweak the site building script so that it adds a link to that page every two lines.

view this post on Zulip Patrick Massot (Jun 28 2020 at 20:17):

Or maybe have some javascript trickery that redirects the first ten requests from a given IP to this page.

view this post on Zulip Jiekai (Jun 30 2020 at 02:40):

Patrick Massot said:

Or maybe have some javascript trickery that redirects the first ten requests from a given IP to this page.

That sounds too much trickery.

view this post on Zulip Shing Tak Lam (Jun 30 2020 at 02:54):

Patrick Massot said:

This graph really makes me wonder how people can still fail to meet https://leanprover-community.github.io/install/project.html

Right now it's just a link at the bottom of the install pages and it's quite easy to miss. Might be worth promoting it to an <h3> with it's own section or something like that so people are less likely to miss it.


Last updated: May 09 2021 at 18:17 UTC