Discoverable list of clean-up tasks

Stream: mathlib4

[Bolton Bailey]

Michael Rothgang said:

16. Make this list discoverable for new or existing contributors, as time goes by. More broadly, how would a contributor find such ideas of tasks? Feel free to start a zulip thread for discussion; I'll be happy to edit in the link.

I have made tracking issues on the GitHub for various things, including tactics, linters, and renamings. I try to update these lists when I come across new ideas on Zulip or on my own - my hope is that by putting the right labels on these issues, it will be easier for people interested in them to find them.

I could make another tracking issue for the things in this list. Is that something we want? Is there a way that these lists could be under another username so they look/can become more of a community effort than my personal project?

[Notification Bot]

A message was moved here from #mathlib4 > Refactoring idea den by Michael Rothgang.

[Michael Rothgang]

Thanks for pointing this out; I had not seen those tracking issues! I think this could be a good start.

[Michael Rothgang]

I continue to think there is something we could do better, but cannot put my finger on it yet. This blog post goes in the right direction, at least.

[Bolton Bailey]

Ok, I made this tracking issue #24212