CI fails with unused variable error

Stream: PR reviews

[Michael Rothgang]

Some recent PRs (certainly my own #11605 and #11607; I haven't checked exhaustively) are failing on CI, with errors unrelated to it: stdout is noisy; as there is a warning emitted

./././Mathlib/Analysis/Distribution/SchwartzSpace.lean:1071:11: warning: unused variable `hpos` [linter.unusedVariables]

[Michael Rothgang]

Filed a PR removing the unused have at #11609.

[Kevin Buzzard]

there has certainly been some chat recently about a much more powerful unused variable linter; perhaps it's hit master and this is fallout?

[Michael Rothgang]

I don't know! In any case, master being noisy is not good - what happened to CI?

[Yaël Dillies]

I am fixing that unused variable in #11606 so it won't be long before master is silent again

[Kevin Buzzard]

Are you using it?

[Kevin Buzzard]

ooh there's drama in #11606 (bors got cancelled for some reason)

[Kevin Buzzard]

Wooah -- are we about to hit some kind of "nothing out of sync" milestone here?? #outofsync

[Yaël Dillies]

Yep!

[Yaël Dillies]

Well, there are a few more files that disappeared from #outofsync because they never were ported, but Alex Kontorovich is taking care of one of them and the other one is mine

[David Loeffler]

FWIW, I suspect the reason this has come up isn't because of linter changes. I think it's because positivity got better as a result of #10661, so it no longer needs to be told that some integral is non-negative – it can work that out for itself.

[Yaël Dillies]

Yes but the question is how the unused argument wasn't detected on master

[Ruben Van de Velde]

I think the recent ci changes to run tests after a failed build may be to blame

[Ruben Van de Velde]

Either that or the cache. Does bors use it?

[Sophie Morel]

Ha, I had the same CI fail on my PR #11155 and was very confused, as I had only been doing linear algebra!

[Yaël Dillies]

It's now fixed on master!

[Eric Wieser]

Michael Rothgang said:

Filed a PR removing the unused have at #11609.

This got merged as an empty commit :upside_down:

[Moritz Doll]

David Loeffler said:

FWIW, I suspect the reason this has come up isn't because of linter changes. I think it's because positivity got better as a result of #10661, so it no longer needs to be told that some integral is non-negative – it can work that out for itself.

In fact the linter-offending code is exactly the reason I wrote the positivity extension. I am very confused however why the linter did not complain on #10661

[Ruben Van de Velde]

Yeah, the change was in #11606