Mathlib docs index page

Stream: general

[Kyle Miller]

Currently https://leanprover-community.github.io/mathlib4_docs/index.html shows the Lean 4 commit used to build the documentation.

What would it take to include the following information?

• The Lean toolchain version
• A list of all the dependencies and their commits (including the Mathlib commit)
• Additional links to https://lean-lang.org/ and https://leanprover-community.github.io/

I think that would help a lot with navigating through some of the Lean ecosystem.

[Bryan Gin-ge Chen]

It seems the template for the main page is here: https://github.com/leanprover/doc-gen4/blob/e3f8a871d2beb4264e31eee6e3e4ee504b88638f/DocGen4/Output/Index.lean

[Henrik Böving]

• The Lean toolchain version: That's trivial as doc-gen is built with the same version so we can include the Lean version string
• A bit less trivial as there is some interaction with lake to be had here but still doable
• That would again be trivial

[Chris Henson]

In general, I think that the old index page for Lean 3 Mathlib had a bit more information that was potentially helpful for newcomers (and also looked nice IMO). Compare what shows up with a Google search:
ebea7eb8-76d1-41ce-8a2c-9d187c057f90.png