Zulip Chat Archive

Stream: general

Topic: documentation links missing


view this post on Zulip 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?

view this post on Zulip 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/

view this post on Zulip 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!

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 14:04):

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

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Aug 15 2020 at 05:41):

I believe you should edit this jinja2 template

view this post on Zulip Scott Morrison (Aug 15 2020 at 05:51):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 15 2020 at 06:01):

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


Last updated: May 14 2021 at 04:22 UTC