small TODOs

Stream: mathlib4

[Eric Rodriguez]

I've just opened #7987, which lists a bunch of todos from mathlib in a semi-disorganised way; I've been going through literally every occurence of the string "todo" in mathlib. These were chosen to specifically be quite small and limited in scope, and the hope is that most can be done in <1hr each, very often much less. I thought it'd be helpful to provide an easy way to access a long list of things to fix in Mathlib when you have a couple seconds here or there (or as the inspriation for this started, on somewhere like the Tube!). If you PR a fix to any of these, I'd appreciate editing the PR number into the issue, so that it is easy for others to keep track of.

I haven't finished going through the whole list yet, so I will probably add far more with time:)

This list uses the abbreviations SP and SC to mean small project and small chore; I feel like these are small mini things that are hopefully rewarding and not too awful to do. Some of these are chosen according to what I know well - there may be many more SPs in category theory, for example, but I'm mega unfamiliar with that part of the library, so I didn't want to send people on a wild goose chase!

Another thing I noticed whilst making this list is that there are often named issues; I saw Mario, Joël and Yael very often. It'd be nice to have a standardised format for these, so that they're easy to keep track of per-person. I think Joël tends to put his github username fairly often - I think this would be good to have!

[Johan Commelin]

Thanks so much for doing this!

[Patrick Massot]

This is nice, but don't forget that we also have thousands of porting notes to deal with. Getting rid of those would be a lot nicer than getting rid of TODOs, and more rewarding because there is a fixed number of porting notes whereas TODOs are created every day.

[Eric Rodriguez]

When I'm done with these I will go through the porting notes and try make a similar list. I worry that for that case it's going to be harder, as there are (as far as I've seen) many linked to the same issues, so it's worth gathering them by issue as opposed to by file.

[Yaël Dillies]

You tagged someone called @Yaelon Github. And it's not me! :sweat_smile:

[Bolton Bailey]

@Eric Rodriguez Do you mind if I edit the top-level comment in that PR to make it a checklist and add some small TODOs of my own? I would like it if there could be a tracking issue for small PRs (potentially with a section for first-timer friendly ones) and #7987 seems like a good candidate for that.

[Eric Rodriguez]

Yes, I'm very happy to have it be edited and formatted by everyone!