2b8c273687
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>
142 lines
2.9 KiB
Text
142 lines
2.9 KiB
Text
import Lean
|
||
|
||
set_option linter.all true
|
||
set_option linter.redundantVisibility false
|
||
|
||
/-- A doc string -/
|
||
def hasDoc (x : Nat) := x
|
||
|
||
def noDoc (x : Nat) := x
|
||
|
||
private def auxDef (x : Nat) := x
|
||
|
||
namespace Foo
|
||
protected def noDoc2 (x : Nat) := x
|
||
end Foo
|
||
|
||
open Foo in
|
||
def openIn (x : Nat) := x
|
||
|
||
open Foo in
|
||
/-- A doc string -/
|
||
def openIn2 (x : Nat) := x
|
||
|
||
set_option pp.all true in
|
||
def setOptionIn1 (x : Nat) := x
|
||
|
||
set_option pp.all true in
|
||
/-- A doc string -/
|
||
def setOptionIn2 (x : Nat) := x
|
||
|
||
set_option linter.all false in
|
||
def nolintAll (x : Nat) := x
|
||
|
||
set_option linter.all true in
|
||
set_option linter.missingDocs false in
|
||
def nolintDoc (x : Nat) := x
|
||
|
||
set_option linter.all false in
|
||
set_option linter.missingDocs true in
|
||
def lintDoc (x : Nat) := x
|
||
|
||
inductive Ind where
|
||
| ind1
|
||
| ind2 : Ind → Ind
|
||
/-- A doc string -/ | doc : Ind
|
||
with
|
||
@[computed_field] field : Ind → Nat
|
||
| _ => 1
|
||
|
||
structure Foo where
|
||
mk1 : Nat
|
||
/-- test -/
|
||
(mk2 mk3 : Nat)
|
||
{mk4 mk5 : Nat}
|
||
[mk6 mk7 : Nat]
|
||
|
||
class Bar (α : Prop) where mk ::
|
||
(foo bar := 1)
|
||
|
||
class Bar2 (α : Prop) where
|
||
bar := 2
|
||
|
||
class Bar3 (α : Prop) extends Bar α where
|
||
bar := 3
|
||
(foo baz := 3)
|
||
|
||
theorem aThm : True := trivial
|
||
example : True := trivial
|
||
instance : Bar True := {}
|
||
|
||
initialize init : Unit ← return
|
||
initialize return
|
||
|
||
declare_syntax_cat myCat
|
||
|
||
syntax "my_syn" : myCat
|
||
syntax (name := namedSyn) "my_named_syn" myCat : command
|
||
infixl:20 "<my_infix>" => Nat.add
|
||
infixr:20 (name := namedInfix) "<my_named_infix>" => Nat.add
|
||
notation:20 "my_notation" x y => Nat.add x y
|
||
notation:20 (name := namedNota) "my_named_notation" x y => Nat.add x y
|
||
|
||
macro_rules | `(my_named_syn my_syn) => `(def hygienic := 1)
|
||
elab_rules : command | `(my_named_syn my_syn) => return
|
||
|
||
my_named_syn my_syn
|
||
|
||
elab "my_elab" : term => return Lean.mkConst ``false
|
||
macro "my_macro" : term => `(my_elab)
|
||
|
||
class abbrev BarAbbrev (α : Prop) := Bar α
|
||
|
||
register_option myOption : Bool := { defValue := my_macro, descr := "hi mom" }
|
||
|
||
elab (name := myCmd) (docComment)? "my_command" ident : command => pure ()
|
||
|
||
my_command x
|
||
|
||
open Lean.Linter.MissingDocs in
|
||
@[missing_docs_handler myCmd]
|
||
def handleMyCmd : SimpleHandler := fun
|
||
| `(my_command $x:ident) => lintNamed x "my_command"
|
||
| _ => pure ()
|
||
|
||
/-- doc -/
|
||
my_command y
|
||
|
||
my_command z
|
||
|
||
-- Test: empty doc strings should be treated as missing
|
||
/---/
|
||
def emptyDoc1 (x : Nat) := x
|
||
|
||
/--
|
||
-/
|
||
def emptyDoc2 (x : Nat) := x
|
||
|
||
/-- -/
|
||
def emptyDoc3 (x : Nat) := x
|
||
|
||
-- Test: empty doc strings on other declaration kinds
|
||
/---/
|
||
inductive EmptyInd where
|
||
/---/ | emptyCtorDoc
|
||
| noCtorDoc
|
||
|
||
/---/
|
||
notation:20 "empty_nota" x y => Nat.add x y
|
||
|
||
/---/
|
||
macro "empty_macro" : term => `(my_elab)
|
||
|
||
/---/
|
||
elab "empty_elab" : term => return Lean.mkConst ``false
|
||
|
||
-- Test: @[inherit_doc] suppresses even with empty doc
|
||
@[inherit_doc hasDoc]
|
||
def inheritedDoc (x : Nat) := x
|
||
|
||
-- Test: Verso doc comments with interpolated content are not empty
|
||
/-- See {name}`hasDoc` for details. -/
|
||
def versoDoc (x : Nat) := x
|