ERR_NUM_LIN

Stream: mathlib4

[Yaël Dillies]

In a message like

Mathlib/RingTheory/DedekindDomain/Ideal.lean#L1: ERR_NUM_LIN: 1700 file contains 1542 lines, try to split it up

what does the 1700 stand for?

[Damiano Testa]

It seems to be a watermark: in the file scripts/lint-style.py there are these lines

            # Each exception contains a "watermark". If the file is longer than that, we also complain.
            if len(lines) > 1500:
                ex = [e for e in exceptions if e[1] == path.resolve()]
                if ex:
                    (_ERR_NUM, _path, watermark) = list(ex)[0]
                    assert int(watermark) > 500 # protect against parse error
                    is_too_long = len(lines) > int(watermark)
                else:
                    is_too_long = True
                if is_too_long:
                    new_exceptions = True
                    # add up to 200 lines of slack, so simple PRs don't trigger this right away
                    watermark = len(lines) // 100 * 100 + 200
                    output_message(path, 1, "ERR_NUM_LIN", f"{watermark} file contains {len(lines)} lines, try to split it up")

[Kevin Buzzard]

So the answer to the question is "it's (1542/100)*100+200 computed with nat division"??

[Damiano Testa]

It looks like it! :smile:

[Damiano Testa]

That and 1542 > 1500.

[Damiano Testa]

Maybe it is some kind of "buffer": it may be saying that the file is longer than what is oped for (1500), but not enough to really complain.

[Mario Carneiro]

The point is that style-exceptions.txt contains all the currently offending files with exact line counts, and we don't want to give a warning whenever any of those files change at all but still give a warning if they have changed significantly since the last time they were admitted as exceptions

[Mario Carneiro]

this works because the watermark is part of the nolint key but the exact line count is not

[Emilie (Shad Amethyst)]

The output_message part makes no sense to me. The "200 lines of slack" doesn't apply, since it's done after if is_too_long, and the message printed also doesn't make sense. The logic should be:

if len(lines) > 1500:
    # ...
    if ex:
        # ...
        watermark = int(watermark) // 100 * 100 + 200
        is_too_long = len(lines) > watermark

[Ruben Van de Velde]

No, that doesn't seem right. If the file is longer than 1500 lines, you need to put an exception in the style-exceptions file with a limit. The limit is suggested to be round(current length of the file) + 200. Once the file goes over that limit, you again get a lint failure

[Ruben Van de Velde]

That is, the watermark variable in the code only calculates the suggested new limit, it doesn't affect whether the linter fails or not

[Emilie (Shad Amethyst)]

Ah, that's not what I understood from the comment and printed message, but that makes sense

[Ruben Van de Velde]

I'm sure the message can be improved; I was just trying to make sense of the code :)

[Ruben Van de Velde]

Ugh. My PR made the lint fail, but bors didn't notice and merged anyway: https://github.com/leanprover-community/mathlib4/actions/runs/7725140864/job/21058735396

[Ruben Van de Velde]

Oh, this is because of python's nasty global variables. PR in a minute

[Damiano Testa]

By the way, this check seems to originate in this comment. And maybe @Michael Rothgang should be pinged as well!

[Michael Rothgang]

Ruben Van de Velde said:

Oh, this is because of python's nasty global variables. PR in a minute

I had noticed and wondered why. Thank you for fixing this quickly!

[Yaël Dillies]

Maybe the solution should rather be "Error iff the file is long and gets more than 100 lines longer in one PR"

[Yaël Dillies]

The current linter still prevents files from growing a tiny bit when close to the limit

[Ruben Van de Velde]

This is more or less what happens (for a value of 100 equal to 200)

[Yaël Dillies]

Maybe this is what was intended, but it's certainly not what's happening

[Ruben Van de Velde]

I disagree; that still allows unbounded growth

[Damiano Testa]

I still think that even if you slowly creep up the size of a file, there should be a predetermined hard limit preventing you to extend even by a single line a previously long file. Something like: you can extend an ignored file by at most 100 lines, but not past 2500 lines anyway.

[Michael Rothgang]

AIUI, the current behaviour is:

1. If a file grows from 1499 to 1502 lines, the linter errors
2. If the file already has more than 1500 lines, there will be a style exception for it, allowing between 100 and 200 lines of slack compared to when the exception was added. If there has been some time and a tiny addition pushes the file over the limit, the linter errors.
3. If a PR adds many lines to a file that is already too long, this might trigger the linter right away.

I see the linter error in (1) and (3) as a feature: it's a small speed-bump, a nudge that this file is too long and should be split. It can easily be silenced (add/update a style exception), but this forces you to think about it.

[Yaël Dillies]

Splitting files meaningfully is hard. I don't want the burden to do so to fall on random contributors. Understand: I would much rather have a list of files that need splitting and split them myself.

[Yaël Dillies]

Context: Scott Morrison hastily split a bunch of files last year to make place for the port, and while I agree with most changes I am still struggling with some of them.

[Michael Rothgang]

Yaël Dillies said:

Splitting files meaningfully is hard. I don't want the burden to do so to fall on random contributors. Understand: I would much rather have a list of files that need splitting and split them myself.

Don't we kind-of have such a list: it's in style-exceptions?

[Damiano Testa]

I agree with you, Yaël, but it is also simpler to add a no-lint than embarking on a split, so this is still the path of least resistance!

[Michael Rothgang]

I would be open to upgrading our policy around the lint to "no new exceptions" :-)

[Eric Rodriguez]

I'm happy for this error to be continually pushed onto style-exceptions; but every time it gets nolinted, we should have a discussion about it and maybe trying to ping relevant people.

[Yaël Dillies]

Damiano Testa said:

I agree with you, Yaël, but it is also simpler to add a no-lint than embarking on a split, so this is still the path of least resistance!

If that's what people end up doing, great! What I'm afraid of is that people will end up splitting suboptimally rather than adding an exception

[Damiano Testa]

Maybe the linter message could suggest adding the exception, unless you really think you can split the file!

[Mario Carneiro]

I think we should allow PRs to add lines to style-exception.txt, but it would be great if new arrivals in style-exception.txt or nolints.json caused a bot to post to zulip

[Kevin Buzzard]

"WARNING EVERYBODY: USER @whoever JUST DID A BAD THING"

[Kevin Buzzard]

yeah, sounds great <JOKE>

[Mario Carneiro]

(I realize you are joking, but) the idea would be to be able to track progress toward emptying those queues since I don't think we have a very good mechanism for it right now

[Mario Carneiro]

and since we want to take the focus for this off the PR author and toward general maintenance

[Mario Carneiro]

i.e. it would be something that people like Yaël Dillies who specialize in file splitting could subscribe to to be able to be regularly reminded that mathlib still has fires to put out

[Yaël Dillies]

Yep, that's exactly what I am after. This would be great :pray: