Lean4
@[inherit_doc Mathlib.Linter.linter.style.missingEnd]
def missingEndLinter : Linter where
run :=
withSetOptionIn fun stx ↦ do
-- Only run this linter at the end of a module.
unless stx.isOfKind ``Lean.Parser.Command.eoi do
return
if getLinterValue linter.style.missingEnd (← getLinterOptions) && !(← MonadState.get).messages.hasErrors then
let sc ← getScopes
if sc.length == 1 then
return
let ends :=
sc.dropLast.map fun s ↦
(s.header, s.isNoncomputable)
-- If the outermost scope corresponds to a `noncomputable section`, we ignore it.
let ends := if ends.getLast!.2 then ends.dropLast else ends
if !ends.isEmpty then
let ending :=
(ends.map Prod.fst).foldl (init := "") fun a b ↦ a ++ s!"\n\nend{(if b == "" then "" else " ")}{b}"
Linter.logLint linter.style.missingEnd stx m! "unclosed sections or namespaces; expected: '{ending}'"
