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

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

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

Instances For