Discussion: Mathlib documentation overview

Stream: mathlib4

[Anne Baanen]

Discussion thread for the #announce > Mathlib documentation overview

If you have written new documentation, you can add it to documentation.yaml in the website repository. If you are missing documentation on a given topic, please request it on Zulip.

In this thread I'm especially curious to hear what you think of the design of the page. Do you have suggestions for the layout or interactivity?

[Chris Henson]

It's great to start collecting these resources! Regarding the design: I think it would be helpful if the h2 headers were collapsible and closed by default. Then you could place the description you have of each quadrant next to the header more easily and not start with such a long list to scroll. Something like:
image.png

[Kim Morrison]

I think it's important to have a (curated) order within each category. e.g. the Lean Language Reference should be the first item in the reference section!

[Kim Morrison]

I think we also already need subcategories. There are many examples here, but e.g. all of Bhavik's lecture notes should be under a collapsible subheading too.

[Lawrence Wu (llllvvuu)]

“library note [implicit instance arguments]” links to AlgebraicHierarchy.lean

EDIT: sorry, I just noticed they are all in the same file. I guess this was just GitHub’s jump to line not working.

[Aaron Liu]

Those links aren't permalinks so I'm worried that when mathlib changes the links will start pointing to something else since the line number the library notes start at jumps around as the file has stuff added or moved or refactored

[Bryan Gin-ge Chen]

We can probably use doc-gen's source-finding feature: https://leanprover-community.github.io/mathlib4_docs/find/?pattern={decl}#src (this is what powers the src#xxx linkifier)

[Bryan Gin-ge Chen]

Hmm, this links to the docs and not the GitHub source, but maybe that's fine: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«implicit instance arguments»#src (Zulip doesn't seem to like the URL)

[Chris Henson]

Maybe even slightly preferable, as the docs are a little nicer to read? I've opened https://github.com/leanprover-community/leanprover-community.github.io/pull/745 for consideration doing this.

[Bryan Gin-ge Chen]

Thanks for making the PR! If we prefer going staying on the docs page rather than GitHub, I think you can replace the #src in the URLs with #doc. (I'm not sure why #src doesn't work, maybe doc-gen isn't able to get the data for that command or something yet.)

I think @Anne Baanen was planning some improvements to doc-gen where library notes, tactics, attributes, commands, etc. would get their own pages, so I don't know if they eventually want to change these URLs to point there, but otherwise this PR looks good to me.

[Chris Henson]

That makes sense, I've updated to #doc links.

[Chris Henson]

And those changes to doc-gen sound great, I'll be looking forward to it!

[Anne Baanen]

Chris Henson said:

It's great to start collecting these resources! Regarding the design: I think it would be helpful if the h2 headers were collapsible and closed by default. Then you could place the description you have of each quadrant next to the header more easily and not start with such a long list to scroll. Something like:
image.png

Thanks for your feedback! I've implemented this in leanprover-community.github.io#750