test/Lint.lean failure

Stream: nightly-testing

[Ruben Van de Velde]

Warning: test/Lint.lean:10:4: warning: The namespace 'add' is duplicated in the declaration 'add.add' [linter.dupNamespace]
Warning: test/Lint.lean:19:4: warning: The namespace 'Foo' is duplicated in the declaration 'Foo.Foo.foo' [linter.dupNamespace]

Probably related to the new dupNamespace linted in std?

[Patrick Massot]

It sounds like a fair warning.

[Ruben Van de Velde]

Yeah, it's testing that the existing linter in mathlib does show the warning

[Damiano Testa]

Sorry, I am not at a computer anymore, but I found that putting set_option ... false in set_option ... true in #guard_msgs in ... tends to make #guard_msgs silence the linters. Maybe this changed?

[Mario Carneiro]

this sounds like https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/.23guard_msgs.20doesn't.20silence.20warnings , but it's not a new issue, how are we handling it currently?

[Damiano Testa]

Yes, I suspect it is the same and it was some report of that kind that motivated me to try the double set_option false in set_option true in. I figured that by the time the #guard_msgs issue was resolved, I would remove these workarounds.

[Kim Morrison]

I think the difference here is that Std doesn't check for silent tests, but Mathlib does.

[Kim Morrison]

I've temporarily disabled these two tests on nightly-testing as I really want a green check so I can run the speed center to look at the overall impact of #3807.

[Eric Wieser]

(lean4#3807)