Lean4
/-- Checks that no command beginning with `#` is present in 'Mathlib',
except for the ones in `allowed_commands`.
If `warningAsError` is `true`, then the linter logs an info (rather than a warning).
This means that CI will eventually fail on `#`-commands, but does not stop it from continuing.
However, in order to avoid local clutter, when `warningAsError` is `false`, the linter
logs a warning only for the `#`-commands that do not already emit a message. -/
def hashCommandLinter : Linter where
run :=
withSetOptionIn' fun stx => do
if
getLinterValue linter.hashCommand (← getLinterOptions) &&
((← get).messages.reportedPlusUnreported.isEmpty || warningAsError.get (← getOptions)) then
if let some sa := stx.getHead? then
let a := sa.getAtomVal
if (a.get ⟨0⟩ == '#' && !allowed_commands.contains a) then
let msg := m! "`#`-commands, such as '{a}', are not allowed in 'Mathlib'"
if warningAsError.get (← getOptions) then
logInfoAt sa (msg ++ " [linter.hashCommand]")
else
Linter.logLint linter.hashCommand sa msg
