linter

Stream: mathlib4

[Antoine Chambert-Loir]

I wonder about the order in which some linters are executed when mathlib is built in branches. For example, after a 30 min long compilation (on github), I get the following error message:

Run ! grep --after-context=1 "stdout:" stdout.log
stdout:
./././Mathlib/Algebra/Algebra/Unitization.lean:739:4: warning: `Function.comp.left_id` has been deprecated, use `Function.id_comp` instead

and I feel it is a waste of computation to have this checked only after mathlib has been compiled in full.

[Mario Carneiro]

that error message would have stopped the build if we had warning-as-error enabled

[Mario Carneiro]

I think we actually want log-as-error in mathlib, because noisy files are not allowed so there is no point in building more oleans based on a noisy file since it can't be merged anyway

[Mario Carneiro]

I don't think there is a way to get lake to do this though, unless we added a shim over the lean called by lake

[Eric Wieser]

Mario Carneiro said:

I think we actually want log-as-error in mathlib, because noisy files are not allowed so there is no point in building more oleans based on a noisy file since it can't be merged anyway

I don't agree with this; if I'm trying to work out if a refactor works, I want to find out about as much fallout as possible before having to think about linter complaints.

[Eric Wieser]

Of course, maybe those PRs should just adjust the flags if they want that behavior, but I think it is worth documenting that approach before we change the default behavior.

[Ruben Van de Velde]

Yeah, I almost never want warnings as errors while I'm working on something, because that limits how many issues I can fix per ci run, especially since those have quite a bit of overhead

[Antoine Chambert-Loir]

I understand. Is there a place where the settings are documented and where I could guess how to change them if I wish to?