feat: `#grind_lint check in module Mathlib` #31866

Stream: PR reviews

[Kim Morrison]

I would like this linting step installed sooner rather than later.

[Chris Henson]

Kim, will this silently fail because #grind_lint only logs errors? Should it have an empty #guard_msgs to make sure it's actually passing?

[Damiano Testa]

Mathlib CI is expected to be completely silent, so emitting a message, whether or not it is an error, should be caught and flagged.

[Damiano Testa]

At the same time, it is also not wrong to be more explicit and add a #guard_msgs, so that a change is flagged as an error.

[Chris Henson]

Ah, thanks. Do you happen to know how that is configured? I didn't see anything in the lakefile, is it on the GitHub actions side? Maybe it should be an option for lean-action to replicate this behavior.

[Damiano Testa]

It is on the GitHub action side. Let me find where exactly.

[Damiano Testa]

(It is a "manual" check, though, not some flag that can be turned on or off.)

[Damiano Testa]

This

https://github.com/leanprover-community/mathlib4/blob/4bb77eb8ab0306647ec206d365aa52a06b316345/.github/build.in.yml#L512

is the check that lake build is silent.

[Chris Henson]

Oh I see, thanks for tracking that down!

[Damiano Testa]

I think that this is the test check:

https://github.com/leanprover-community/mathlib4/blob/4bb77eb8ab0306647ec206d365aa52a06b316345/.github/workflows/build.yml#L494

I forget whether the -iofail flag does what I said, but I am hoping that it does!

[Chris Henson]

Yes, that appears correct, lake --help says:

--iofail      fail build if any I/O or other info is logged (same as --fail-level=info)

[Chris Henson]

(And you can already pass args like this to either lake build or lake test with the GitHub action)

[Damiano Testa]

Ok, great! Mathlib has various stages of the build in CI and only at the very end it should fail. Also, when the CI was setup, these flags and the replay feature were not available, which probably explains a little of the clunkiness.

[Damiano Testa]

Basically, try to build as much as you can, possibly with errors, upload the cache, lint and after that, fail if there were some errors/noise.