feat: implement "linter sets" that can be turned on as a group#8106
feat: implement "linter sets" that can be turned on as a group#8106
Conversation
|
Mathlib CI status (docs):
|
grunweg
left a comment
There was a problem hiding this comment.
Looks very nice and mostly straightforward. At first, I was confused about what happens when disabling linter sets again; I wonder if this can be clarified.
grunweg
left a comment
There was a problem hiding this comment.
Thanks, just two small comments and one reply.
| declName := ref | ||
| defValue := false | ||
| group := "linterSet" | ||
| descr := "" |
There was a problem hiding this comment.
(I have no idea if this should also be populated.)
There was a problem hiding this comment.
I copied this from a few other registerOption calls, not sure what descr should be set to otherwise.
|
|
||
| open Lean.Elab.Command in | ||
| /-- Declare a new linter set by giving the set of options that will be enabled along with the set. -/ | ||
| elab doc?:(docComment)? "register_linter_set" name:ident " := " decl:ident* : command => do |
There was a problem hiding this comment.
What do you think of a command like #show_linter_sets that prints out which are the registered linter sets, maybe with "foldable" entries, so that you see the name of each registered linter set, the value of the option and you can click on it to see which options it contains?
There was a problem hiding this comment.
(I think this is a great idea, by the way.)
There was a problem hiding this comment.
It is a great suggestion! It sounds quite complicated though and I'm not familiar how to do fancy trace messages with the unfolding, so I propose to leave this to future work.
| structure LinterOptions where | ||
| toOptions : Options | ||
| linterSets : LinterSets |
There was a problem hiding this comment.
Why are you effectively extending Options? Just handle this in parallel, no?
There was a problem hiding this comment.
I've added a comment to this definition, does that help?
|
Thanks, this looks good. Please ping me once you have Batteries/Mathlib updated. |
This PR adds a `register_linter_set` command for declaring linter sets. The `getLinterValue` function now checks if the present linter is contained in a set that has been enabled (using the `set_option` command or on the command line). The implementation stores linter set membership in an environment extension. As a consequence, we need to pass more data to `getLinterValue`: the argument of ype `Options` has been replaced with a `LinterOptions`, which you can access by writing `getLinterOptions` instead of `getOptions`. (The alternative I considered is to modify the `Options` structure. The current approach seems a bit higher-level and lower-impact.) The logic for checking whether a linter should be enabled now goes in four steps: 1. If the linter has been explicitly en/disabled, return that. 2. If `linter.all` has been explicitly set, return that. 3. If the linter is in any set that has been enabled, return true. 4. Return the default setting for the linter. Reasoning: * The linter's explicit setting should take precedence. * We want to be able to disable all but the explicitly enabled linters with `linter.all`, so it should take precedence over linter sets. * We want to progressively enable more linters as they become available, so the check over sets should be *any*. * Falling back to the default value last, ensures compatibility with the current way we define linters. The public-facing API currently does not allow modifying sets: all linters have to be added when the set is declared. This way, there is one place where all the contents of the set are listed. Linter sets can be declared to contain linters that have not been declared (yet): this allows declaring linter sets low down in the import hierarchy when not all the requested linters are defined yet.
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
90149bb to
9f06107
Compare
#24924) …y default Use the new feature added in leanprover/lean4#8106. Co-authored-by: grunweg <rothgami@math.hu-berlin.de> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
#24924) …y default Use the new feature added in leanprover/lean4#8106. Co-authored-by: grunweg <rothgami@math.hu-berlin.de> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
#24924) …y default Use the new feature added in leanprover/lean4#8106. Co-authored-by: grunweg <rothgami@math.hu-berlin.de> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
leanprover-community#24924) …y default Use the new feature added in leanprover/lean4#8106. Co-authored-by: grunweg <rothgami@math.hu-berlin.de> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
This PR adds a
register_linter_setcommand for declaring linter sets. ThegetLinterValuefunction now checks if the present linter is contained in a set that has been enabled (using theset_optioncommand or on the command line).The implementation stores linter set membership in an environment extension. As a consequence, we need to pass more data to
getLinterValue: the argument of ypeOptionshas been replaced with aLinterOptions, which you can access by writinggetLinterOptionsinstead ofgetOptions. (The alternative I considered is to modify theOptionsstructure. The current approach seems a bit higher-level and lower-impact.)The logic for checking whether a linter should be enabled now goes in four steps:
linter.allhas been explicitly set, return that.Reasoning:
linter.all, so it should take precedence over linter sets.The public-facing API currently does not allow modifying sets: all linters have to be added when the set is declared. This way, there is one place where all the contents of the set are listed.
Linter sets can be declared to contain linters that have not been declared (yet): this allows declaring linter sets low down in the import hierarchy when not all the requested linters are defined yet.