feat: add missingDocs linter

src/Init/Meta.lean

@@ -1258,14 +1258,14 @@ macro "erw " s:rwRuleSeq loc:(location)? : tactic =>
 syntax simpAllKind := atomic("(" &"all") " := " &"true" ")"
 syntax dsimpKind   := atomic("(" &"dsimp") " := " &"true" ")"
 
-macro "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?) tacName:ident tacToken:str updateCfg:term : command => do
+macro (name := declareSimpLikeTactic) doc?:(docComment)? "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?) tacName:ident tacToken:str updateCfg:term : command => do
   let (kind, tkn, stx) ←
     if opt.raw.isNone then
-      pure (← `(``simp), ← `("simp "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``simp), ← `("simp "), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
     else if opt.raw[0].getKind == ``simpAllKind then
-      pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
+      pure (← `(``simpAll), ← `("simp_all "), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
     else
-      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``dsimp), ← `("dsimp "), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
   `($stx:command
     @[macro $tacName] def expandSimp : Macro := fun s => do
       let c ← match s[1][0] with

src/Init/NotationExtra.lean

@@ -218,7 +218,8 @@ macro_rules
   attribute [instance] C.mk
   ```
 -/
-syntax declModifiers "class " "abbrev " declId bracketedBinder* (":" term)?
+syntax (name := Lean.Parser.Command.classAbbrev)
+  declModifiers "class " "abbrev " declId bracketedBinder* (":" term)?
   ":=" withPosition(group(colGe term ","?)*) : command
 
 macro_rules

src/Lean/Data/Options.lean

@@ -146,10 +146,10 @@ protected def register [KVMap.Value α] (name : Name) (decl : Lean.Option.Decl 
   registerOption name { defValue := KVMap.Value.toDataValue decl.defValue, group := decl.group, descr := decl.descr }
   return { name := name, defValue := decl.defValue }
 
-macro doc?:(docComment)? "register_builtin_option" name:ident " : " type:term " := " decl:term : command =>
+macro (name := registerBuiltinOption) doc?:(docComment)? "register_builtin_option" name:ident " : " type:term " := " decl:term : command =>
   `($[$doc?]? builtin_initialize $name : Lean.Option $type ← Lean.Option.register $(quote name.getId) $decl)
 
-macro doc?:(docComment)? "register_option" name:ident " : " type:term " := " decl:term : command =>
+macro (name := registerOption) doc?:(docComment)? "register_option" name:ident " : " type:term " := " decl:term : command =>
   `($[$doc?]? initialize $name : Lean.Option $type ← Lean.Option.register $(quote name.getId) $decl)
 
 end Option

src/Lean/Elab/Tactic/Config.lean

@@ -9,7 +9,7 @@ import Lean.Elab.SyntheticMVars
 
 namespace Lean.Elab.Tactic
 open Meta
-macro doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command =>
+macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ident type:ident : command =>
  `(unsafe def evalUnsafe (e : Expr) : TermElabM $type :=
     Meta.evalExpr' (safety := .unsafe) $type ``$type e
    @[implementedBy evalUnsafe] opaque eval (e : Expr) : TermElabM $type

src/Lean/Linter.lean

@@ -1,3 +1,4 @@
 import Lean.Linter.Util
 import Lean.Linter.Builtin
 import Lean.Linter.UnusedVariables
+import Lean.Linter.MissingDocs

src/Lean/Linter/Builtin.lean

@@ -7,7 +7,7 @@ register_builtin_option linter.suspiciousUnexpanderPatterns : Bool := {
   descr := "enable the 'suspicious unexpander patterns' linter"
 }
 
-def getLinterSuspiciousUnexpanderPatterns (o : Options) : Bool := o.get linter.suspiciousUnexpanderPatterns.name (getLinterAll o)
+def getLinterSuspiciousUnexpanderPatterns (o : Options) : Bool := getLinterValue linter.suspiciousUnexpanderPatterns o
 
 def suspiciousUnexpanderPatterns : Linter := fun cmdStx => do
   unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do

src/Lean/Linter/MissingDocs.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Mario Carneiro
+-/
+import Lean.Elab.Command
+import Lean.Elab.Tactic.Config
+import Lean.Linter.Util
+
+namespace Lean.Linter
+open Elab.Command Parser.Command
+open Parser.Term hiding «set_option»
+
+register_builtin_option linter.missingDocs : Bool := {
+  defValue := false
+  descr := "enable the 'missing documentation' linter"
+}
+
+def getLinterMissingDocs (o : Options) : Bool := getLinterValue linter.missingDocs o
+
+partial def missingDocs : Linter := fun stx => do
+  go (getLinterMissingDocs (← getOptions)) stx
+where
+  lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
+    logWarningAt stx s!"missing doc string for {msg} [linter.missingDocs]"
+
+  lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
+    lint stx s!"{msg} {stx.getId}"
+
+  lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
+    lint stx s!"{msg} {parent.getId}.{stx.getId}"
+
+  go (enabled : Bool) : Syntax → CommandElabM Unit
+  | stx@(Syntax.node _ k args) => do
+    match k with
+    | ``«in» =>
+      if stx[0].getKind == ``«set_option» then
+        let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
+        withScope (fun scope => { scope with opts }) do
+          go (getLinterMissingDocs opts) stx[2]
+      else
+        go enabled stx[2]
+      return
+    | ``«mutual» =>
+      args[1]!.getArgs.forM (go enabled)
+      return
+    | _ => unless enabled do return
+    match k with
+    | ``declaration =>
+      let #[head, rest] := args | return
+      if head[2][0].getKind == ``«private» then return -- not private
+      if head[0].isNone then -- no doc string
+        match rest.getKind with
+        | ``«abbrev» => lintNamed rest[1][0] s!"public abbrev"
+        | ``«def» => lintNamed rest[1][0] "public def"
+        | ``«opaque» => lintNamed rest[1][0] "public opaque"
+        | ``«axiom» => lintNamed rest[1][0] "public axiom"
+        | ``«inductive» => lintNamed rest[1][0] "public inductive"
+        | ``classInductive => lintNamed rest[1][0] "public inductive"
+        | ``«structure» => lintNamed rest[1][0] "public structure"
+        | _ => pure ()
+      if rest.getKind matches ``«inductive» | ``classInductive then
+        for stx in rest[4].getArgs do
+          let head := stx[1]
+          if head[2][0].getKind != ``«private» && head[0].isNone then
+            lintField rest[1][0] stx[2] "public constructor"
+        unless rest[5].isNone do
+          for stx in rest[5][0][1].getArgs do
+            let head := stx[0]
+            if head[2][0].getKind == ``«private» then return -- not private
+            if head[0].isNone then -- no doc string
+              lintField rest[1][0] stx[1] "computed field"
+      else if rest.getKind == ``«structure» then
+        unless rest[5].isNone || rest[5][2].isNone do
+          for stx in rest[5][2][0].getArgs do
+            let head := stx[0]
+            if head[2][0].getKind != ``«private» && head[0].isNone then
+              if stx.getKind == ``structSimpleBinder then
+                lintField rest[1][0] stx[1] "public field"
+              else
+                for stx in stx[2].getArgs do
+                  lintField rest[1][0] stx "public field"
+    | ``«initialize» =>
+      let #[head, _, rest, _] := args | return
+      if rest.isNone then return
+      if head[2][0].getKind != ``«private» && head[0].isNone then
+        lintNamed rest[0] "initializer"
+    | ``«syntax» =>
+      if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+        if stx[5].isNone then lint stx[3] "syntax"
+        else lintNamed stx[5][0][3] "syntax"
+    | ``syntaxAbbrev =>
+      if stx[0].isNone then
+        lintNamed stx[2] "syntax"
+    | ``syntaxCat =>
+      if stx[0].isNone then
+        lintNamed stx[2] "syntax category"
+    | ``«macro» =>
+      if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
+        if stx[4].isNone then lint stx[2] "macro"
+        else lintNamed stx[4][0][3] "macro"
+    | ``«elab» =>
+      if stx[0].isNone && stx[1][0][0].getKind != ``«local» then
+        if stx[4].isNone then lint stx[2] "elab"
+        else lintNamed stx[4][0][3] "elab"
+    | ``classAbbrev =>
+      let head := stx[0]
+      if head[2][0].getKind != ``«private» && head[0].isNone then
+        lintNamed stx[3] "class abbrev"
+    | ``Parser.Tactic.declareSimpLikeTactic =>
+      if stx[0].isNone then
+        lintNamed stx[3] "simp-like tactic"
+    | ``Option.registerBuiltinOption =>
+      if stx[0].isNone then
+        lintNamed stx[2] "option"
+    | ``Option.registerOption =>
+      if stx[0].isNone then
+        lintNamed stx[2] "option"
+    | ``registerSimpAttr =>
+      if stx[0].isNone then
+        lintNamed stx[2] "simp attr"
+    | ``Elab.Tactic.configElab =>
+      if stx[0].isNone then
+        lintNamed stx[2] "config elab"
+    | _ => return
+  | _ => return
+
+builtin_initialize addLinter missingDocs

src/Lean/Linter/UnusedVariables.lean

@@ -21,7 +21,7 @@ register_builtin_option linter.unusedVariables.patternVars : Bool := {
   descr := "enable the 'unused variables' linter to mark unused pattern variables"
 }
 
-def getLinterUnusedVariables (o : Options) : Bool := o.get linter.unusedVariables.name (getLinterAll o)
+def getLinterUnusedVariables (o : Options) : Bool := getLinterValue linter.unusedVariables o
 def getLinterUnusedVariablesFunArgs (o : Options) : Bool := o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
 def getLinterUnusedVariablesPatternVars (o : Options) : Bool := o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
 

src/Lean/Linter/Util.lean

@@ -5,11 +5,13 @@ import Lean.Server.InfoUtils
 namespace Lean.Linter
 
 register_builtin_option linter.all : Bool := {
-  defValue := true,
+  defValue := false
   descr := "enable all linters"
 }
 
-def getLinterAll (o : Options) : Bool := o.get linter.all.name linter.all.defValue
+def getLinterAll (o : Options) (defValue := linter.all.defValue) : Bool := o.get linter.all.name defValue
+
+def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.name (getLinterAll o opt.defValue)
 
 open Lean.Elab Lean.Elab.Command
 

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -411,7 +411,8 @@ def SimpTheoremsArray.isErased (thmsArray : SimpTheoremsArray) (thmId : Name) :
 def SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName : Name) : Bool :=
   thmsArray.any fun thms => thms.isDeclToUnfold declName
 
-macro doc?:(docComment)? "register_simp_attr" id:ident descr:str : command => do
+macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc?:(docComment)?
+  "register_simp_attr" id:ident descr:str : command => do
   let str := id.getId.toString
   let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
   `($[$doc?]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr

tests/lean/linterMissingDocs.lean

@@ -0,0 +1,80 @@
+import Lean
+
+set_option linter.all true
+
+/-- 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
+  @[computedField] field : Ind → Nat
+  | _ => 1
+
+structure Foo where
+  mk1 : Nat
+  /-- test -/
+  (mk2 mk3 : Nat)
+  {mk4 mk5 : Nat}
+  [mk6 mk7 : Nat]
+
+class Bar (α : Prop) := mk ::
+
+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
+
+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" }

tests/lean/linterMissingDocs.lean.expected.out

@@ -0,0 +1,24 @@
+linterMissingDocs.lean:8:4-8:9: warning: missing doc string for public def noDoc [linter.missingDocs]
+linterMissingDocs.lean:13:14-13:20: warning: missing doc string for public def noDoc2 [linter.missingDocs]
+linterMissingDocs.lean:17:4-17:10: warning: missing doc string for public def openIn [linter.missingDocs]
+linterMissingDocs.lean:24:4-24:16: warning: missing doc string for public def setOptionIn1 [linter.missingDocs]
+linterMissingDocs.lean:39:4-39:11: warning: missing doc string for public def lintDoc [linter.missingDocs]
+linterMissingDocs.lean:41:10-41:13: warning: missing doc string for public inductive Ind [linter.missingDocs]
+linterMissingDocs.lean:42:4-42:8: warning: missing doc string for public constructor Ind.ind1 [linter.missingDocs]
+linterMissingDocs.lean:43:4-43:8: warning: missing doc string for public constructor Ind.ind2 [linter.missingDocs]
+linterMissingDocs.lean:46:19-46:24: warning: missing doc string for computed field Ind.field [linter.missingDocs]
+linterMissingDocs.lean:49:10-49:13: warning: missing doc string for public structure Foo [linter.missingDocs]
+linterMissingDocs.lean:50:2-50:5: warning: missing doc string for public field Foo.mk1 [linter.missingDocs]
+linterMissingDocs.lean:53:3-53:6: warning: missing doc string for public field Foo.mk4 [linter.missingDocs]
+linterMissingDocs.lean:53:7-53:10: warning: missing doc string for public field Foo.mk5 [linter.missingDocs]
+linterMissingDocs.lean:54:3-54:6: warning: missing doc string for public field Foo.mk6 [linter.missingDocs]
+linterMissingDocs.lean:54:7-54:10: warning: missing doc string for public field Foo.mk7 [linter.missingDocs]
+linterMissingDocs.lean:56:6-56:9: warning: missing doc string for public structure Bar [linter.missingDocs]
+linterMissingDocs.lean:62:11-62:15: warning: missing doc string for initializer init [linter.missingDocs]
+linterMissingDocs.lean:65:19-65:24: warning: missing doc string for syntax category myCat [linter.missingDocs]
+linterMissingDocs.lean:67:0-67:6: warning: missing doc string for syntax [linter.missingDocs]
+linterMissingDocs.lean:68:16-68:24: warning: missing doc string for syntax namedSyn [linter.missingDocs]
+linterMissingDocs.lean:75:0-75:4: warning: missing doc string for elab [linter.missingDocs]
+linterMissingDocs.lean:76:0-76:5: warning: missing doc string for macro [linter.missingDocs]
+linterMissingDocs.lean:78:13-78:22: warning: missing doc string for class abbrev [anonymous] [linter.missingDocs]
+linterMissingDocs.lean:80:16-80:24: warning: missing doc string for option myOption [linter.missingDocs]

tests/lean/linterUnusedVariables.lean

@@ -1,8 +1,9 @@
 import Lean
 
+set_option linter.missingDocs false
 set_option linter.all true
 
-def explicitelyUsedVariable (x : Nat) : Nat :=
+def explicitlyUsedVariable (x : Nat) : Nat :=
   x
 
 theorem implicitlyUsedVariable : P ∧ Q → Q := by