Zulip Chat Archive

Stream: general

Topic: maintenance paper


view this post on Zulip Rob Lewis (Mar 17 2020 at 17:34):

@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

view this post on Zulip Patrick Massot (Mar 20 2020 at 16:33):

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.

view this post on Zulip Johan Commelin (Mar 20 2020 at 19:19):

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

view this post on Zulip Johan Commelin (Mar 20 2020 at 19:19):

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)

view this post on Zulip Scott Morrison (Mar 20 2020 at 19:20):

Sounds good.


Last updated: May 11 2021 at 13:22 UTC