Lean #lint in <Namespace> silently checks nothing; it takes a package name

#lint in Foo expects a package (root module prefix such as Mathlib or your project root), not a namespace. If you pass a namespace like #lint in MyNamespace, it prints 'Found 0 errors in 0 declarations ... All linting checks passed!', which looks like success. Use #lint in MyProject in a scratch file that imports the modules you care about. Always check that the declaration count in the output is nonzero before reporting lint-clean.