feat: don't consider private names autogenerated in isAutoDecl (#1831)

Co-authored-by: Marcelo Lynch <marcelomlynch@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: 3 people

Batteries/Tactic/Lint/Basic.lean

@@ -31,16 +31,15 @@ metadata is stored in the `Linter` structure. We define two attributes:
    the linter with name `linterName`.
 -/
 
--- TODO: do not consider private names autogenerated (batteries#1831)
 /--
 Returns true if `decl` is an automatically generated declaration.
 
-Also returns true if `decl` is an internal name or created during macro
-expansion.
+Also returns true if `decl` is an internal name or created during macro expansion (after stripping
+private mangling; i.e., private names are not necessarily considered autogenerated).
 -/
 def _root_.Lean.Environment.isAutoDecl (env : Environment) (decl : Name) : Bool := Id.run do
-  if decl.hasMacroScopes then return true
-  if decl.isInternal then return true
+  let declUserName := privateToUserName decl
+  if declUserName.hasMacroScopes || declUserName.isInternal then return true
   if isReservedName env decl then return true
   if let Name.str n s := decl then
     if env.isAutoDecl n then return true

Batteries/Tactic/Lint/Misc.lean

@@ -44,6 +44,9 @@ their value, and allow arguments starting with `_` to be unused. -/
       | _ => return none
     if val.hasSorry || ty.hasSorry then return none
     forallTelescope ty fun args ty => do
+      -- Exempt decls generated by `proof_wanted`/`def_wanted` (not imported here),
+      -- which are of the form e.g. `(binders) → ProofWanted P` and have trivial content
+      if ty.isAppOfArity' `ProofWanted 1 || ty.isAppOfArity' `DefWanted 1 then return none
       let mut e := (mkAppN val args).headBeta
       let ldecls ← args.mapM getFVarLocalDecl
       e := mkApp e ty

BatteriesTest/lint_docBlame.lean

@@ -1,15 +1,31 @@
+module
+
 import Batteries.Tactic.Lint
 
 set_option linter.missingDocs false
 
-/-- A docstring is needed here -/
+public section
+
+-- A docstring is needed here
 structure AtLeastThirtySeven where
-  /-- and here -/
+  -- and here
   val : Nat := 1
   -- but not here
   prop : 37 ≤ val
 
--- or here
+-- or here (due to being a theorem)
 theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.prop
 
+def foo_bad := 3 -- Needs a docstring
+private def foo_ok := 7 -- Doesn't (due to being private)
+
+/--
+error: /- The `docBlame` linter reports:
+DEFINITIONS ARE MISSING DOCUMENTATION STRINGS:
+This linter can be disabled with `@[nolint docBlame]`. -/
+#check AtLeastThirtySeven /- inductive missing documentation string -/
+#check AtLeastThirtySeven.val /- definition missing documentation string -/
+#check foo_bad /- definition missing documentation string -/
+-/
+#guard_msgs in
 #lint- only docBlame

BatteriesTest/lint_simpNF_respectTransparency.lean

@@ -36,7 +36,7 @@ private theorem Bundle.of_op {X : Type} [MyClass X] :
     @MyClass.op (Bundle.of X).carrier (Bundle.of X).inst = @MyClass.op X _ := rfl
 
 /--
-error: -- Found 1 error in 0 declarations (plus 31 automatically generated ones) in the current file with 1 linters
+error: -- Found 1 error in 12 declarations (plus 19 automatically generated ones) in the current file with 1 linters
 
 /- The `simpNF` linter reports:
 SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.

BatteriesTest/lintunused.lean

@@ -1,4 +1,9 @@
+module
+
 import Batteries.Tactic.Lint
+import Batteries.Util.ProofWanted
+
+public section
 
 -- should be ignored as the proof contains sorry
 /-- warning: declaration uses `sorry` -/
@@ -33,6 +38,13 @@ theorem foo7_bad [Mul Nat] [inst : Add Nat] {h : 1 = 1} ⦃h' : 0 = 0⦄ : True
 set_option linter.unusedVariables false in
 @[deprecated foo6_ok (since := "today")] theorem foo6_ok' (h : Nat) : True := trivial
 
+-- private theorems are still linted
+private theorem foo8_bad [Mul Nat] : True := trivial
+
+-- `proof_wanted`/`def_wanted` is ignored
+proof_wanted wanted (h : Bool) : True
+def_wanted wanted' (h : Bool) : Bool
+
 /--
 error: /- The `unusedArguments` linter reports:
 UNUSED ARGUMENTS.
@@ -50,6 +62,8 @@ This linter can be disabled with `@[nolint unusedArguments]`. -/
   argument 2: [inst : Add Nat]
   argument 3: {h : 1 = 1}
   argument 4: ⦃h' : 0 = 0⦄ -/
+#check @foo8_bad /- 1 unused argument:
+  argument 1: [Mul Nat] -/
 -/
 #guard_msgs in
 #lint- only unusedArguments