From 8400f359b40c8be683aa572abbbcc319172287ea Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Apr 2026 13:24:22 +0000 Subject: [PATCH] feat: add `linter.redundantExpose` for redundant `@[expose]`/`@[no_expose]` attributes This PR adds a `linter.redundantExpose` option (default `true`) that warns when `@[expose]` or `@[no_expose]` attributes have no effect: - `@[expose]` on `abbrev` (always exposed) or non-Prop `instance` (always exposed) - `@[expose]` on a `def` inside an `@[expose] section` (already exposed by the section) - `@[expose]`/`@[no_expose]` in a non-`module` file (no module system) - `@[no_expose]` on a declaration that wouldn't be exposed by default Co-Authored-By: Claude Opus 4.6 (1M context) --- src/Lean/Elab/MutualDef.lean | 48 +++++++++++++++++++++++ tests/elab/linterRedundantExpose.lean | 56 +++++++++++++++++++++++++++ 2 files changed, 104 insertions(+) create mode 100644 tests/elab/linterRedundantExpose.lean diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 3f6e14799923..aa6498197954 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1184,6 +1184,11 @@ register_builtin_option warn.exposeOnPrivate : Bool := { descr := "warn about uses of `@[expose]` on private declarations" } +register_builtin_option linter.redundantExpose : Bool := { + defValue := true + descr := "warn on redundant `@[expose]`/`@[no_expose]` attributes" +} + def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit := if isExample views then withoutModifyingEnv do @@ -1336,6 +1341,49 @@ where logWarningAt attr.stx m!"Redundant `[expose]` attribute, it is meaningful on public \ definitions only" + if Linter.getLinterValue linter.redundantExpose (← Linter.getLinterOptions) then + let inExposeSection := sc.attrs.any (· matches `(attrInstance| expose)) + for header in headers do + for attr in header.modifiers.attrs do + unless attr.stx.getHeadInfo matches .original .. do continue + if attr.name == `expose then do + if !env.header.isModule then + logWarningAt attr.stx m!"`@[expose]` has no effect outside a `module` file{ + .note m!"This linter can be disabled with \ + `set_option {linter.redundantExpose.name} false`"}" + else if env.isExporting then + if header.kind == .abbrev then + logWarningAt attr.stx m!"`@[expose]` has no effect on `abbrev` declarations; \ + they are always exposed{ + .note m!"This linter can be disabled with \ + `set_option {linter.redundantExpose.name} false`"}" + else if header.kind == .instance && !(← isProp header.type) then + logWarningAt attr.stx m!"`@[expose]` has no effect on data `instance` declarations; \ + they are always exposed{ + .note m!"This linter can be disabled with \ + `set_option {linter.redundantExpose.name} false`"}" + else if header.kind == .def && (!header.modifiers.isMeta || sc.isMeta) && inExposeSection then + logWarningAt attr.stx m!"`@[expose]` has no effect inside an `@[expose] section`{ + .note m!"This linter can be disabled with \ + `set_option {linter.redundantExpose.name} false`"}" + else if attr.name == `no_expose then + if !env.header.isModule then + logWarningAt attr.stx m!"`@[no_expose]` has no effect outside a `module` file{ + .note m!"This linter can be disabled with \ + `set_option {linter.redundantExpose.name} false`"}" + else if env.isExporting then + -- Would the declaration be exposed without `@[no_expose]`? + let wouldBeExposed := + (header.kind == .def && (!header.modifiers.isMeta || sc.isMeta) && inExposeSection) || + header.modifiers.attrs.any (·.name == `expose) || + header.kind == .abbrev || + (header.kind == .instance && !(← isProp header.type)) + if !wouldBeExposed then + logWarningAt attr.stx m!"`@[no_expose]` has no effect; this declaration would not \ + be exposed by default{ + .note m!"This linter can be disabled with \ + `set_option {linter.redundantExpose.name} false`"}" + -- Switch to private scope if... withoutExporting (when := (← headers.allM (fun header => do diff --git a/tests/elab/linterRedundantExpose.lean b/tests/elab/linterRedundantExpose.lean new file mode 100644 index 000000000000..50dcb7135b0f --- /dev/null +++ b/tests/elab/linterRedundantExpose.lean @@ -0,0 +1,56 @@ +module + +set_option linter.all true +set_option linter.missingDocs false + +public section + +-- `@[expose]` on abbrev should warn +/-- +warning: `@[expose]` has no effect on `abbrev` declarations; they are always exposed + +Note: This linter can be disabled with `set_option linter.redundantExpose false` +-/ +#guard_msgs in +@[expose] abbrev myAbbrev := 1 + +-- `@[expose]` on a regular public def should not warn +#guard_msgs in +@[expose] def myDef := 1 + +-- `@[no_expose]` on a regular def outside expose section should warn +/-- +warning: `@[no_expose]` has no effect; this declaration would not be exposed by default + +Note: This linter can be disabled with `set_option linter.redundantExpose false` +-/ +#guard_msgs in +@[no_expose] def myDef3 := 3 + +-- `@[no_expose]` on abbrev should not warn (it overrides auto-expose) +#guard_msgs in +@[no_expose] abbrev myAbbrev2 := 5 + +end + +-- `@[expose]` inside `@[expose] section` on a def should warn +@[expose] public section +/-- +warning: `@[expose]` has no effect inside an `@[expose] section` + +Note: This linter can be disabled with `set_option linter.redundantExpose false` +-/ +#guard_msgs in +@[expose] def myDef2 := 2 + +-- `@[no_expose]` inside `@[expose] section` should not warn (it's meaningful) +#guard_msgs in +@[no_expose] def myDef4 := 4 +end + +-- disabling the linter should suppress warnings +public section +#guard_msgs in +set_option linter.redundantExpose false in +@[expose] abbrev myAbbrev3 := 6 +end