Error message about noisy commands

Stream: mathlib4

[Michael Rothgang]

A recent CI run of #35122 failed because of a stray #check command: so far, so good. However, the error message is pretty inscrutable... I don't see it explaining the problem at all. (This error happened to a student of mine, who is new to mathlib. Expected them to understand and fix this is... tough.)

We used to have nice errors for noisy lines: can we get this check back? (Didn't we have a linter for noisy commands, for example?)

[Thomas Murrills]

There's the hashCommand linter, at least, which should have caught this...I see it checks for warningAsError to be true as a proxy for being in CI? Did CI change which options it takes at some point, perhaps?

[Damiano Testa]

If I remember correctly, the hashCommand linter only emits a warning if the command itself does not. In the case of #check, then hashCommand linter should say nothing, since #check is already being noisy.

[Thomas Murrills]

Looking at the current logic, it seems to emit a warning if the original command is silent or warningAsError is true, and there are a couple of comments nearby about logging during CI; it seems that warningAsError is being used as a proxy for activating the linter even on noisy commands during CI, but this isn’t explicit… :thinking:

[Thomas Murrills]

Though, if that is the goal, I wonder if we should instead either be checking an environment variable for being in CI, or checking Elab.inServer (so that behavior is the same in local lake builds, but doesn’t clutter your infoview while editing)