feat: syntax linter for `#`-commands

[adomani]

trafficstars

A Lean-linter implementation of the #-command linter introduced in #10809.

This linter produces a warning whenever a non-whitelisted #-commands is used. The whitelist consists of #align, #align_import, #noalign.

This PR is accompanied by #11028, which places the linter in Tactic.Basic, to make sure that (most of) Mathlib passes the #-command linter.

Zulip discussion

---

[alexjbest]

I like this much more than the sed version!

[adomani]

Thomas, thank you very much for your comments! The new withSetOptionIn' command works great, thanks! I added it and also put some tests in to ensure that it does what it should!

[adomani]

@thorimur I thought that I had written this already somewhere, but maybe it got lost.

I am going to change the behaviour of the linter: it will emit a message if and only if the #-command emits no message.

This means that by leaving it always on, you can still try out a #-command and see its output without clutter from the linter. However, every #-command now emits a message: either because the command itself does, or because the linter does (but not both!). This means that CI will pick up #-commands no matter what.

[thorimur]

Hmm, I'm not totally sure about only linting the silent commands, because it's nice to have an error telling you explicitly what's wrong! But I do like having it show up outside of CI when there are no messages, and it definitely works. (The "noisy stdout" section of build tells you where the noise is happening, right?) I'd like someone else to sign off on that specific choice, since I'm not sure what the best option is there. Also see the comment on the earlier thread. (Sorry, maybe I should have just commented there!)

[adomani]

I asked on Zulip about emitting an extra warning in CI, but I feel like I failed to communicate properly what the issue was.

I also accepted your suggestion of the extra warning when warningAsError is true.

[adomani]

@grunweg I should have fixed all the issues. Since your review, the changes have been to

• allow #adaptation_note and
• fix a syntax bug with handling nested set_option ... in commands.

I also extended the list of tests and went ahead to lint most of mathlib!

[grunweg]

Thanks for the quick response. I was wondering about #guard_msg; good catch! Looking at the past logs, it seems #guard (in test/vec_notation) might also need to be allowed.

From my side, once CI passes, it's ready to be merged. (In particular, given the negligible performance effect.)

[adomani]

Michael, thank you for the reviews!

Re #guard_msgs: I simply silenced it, since it was quick and I do not expect lots of them to show up in Mathlib. Probably a better solution would be to allow them only in test files, but I would leave this discussion for later.

Re #guard: I am happy not allowing it in Mathlib. If I remember correctly, I actually removed some #guards in Mathlib that were picked up by the linter and moved them to test files.

[adomani]

Ok, after yet another failed test, I decided to make the #guards not allowed, except in test other than test.HashCommandLinter. I hope that this time the tests pass!

[grunweg]

Tests pass; I took one last look and pushed a few tiny tweaks. (@adomani Feel free to revert those if you prefer!) I think this lint is ready to go: performance is good, mathlib passes, no bad test changes or anything that looks questionable. Thank you for your work on this, this one took a while - but I'm glad it lands! maintainer merge

(A follow-up PR could remove the sed-based linter this replaces. Imho, this doesn't have to happen in this PR.)

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[grunweg]

Filed #13142 for the follow-up.

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style