lean-lang.org website

Stream: new members

[corrededCrustacean]

Hi, is there a way to contribute to the lean-lang.org website? There are many important resources which are hard to find and which should be linked on the main website imo, like the mathlib documentation, reservoir and loogle.

I also think the link style should be changed to something more readable, the unhovered line is almost transparent and makes it really hard to see where the links are.

Another thing which would be nice to have is an RSS feed for publications and blog posts.

[Bolton Bailey]

Not sure if the mathlib documentation should be linked from the FRO website because mathlib is not managed by the FRO, it's managed by leanprover-community. The other points I agree on though.

[corrededCrustacean]

Right, by mathlib I meant the standard library more specifically, I was confused by the fact that they're together on the lean community website.

[Patrick Massot]

There are plans do redesign that whole website, I don’t think that isolated contributions would be productive at this point. But thanks for proposing to help!

[Eric Wieser]

It's possible that a contribution of an RSS generator to verso (the tool which generates the blog) would be appreciated, but @David Thrane Christiansen is the person to ask there. Perhaps opening a feature request on the repo is a reasonable step?

[Patrick Massot]

I missed the RSS bit, that may be welcome indeed.

[corrededCrustacean]

cool, I will look at it!

[David Thrane Christiansen]

RSS generator is planned, but it's prioritized under various other tasks (like supporting a revised user's manual). My only concern with incoming RSS code is that I'd spend much more time managing the PR than it would take just writing the code - RSS/Atom include lots of XML complexity to get right, and the existing codebase is still poorly documented and rapidly evolving. But RSS is definitely on the roadmap, and if code arrives that I'm happy to support and maintain forever without requiring tons of mentorship on the way, then it'd be good :⁠-⁠)

[David Thrane Christiansen]

Thanks, @corrededCrustacean !

[David Thrane Christiansen]

RE the graphics - we've got a redesign on the way, and the website repo is private (so we can do things like prepare a PR about something like a hiring announcement), so CSS tweaks there are probably better dealt with through patience.