linter.missingDocs はドキュメントのない定理を無視する

[Seasawher]

ドキュメントのない定理に警告を出すリンターを自作できるか？

[Seasawher]

これの実装を真似ればOK

Mathlib PR https://github.com/leanprover-community/mathlib4/pull/12869

[Seasawher]

この実装よくわからない

import Lean.Elab.Command
import Lean.Linter.Util

open Lean Elab Command

def thmNoDoc : Syntax → Option (Syntax × Syntax)
  | .node _ ``Lean.Parser.Command.declaration #[
    -- the inner `#[]` detects the absence of a doc-string
    .node _ ``Lean.Parser.Command.declModifiers #[.node _ `null #[], _, _, _, _, _],
    .node _ ``Lean.Parser.Command.theorem #[
      thm@(.atom _ "theorem"),
      .node _ ``Lean.Parser.Command.declId #[id, _],
      _,
      _]
    ] => some (thm, id)
  | _ => none

/-- The `theorem` vs `lemma` linter emits a warning on a `theorem` without a doc-string. -/
register_option linter.thmLemma : Bool := {
  defValue := true
  descr := "enable the `theorem` vs `lemma` linter"
}

/-- Gets the value of the `linter.thmLemma` option. -/
def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.thmLemma o

/-- The main implementation of the `theorem` vs `lemma` linter. -/
def thmLemmaLinter : Linter where
  run := withSetOptionIn fun stx => do
    unless getLinterHash (← getOptions) do
      return
    if (← MonadState.get).messages.hasErrors then
      return
    if let some (thm, id) := thmNoDoc stx then
      Linter.logLint linter.thmLemma thm m!"'theorem' requires a doc-string. \
        Either add one to '{id}' or use 'lemma' instead."

initialize addLinter thmLemmaLinter