silent CI lint error

Stream: mathlib4

[Edward van de Meent]

in this pipeline, the step throws an error but succeeds anyway?

[Edward van de Meent]

that's not intended, right?

[Kim Morrison]

No, that is definitely not intended!

[Damiano Testa]

The reason it continues is probably this line

https://github.com/leanprover-community/mathlib4/blob/master/.github%2Fworkflows%2Flint_and_suggest_pr.yml#L25

It is probably intended that the linting continues, but there is probably a missing final step that catches all failures.

The reason this step fails, though, is likely that lake is not installed, so a previous CI step in this workflow should make it available.

[Kim Morrison]

@Damiano Testa, would you be able to look into making sure lake is installed there?

[Damiano Testa]

#15250

[Damiano Testa]

As always, CI is very tricky! This step must have never worked: I checked one of my latest PRs and indeed it was failing. It does not fail on the PR linked above.

[Damiano Testa]

It seems that the same battery of tests is also run on CI and after elan/lake is installed, so there were no missed linting, just missed suggestions, I think.

[Damiano Testa]

While we are at it, I also enabled reviewdog to suggest missing imports. I did it in the same PR, since it was just a one -line addition to CI.

[Damiano Testa]

The way in which it works is that the continue-on-error: true step allows the following reviewdog step to apply the suggestions of the previous step. Thus, there is no need to add a later check catching these failures, since reviewdog will comment on the PR.

I added a comment to the continue-on-error: true steps.

[Kim Morrison]

Thanks so much!