feat: documentation overview page

[Vierkantor]

This page is intended to be a complete collection of all the pieces of documentation for Mathlib users and Lean users more generally. I have gone through everything findable on the community website, and quite a few suggestions on the Zulip chat and tagged and categorized them all.

On the rendered page, we can see a diagram of the Divio classification system. I also added the possibility to filter the entries by tags.

Here is the rendered page, which works standalone in your browser (only missing a bit of its formatting):
documentation.html.

[bryangingechen]

This is great! A few things:

• The "sticky" tag selection banner is a bit large and it might be a bit annoying on mobile or narrow screens. Could you add a way to collapse it?
• It might be nice to put numbers next to the tags showing how many items have that tag. For example, there doesn't seem to be anything tagged "Lean 3" yet; maybe we can just hide such tags?
• Maybe we should hide the outdated documentation elements by default? Or grey them out somehow since the "historical" tag is itself grey and might be easy to miss.
• It would be good to add and display author data. I'm happy to help with editing the YAML file once you decide on the format for that.

[Vierkantor]

Thanks for the review! I implemented your suggestions: adding a show/hide button for the tag filters, tag counts (hiding tags with count 0), and also hiding entries with tag historical.

For author data, I went with a plain string field, comma-separated like we have for the Authors: line in the copyright headers. For entries that do not have any obvious authorship information and live on the leanprover-community.github.io website, I went with "the Mathlib community". Or should we be more precise (for example, looking at the commit history for this information)?

[bryangingechen]

Thanks, looks like you've addressed all my concerns! Am I correct that there's intentionally no way to view items tagged historical now? I'd prefer if they were still accessible somehow, but I can also get behind the idea to keep them from polluting search results, etc.

I'm fine with "the Mathlib community"; it would feel strange to include authorship info that isn't written in the source files. (If any of the authors would like to claim authorship of one of the documents here, we'll have to remember to remind them to update both the markdown and this yaml file though)

[adomani]

I love this, thanks! I just have one comment: would it be possible to have links external to leanprover-community to open in a separate tab?

Maybe this already happens, but I noticed that it didn't in the html file linked in the PR description.

[YaelDillies]

What about blogposts on the community website? For example, @Paul-Lez and I are publishing simproc documentation on it. Should the corresponding blogposts be referred in documentation.yaml, or is the consensus that we should perhaps turn the blogposts into a more perennial form of documentation?

[Vierkantor]

would it be possible to have links external to leanprover-community to open in a separate tab?

Doing so is mostly discouraged by web accessibility guidelines: https://www.w3.org/WAI/WCAG22/Techniques/general/G200

What we could do, however, is add a little icon to indicate external links. (It may be a good idea in general to indicate whether something is community-maintained or not!)

[Vierkantor]

What about blogposts on the community website?

Good question! Blog posts can definitely count as documentation, and we already link a few blog posts on this page. But they should also remain relevant as time goes by. Are you, as authors, planning on updating your post to keep up with Lean changes? If not, making it part of the living set of documentation we have (maybe eventually as part of the Mathlib manual?) would be worth it.

But I think for this PR we should focus more on the structure of the page, not its exact contents. I'd be very happy to accept PRs changing the contents of documentation.yaml later!