flakiness in style linter?

Stream: mathlib4

[Bryan Gin-ge Chen]

Today a number of bors batches ended up failing due to a style problems coming from code in master, see e.g. this log. This was fixed in #16677, but the underlying issue of how this code snuck past the style linter is still unresolved.

If anyone can help investigate this, it would be greatly appreciated! It looks like this time the culprit PR was #16317. It seems to have passed all the checks before merging, and got a green check on master as well. What's also strange is that not all of the bors batches failed, e.g. #16611 was merged successfully.

Note that a similar incident occurred a few weeks ago with #16255 getting merged with style issues and #16292 fixing them.

[Damiano Testa]

I'll try to take a look, but it will likely be tomorrow.

[Damiano Testa]

I could only take a quick look, but I can see that the failed linter step in the log that you linked to is preceded by a (failed? not executed?) install Python check.

[Damiano Testa]

Today there was an issue with CI that made other similar installation steps take long and maybe timeout and fail.

[Damiano Testa]

I still think that CI should have picked this up, but maybe it is an indication that there was some unusual external condition that made CI pass even with the linter warnings?

[Bryan Gin-ge Chen]

I think skipping install Python is expected, per this line in the workflow.

[Damiano Testa]

Ah, ok. Back to debugging... :smile:

[Damiano Testa]

I don't have more time today, I'll try to investigate more tomorrow.

[Bryan Gin-ge Chen]

Thanks very much for taking this on!

[Adomas Baliuka]

In case it helps to localize the issue, I think I already had this 2 weeks ago here:

https://github.com/leanprover-community/mathlib4/pull/16257

[Bryan Gin-ge Chen]

Yes, it looks like your PR was one of the victims from #16255 sneaking past the linter somehow.

[Damiano Testa]

This is very confusing: the tests work on the same code... sometimes!

I wonder whether it is caused by the fact that there are different scripts for the linters floating around and these are PRs that use a temporary faulty script, that is no longer in master, but is somehow used by CI?

[Bryan Gin-ge Chen]

Hmm, but when each PR is sent to bors it should be placed on top of master which should always have the latest version of the scripts, right?

[Bryan Gin-ge Chen]

Just brainstorming some possible sources of non-determinism before bed (without ever having studied the style linter code), but:

Whenever style linting is run, it is run on every single file in mathlib, right? There shouldn't be any circumstances when we skip linting some files due to some caching or something?

The order that files are linted in shouldn't affect the results of style linting, right?

[Damiano Testa]

I have not written the text-based linters (which check, for instance, wrong indentation and ending whitespace), but my understanding is that indeed they run on every file and each file is a completely separate and independent run.

[Damiano Testa]

Here is a possible explanation.

1. The text-based linters are run in a workflow separate from the main build;
2. the text-based linters use the content of {Mathlib Archive Counterexamples}.lean to decide what to lint;
3. the mk_all script is in the main build and takes some time to run;
4. by the time the lint workflow reaches the actual linting, it may or may not be the case that the mk_all script has added all the new files to Mathlib.lean;
5. if the files are missing from Mathlib.lean, the linting does not inspect them.

[Damiano Testa]

Given that the text-based linters use Mathlib.lean, I am tempted to add anyway a lake exe mk_all step to the Lint style workflow, just in case it matters.

[Kim Morrison]

Damiano, if it's a separate workflow, whatever mk_all does in the main workflow is completely irrelevant: it's probably running on different machine!

[Damiano Testa]

Ah, that would also explain the flakiness! :smile:

[Damiano Testa]

Let me add the mk_all step anyway, since it will make it at least lint all the mathlib files anyway.

[Damiano Testa]

Oh, sorry, it is not a different workflow it is a different step in the same workflow.

[Damiano Testa]

(Not sure about the exact name: it is in the same file, but it is run independently of the build step.)

[Damiano Testa]

#16696

[Kim Morrison]

In that case it is operating on the same local files.

[Damiano Testa]

Ok, I'm not sure that my explanation for why some CI runs fail to identify linter failures is correct, but I do think that adding lake exe mk_all before linting makes the linting step more reliable.

[Ruben Van de Velde]

That makes no sense to me. If mk_all changes something, bors shouldn't merge

[Damiano Testa]

I have seen a situation where a first run of bors fails, it bisects the PRs, runs again and now it is successful due to some modification that happened in the previous run. I wonder if maybe this is an explanation?

[Damiano Testa]

(Anyway, I am just brainstorming at the moment, I do not understand what is going on.)

[Ruben Van de Velde]

(The entire situation makes no sense to me either)

[Ruben Van de Velde]

Also the failures in #16317 should have been caught by the python linter, which doesn't seem to read Mathlib.lean at all

[Ruben Van de Velde]

Oh hmm.

$ ./scripts/print-style-errors.sh
xargs: unmatched single quote; by default quotes are special to xargs unless you use the -0 option

[Michael Rothgang]

Two comments from the peanut gallery. I sadly won't have time to look into this for two weeks.
Nice robustness improvement! I'm not sure if it will help, though: the text-based linter calls lint-style.py via print-style-errors.sh --- which uses find and not Mathlib.lean for determining which files to lint.

In terms of recent bugfixes/changes to the handling of Python linters: did the PR include #15954 already?
Put differently: if you can reproduce the error in local testing, does running lint-style.py on the affected file find it? Does running print-style-errors.sh find it? (If the answer is yes and yes, but lake exe lint-style does not, that sounds like #15954.)

[Damiano Testa]

Great find! I'm still not sure why it later decided to do the right thing, once stuff was in master, but finding an error is a good thing!

[Michael Rothgang]

Ruben Van de Velde said:

Oh hmm.

$ ./scripts/print-style-errors.sh
xargs: unmatched single quote; by default quotes are special to xargs unless you use the -0 option

I saw that in local testing also (and sadly have no idea where this comes from). Running lake exe lint-style still errored for me, though - so this shouldn't matter. (Unless I'm wrong :-))

[Ruben Van de Velde]

It's probably Mathlib.Tactic.LinearCombination'

[Ruben Van de Velde]

Let's see if I can verify that...

[Damiano Testa]

So, besides the ' linter for declaration names, there is also the need for a ' linter for file names!

[Michael Rothgang]

which can be purely text-based :-)

[Damiano Testa]

There is already a check that filenames are unique up to capitalization. Maybe filenames should consist just of upper/lower case letters?

[Ruben Van de Velde]

Bingo!

[Ruben Van de Velde]

If Mathlib/Tactic/LinearCombination'.lean comes before the offending file in the find output, it fails to fail (heh), otherwise it finds the issue

[Damiano Testa]

So, an alternative could be to rename Mathlib/Tactic/LinearCombination'.lean to Mathlib/Z/Tactic/LinearCombination'.lean.

[Damiano Testa]

Or Mathlib/ZZZZZZZZZZZZZZZZZZZZZZZ/Tactic/LinearCombination'.lean, just to be safe.

[Ruben Van de Velde]

Fix incoming

[Ruben Van de Velde]

#16699

[Bryan Gin-ge Chen]

Wow, thanks for getting to the bottom of this!

[Ruben Van de Velde]

It's annoying that IO.Process.run just drops the stderr on the floor

[Sebastian Ullrich]

Use Process.output?

[Ruben Van de Velde]

Then I'd have to basically inline run, right?

[Sebastian Ullrich]

I don't really know what your requirements are. But it's not much to inline.

[Michael Rothgang]

#16709 fixes this, and is just three added lines