This PR adds a `linter.redundantVisibility` option (default `true`) that
warns
when a visibility modifier has no effect because it matches the default
for the
current context:
- `private` outside a `public section` in a `module` file, where
declarations
are already module-scoped by default
- `public` in a non-`module` file or inside a `public section`, where
declarations are already public by default
The check is integrated directly into `elabModifiers` so it covers all
declaration types uniformly.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR extends the `missingDocs` linter to detect and warn about empty
doc strings (e.g. `/---/` or `/-- -/`), in addition to missing doc
strings. Previously, an empty doc comment would silence the linter even
though it provides no documentation value. Now empty doc strings produce
a distinct "empty doc string for ..." warning, while `@[inherit_doc]`
still suppresses warnings as before.
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.
For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
2026-02-25 13:51:53 +00:00
Renamed from tests/lean/linterMissingDocs.lean (Browse further)
