website

Stream: general

[Patrick Massot]

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.

[Rob Lewis]

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

[Patrick Massot]

Yes, but first we need a cleaner structure.

[Patrick Massot]

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

[Bryan Gin-ge Chen]

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

[Patrick Massot]

Actually it looks like there are bugs in my script

[Patrick Massot]

There should be more links coming out of mathlib-overview

[Patrick Massot]

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

[Mario Carneiro]

I assume the links aren't actually a tree?

[Mario Carneiro]

because that would be really weird

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Jiekai]

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.

[Shing Tak Lam]

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.