Fixing docstrings in Mathlib 4

Stream: mathlib4

[Antoine Chambert-Loir]

I often notice that some docstrings have not been ported correctly, for example, because the comments still mention the old Mathlib3 name. What is the proper way to suggest corrections?
Should I open a PR for each of them, or could there be a larger collaborative PR to that aim?

[Anatole Dedecker]

I think the most efficient way is not to organize things too much here, so you can open a PR for each one (or a small batch) and tag the corresponding PR as "easy". At some point we will probably organize some kind of coordinated effort for this, but for now please fix the one you stumble upon!

[Riccardo Brasca]

There are several PRs fixing small problems like this. I think you can just open a PR every time you notice a problem (maybe check at least the whole file...). If it is just in the doc you can label it "easy" and it should be reviewed quicky.

[Eric Wieser]

Separate PRs are better because if the fixes are in different areas of the library, different people might feel more qualified to know what the comment was supposed to be

[Eric Wieser]

If it's all in one PR, everyone is waiting on someone else to review part of it

[Matthew Ballard]

I am hopeful this organic piecemeal approach will be all that is necessary

[Eric Wieser]

I guess an alternative would be to run fix-comments.py on everything, and then have people carefully review for false-positives

[Ruben Van de Velde]

Eric Wieser said:

I guess an alternative would be to run fix-comments.py on everything, and then have people carefully review for false-positives

Note that the script is not idempotent, e.g. ring -> Ring -> RingCat

[Jireh Loreaux]

Could fix-comments read an align file where we remove all the category theory stuff? Or all the stuff with upper case Lean 3 decls? That should make it almost idempotent.

[Eric Wieser]

What if you ran fix-comments in reverse first, then ran it forwards again?

[Jireh Loreaux]

Did anything get aligned to an existing mathlib 3 name (different from the one it's coming from)? If so, then that approach doesn't work either, but it's possible it would be less error prone.

[Eric Wieser]

Yes, there are a few lemmas where the prime swapped between 3 and 4

[Eric Wieser]

I think they're probably not mentioned in docstrings that often

[Mario Carneiro]

why don't you use the actual #aligns in mathlib to do this, instead of just using the mathport heuristic?

[Jireh Loreaux]

Isn't that what we do already?

[Eric Wieser]

fix-comments does that (via grep), but as pointed out above we now have no automated way to tell which comments have already been fixed