Zulip Chat Archive

Stream: mathlib4

Topic: where did the noisy linter go?

Mario Carneiro (Dec 18 2022 at 19:12):

I don't think this was literally part of the linter

Kevin Buzzard (Dec 18 2022 at 19:13):

I see -- so what you're saying is that I actually mean "please can we have CI for mathlib4 report noisy files"?

Mario Carneiro (Dec 18 2022 at 19:14):

can you link a mathlib CI run that fails because a file was noisy?

Mario Carneiro (Dec 18 2022 at 19:15):

ah, I found the relevant code: https://github.com/leanprover-community/mathlib/blob/master/scripts/detect_errors.py#L26-L47

Mario Carneiro (Dec 18 2022 at 19:21):

Making code exactly like this looks difficult because the python script is a postprocessor on an invocation of lean --json. We would need to modify lake to also produce json output to do something similar

Notification Bot (Dec 18 2022 at 19:23):

This topic was moved here from #std4 > where did the noisy linter go? by Mario Carneiro.

Kevin Buzzard (Dec 18 2022 at 20:07):

This is low priority, I was just surprised to see a #check in a mathlib4 PR I was reviewing.

Last updated: Dec 20 2023 at 11:08 UTC