Topic: documentation links missing
Scott Morrison (Aug 14 2020 at 00:00):
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:
to the sidebar?
Scott Morrison (Aug 14 2020 at 00:01):
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 (Aug 14 2020 at 00:32):
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 (Aug 14 2020 at 14:04):
One more idea for docs: add "Namespaces" subtree that does the same thing as
Scott Morrison (Aug 15 2020 at 05:02):
@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 (Aug 15 2020 at 05:41):
I believe you should edit this jinja2 template
Scott Morrison (Aug 15 2020 at 05:51):
I see! A whole repository I didn't even know about. :-)
Scott Morrison (Aug 15 2020 at 05:55):
Presumably I should put this under the "Tutorials" header, and add these links to wherever
extra_doc_files is drawn from.
Scott Morrison (Aug 15 2020 at 06:01):
Last updated: May 14 2021 at 04:22 UTC