Splitting Mathlib/Data/Finset/Basic

Stream: mathlib4

[Antoine Chambert-Loir]

The addition of a 4-line lemma in Mathlib/Data/Finset/Basic.lean, see #17046, made it be 2 lines longer than the 3100 line limit. So either I change the counter at the end, or I try to split it, but it is not clear to me how to do it in a reasonable way (beyond putting roughly each section into a different file).

[Yaël Dillies]

The counter is there to be changed :wink:

[Antoine Chambert-Loir]

So let me put it at 314159 lines and everybody will be happy for some time.

[Ruben Van de Velde]

Add 200, please

[Ruben Van de Velde]

And with a bit of luck Yaël will deal with it :innocent:

[Damiano Testa]

The design should be that you cannot choose what the value is, automation will tell you what to use. If that is not the case, then it is a bug in the linter.

[Damiano Testa]

The linter had indeed a bug that would not check that the increase in the limit was "small". I fixed this, as well as a few other hanging issues with the linter:

• #17311, isolates the tests for the longFile to a separate file (probably completely uncontroversial);
• #17312, introduces the default value for file lengths, rather than hardcoding the 1500 limit (previously discussed on Zulip, probably also uncontroversial, though maybe less so than the previous one);
• #17309 combining the previous changes and revising the logic to really fix the issue at hand.

[Johan Commelin]

#17311
#17312 :writing:

[Damiano Testa]

Thanks Johan, for the merge and the suggestion!

[Johan Commelin]

#17312

[Damiano Testa]

#17309 is now available: it implements the correct behaviour, I hope.

Although it is labeled as t-linter, there is nothing meta to the PR, just a tricky sequence of if ... then... else that is supposed to

• disallow setting the linter value to a quantity less than or equal to the default,
• disallow setting the linter value, if the length is at most the default,
• suggest the second multiple of 100 larger than the file length, if needed;
• allow also the first multiple of 100 larger than the file length.

[Damiano Testa]

I find the tests and catching an issue in current master very encouraging. The testing has been much improved by moving longFile to a separate file and the customizable option.

[Michael Rothgang]

I just left a few comments. I would encourage another follow-up, auditing all occurrences of the magic number 1500 :-) and will be happy to review that quickly.
And I would suggest even more tests for that linter. The logic is subtle enough; having close to complete test coverage actually seems useful here.

[Michael Rothgang]

Damiano Testa said:

#17309 is now available: it implements the correct behaviour, I hope.

Although it is labeled as t-linter, there is nothing meta to the PR, just a tricky sequence of if ... then... else that is supposed to

• disallow setting the linter value to a quantity less than or equal to the default,
• disallow setting the linter value, if the length is at most the default,
• suggest the second multiple of 100 larger than the file length, if needed;
• allow also the first multiple of 100 larger than the file length.

and I should add: complain if the user set an option that is "unnecessarily" high (or not needed at all)