chore: constructorNameAsVariable linter respects linter.all #4966
Conversation
|
Mathlib CI status (docs):
|
|
Hmm, the test file works fine interactively, where |
|
Modulo the test issue, LGTM. I agree about a better structure here, but I'm not sure what it should be - might as well fix the bug in the meantime. Thanks! |
|
I suppose for test purposes, it would work fine to inline the part of |
| @@ -53,7 +58,7 @@ def constructorNameAsVariable : Linter where | |||
| if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return | |||
| let opts := ci.options | |||
| -- we have to check for the option again here because it can be set locally | |||
| if !linter.constructorNameAsVariable.get opts then return | |||
| if !getLinterValue linter.constructorNameAsVariable opts then return | |||
There was a problem hiding this comment.
Any reason you use getLinterConstructorNameAsVariable at the top of the function but inline it here? I'd lean towards not having getLinterConstructorNameAsVariable at all, but if you really want it then it would be good to use consistently.
@eric-wieser discovered while investigating a quote4 issue that
linter.alldoesn't disableconstructorNameAsVariable.This seems like an easy mistake to make when setting up a new linter, and perhaps we need a better structure to make it easy to do the right thing.