documentation links missing

Stream: general

[Scott Morrison]

Now that https://leanprover-community.github.io/mathlib_docs/ is turning into the main entry point for documentation, a few very useful pages have perhaps been orphaned.

Should we add links directly to:

• https://leanprover-community.github.io/contribute/doc.html
• https://leanprover-community.github.io/contribute/style.html
• https://leanprover-community.github.io/contribute/naming.html

to the sidebar?

[Scott Morrison]

Otherwise I don't see how to find them once you've arrived at https://leanprover-community.github.io/mathlib_docs/

[Frédéric Dupuis]

Not too long ago I tried (and failed!) to find those pages that I had definitely seen at some point. So I think it's a great idea!

[Yury G. Kudryashov]

One more idea for docs: add "Namespaces" subtree that does the same thing as #print prefix

[Scott Morrison]

@Gabriel Ebner, @Rob Lewis, I'm happy to add these links myself, but I realise that I don't know how to. How am I meant to learn how the mathlib_docs directory of the community website is generated?

[Bryan Gin-ge Chen]

I believe you should edit this jinja2 template

[Scott Morrison]

I see! A whole repository I didn't even know about. :-)

[Scott Morrison]

Presumably I should put this under the "Tutorials" header, and add these links to wherever extra_doc_files is drawn from.

[Scott Morrison]

https://github.com/leanprover-community/doc-gen/pull/51