#-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.

def Mathlib.Linter.HashCommandLinter.hashCommandLinter : Lean.Linter

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.

Equations

• One or more equations did not get rendered due to their size.