mathlib index page small tweak

Stream: general

[Arthur Paulino]

I've opened this issue on doc-gen repo about making the index page more welcoming. I've also started a draft PR with some ideas. What do you guys think?

[Patrick Massot]

This webpage is not really meant to be welcoming. The welcoming page is https://leanprover-community.github.io/. We certainly don't want to lead people to think the reference API doc is the documentation entry point.

[Patrick Massot]

It doesn't mean we shouldn't work on improving that page, but let's not make it confusing.

[Johan Commelin]

I agree. But the part that makes the commit hashes explicit seems useful to me.

[Scott Morrison]

There should certainly be a link back to https://leanprover-community.github.io/ from the documentation index page, for people who've accidentally landed there.

[Scott Morrison]

Perhaps something along the lines of

This is the main documentation site for mathlib, the library of mathematics being developed in [Lean]. If you need information about installing Lean or mathlib, or getting started with a project, please visit our [community website].

This documentation site ...

[Scott Morrison]

It would be good if the text of the index page explained the structure of the sidebar a little.

[Arthur Paulino]

@Scott Morrison which URL should I use on the [Lean] hyperlink?

[Scott Morrison]

Good question. We don't really want to direct anyone to the essentially frozen page for Lean 3.whatever (before the community edition). Perhaps no hyperlink there, and just a link for [community website] in the second sentence.

[Arthur Paulino]

Hmm, maybe https://github.com/leanprover/?

[Eric Wieser]

That's the one we _don't_ want to link to!

[Patrick Massot]

This is the main documentation site for mathlib, the library of mathematics being developed in [Lean]. If you need information about installing Lean or mathlib, or getting started with a project, please visit our [community website].

This documentation site ...

I don't think of this as the "main documentation site". It's the API reference site. But this is not where people should go to learn.

[Arthur Paulino]

PR updated with improvements from feedback: https://github.com/leanprover-community/doc-gen/pull/140

[Arthur Paulino]

@Gabriel Ebner is there something else I need to do regarding this PR?

[Gabriel Ebner]

I believe Eric suggested to include the doc-gen revision as well.

[Gabriel Ebner]

I've only triggered the #deploy because I want to look at the rendered front page without building it locally.

[Arthur Paulino]

I see. How do I get the doc-gen commit? I searched in the repo files and I couldn't find anything similar to docgen_commit

[Eric Wieser]

You would have to plumb that through somehow, I don't think anything has access to it today; ultimately somewhere you'd call git rev-parse HEAD, or find a github env var with the commit sha.

[Eric Wieser]

So it would be fine IMO to leave to a follow-up PR

[Gabriel Ebner]

Like this https://github.com/leanprover-community/doc-gen/blob/e91ff9e28de1423658aa135ebca75baf17e9c375/print_docs.py#L168 and this https://github.com/leanprover-community/doc-gen/blob/e91ff9e28de1423658aa135ebca75baf17e9c375/print_docs.py#L229

[Arthur Paulino]

Alright, will do

[Arthur Paulino]

PR updated :+1:
https://github.com/leanprover-community/doc-gen/pull/140