maintenance paper

Stream: general

[Rob Lewis]

@Floris van Doorn , @Gabriel Ebner , and I have written a paper about mathlib maintenance, specifically, linting and documentation. While it's not the deepest topic, we think there are interesting things to say here! If you're interested, take a look. Comments are welcome.
https://lean-forward.github.io/mathlib-maintenance/paper.pdf

[Patrick Massot]

I just found time to read that paper, it's really nice. It should become part of mathlib's documentation if the equation compiler doesn't complain too much about this idea.

[Johan Commelin]

Yes, I've also found reading the paper very pleasant.

[Johan Commelin]

While reading library notes, it made me think, should we turn https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category/default.lean#L27 into a note as well? (@Scott Morrison)

[Scott Morrison]

Sounds good.