Zulip Chat Archive

Stream: general

Topic: Using MSC identifiers in mathlib

Scott Morrison (Jun 01 2021 at 00:51):

194 missing module docstrings!

Scott Morrison (Jun 01 2021 at 00:53):

All listed at https://github.com/leanprover-community/mathlib/blob/master/scripts/style-exceptions.txt if anyone wants to tackle a few!

Johan Commelin (Jun 01 2021 at 05:17):

@Yaël Dillies has been making several PRs with module docstrings lately. Thanks a lot for that!

Yaël Dillies (Jun 01 2021 at 07:07):

Having to revise for exams gives me documentation energy :sweat_smile:

Sebastian Reichelt (Jun 01 2021 at 20:32):

Mario Carneiro said:

I usually find wikipedia links to be significantly more helpful than MSC codes

It would be great to have a Wikipedia link in every docstring because such a link could also be used as a key into a database of definitions and theorems. I wrote a proposal about this here: https://github.com/SReichelt/slate/discussions/84. If the Wikipedia links are already in the source code, that would be the best of the different variants described there, because the database could be updated automatically by regularly scraping the mathlib docs.

Last updated: Aug 03 2023 at 10:10 UTC