#-command linter

The #-command linter produces a warning when a command starting with # is used and

• either the command emits no message;
• or warningAsError is set to true.

The rationale behind this is that #-commands are intended to be transient: they provide useful information in development, but are not intended to be present in final code. Most of them are noisy and get picked up anyway by CI, but even the quiet ones are not expected to outlive their in-development status.

opaque Mathlib.Linter.linter.hashCommand : Lean.Option Bool

The linter emits a warning on any command beginning with # that itself emits no message. For example, #guard true and #check_tactic True ~> True by skip trigger a message. There is a list of silent #-command that are allowed.