[Merged by Bors] - feat: rewrite set_option style linter in lean#12928
[Merged by Bors] - feat: rewrite set_option style linter in lean#12928
Conversation
|
Actually, this PR is blocked on #11807 (and adapting it accordingly). |
78843a8 to
0829a34
Compare
b9f8379 to
b683b75
Compare
|
|
0c2aeec to
5649950
Compare
Unlike the Python version, this script also supports set_option tactics and terms.
…e option could be simply removed.
5649950 to
5017c0c
Compare
Mathlib/Tactic/Linter/Style.lean
Outdated
| return | ||
| if (← MonadState.get).messages.hasErrors then | ||
| return | ||
| match stx.findStack? (fun _ ↦ true) is_set_option with |
There was a problem hiding this comment.
It seems like findStack? isn't an ideal API for this use case. I would think Syntax should provide a function like find? (root : Syntax) (needle : Syntax → Option β) : Option β or List β. This would avoid having to parse_set_option twice. Overall, probably not worth bothering with unless this pattern comes up a lot when linting.
There was a problem hiding this comment.
Good point. I've switched to Syntax.find? now - this is not quite the API you described, but closer (and more concise also). It still requires parsing the set_option call twice, but if there are no errors, this hopefully doesn't matter.
|
I could see a case for generalizing this: the list of disallowed options should be customizable/extensible by downstream projects. But, future work. Thanks! bors merge |
Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.
|
Pull request successfully merged into master. Build succeeded: |
|
Thanks for the review! |
Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.
Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.
Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.
Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.
Mentored by @digama0; thanks for all your help. Written at the HIM school on formalization of mathematics.