CI "lint style" failure

Stream: mathlib4

[Bryan Gin-ge Chen]

If you have a PR where the "Lint style" job started failing with some stuff in the logs about references.bib: merging master into your branch should fix this.

The cause is that the linter checking the format of the .bib file was turned off until #29575. (The issues were fixed in master in #29572).

[David Loeffler]

I just got a CI failure on the "lint style" step for one of my PR's – CI run here:

https://github.com/leanprover-community/mathlib4/actions/runs/17697069282

I'm puzzled because the output of the "lint style" script doesn't seem to contain any actual error message – all the output looks fine, but it still says Error: Process completed with exit code 1 at the end and I can't work out why.

[Michael Rothgang]

The log shows an error: the .bib file is not normalised.

[Michael Rothgang]

That one was fixed a few days ago; does merging master fix this?

[Bryan Gin-ge Chen]

Indeed, merging master should fix this, see #mathlib4 > CI "lint style" failure

[David Loeffler]

Thanks, trying that now! (This would have been easier to debug if the .bib file linter printed an explicit error message "ERROR: .bib file wrongly formatted" rather than, or as well as, outputting the diff into the CI logs.)

[Michael Rothgang]

I think doing both would be nice, with the big "error" after the diff.

[Bryan Gin-ge Chen]

I think we never added messages like this because the linters used to be in separate named steps; now that they've been combined into one action this is indeed necessary.

I've opened lint-style-action#2 for this, since I probably won't be able to work on this for a while.