Approach for `nthLe` refactoring?

Stream: mathlib4

[Arien Malec]

For Combinatorics.Composition I want to refactor nthLe to get but BigOperators.sum_take_succ is defined in terms of nthLe

Is the right thing to do here to rename BigOperators.sum_take_succ to BigOperators.sum_take_succ' or refactor to use get or to mark things in Combinatorics.Composition as nolint?

(I've noticed that the deprecated lint does not fire when the deprecation is in the binding rather than the body).

[Thomas Murrills]

there might be some useful discussion about this in the old Data.List.Basic zulip thread—iirc “get is the new nthLe” and we should just transition everything to get, but it’s worth checking with someone who’s sure :)

[Arien Malec]

that's right & that's the deprecated message for nthLe -- the question is really how far/fast to take the refactor..

[Thomas Murrills]

as it happens this was indeed addressed by Mario right at the end of the #mathlib4 > Data.List.Basic thread :)

[Thomas Murrills]

(actually it's still a little unclear to me what to do after re-reading those messages...I'm not sure if we now have the majority of code available for the nthLe refactor to proceed and therefore it should, or if it's still intended to be a future refactor)

[Yury G. Kudryashov]

I don't think that we should start a refactor before the porting is done (unless you want to do the refactor both in Lean 3 and Lean 4).

[Arien Malec]

So, to make it clear:

1. If it's easy and targeted to remove nthLe in favor of get, do it.
2. If not, nolint the deprecated message with a porting note TODO

[Yury G. Kudryashov]

In case 1, leave a deprecated version of a lemma formulated using nthLe anyway.

[Yury G. Kudryashov]

It can call the get version. Also,

3. If you're talking about a leaf file/folder, then you can migrate once the whole folder is ported.

[Eric Wieser]

The "whole folder" strategy is still risky if mathlib3 gains new theory in that folder.

[Yury G. Kudryashov]

IMHO, if the whole leaf folder is ported, then we can freeze it in mathlib3 and tell contributors to add new results to the mathlib4 version.

[Yury G. Kudryashov]

(of course, this is only my opinion and any freeze should be discussed with all maintainers)