damiano
damiano
Michael, thanks for reviewing! I had intended this PR as an experiment for the "generic" framework and I thought that `cdot` was a good candidate, since it is just a...
Maybe we could have something like `set_option no_lint "cdot"` to selectively disable `cdot`. I think that `String`s can be supported. The implementation of the linter would need to handle these...
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...
@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...
I [asked on Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311019.3A.20a.20syntax.20linter.20for.20.23-commands) 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...
@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 ......
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...
Ok, after yet another failed test, I decided to make the `#guard`s not allowed, except in `test` other than `test.HashCommandLinter`. I hope that this time the tests pass!
I also think that "import" requirements are quite project-specific. Even this tool is not just "import all files and/or all libraries": * `Cache` is not created; * `Mathlib/Tactic` should also...