Skip to content

feat: implement "linter sets" that can be turned on as a group#8106

Merged
kim-em merged 8 commits intomasterfrom
anne/linterSets
May 15, 2025
Merged

feat: implement "linter sets" that can be turned on as a group#8106
kim-em merged 8 commits intomasterfrom
anne/linterSets

Conversation

@Vierkantor
Copy link
Copy Markdown
Contributor

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.

@Vierkantor Vierkantor added the changelog-language Language features and metaprograms label Apr 25, 2025
@Vierkantor Vierkantor requested a review from digama0 as a code owner April 25, 2025 16:46
@Vierkantor Vierkantor requested a review from kim-em April 25, 2025 16:46
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 25, 2025
@ghost
Copy link
Copy Markdown

ghost commented Apr 25, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2b3daf1dd658a6c7c5fdf63cb19b3a56ae89277 --onto 416e07a68e5d9b884de8af4836497a7cc2414c8f. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-25 17:16:47)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2b3daf1dd658a6c7c5fdf63cb19b3a56ae89277 --onto 747ea853b5936166b59b82d2e3057395544114aa. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-28 15:35:34)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2b3daf1dd658a6c7c5fdf63cb19b3a56ae89277 --onto afab374305fb2327036e4fe1ab799fc8928425b7. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-03 13:37:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2b3daf1dd658a6c7c5fdf63cb19b3a56ae89277 --onto ef603cf37d20dce48eda63f740b83480faedd613. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-05 13:04:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2b3daf1dd658a6c7c5fdf63cb19b3a56ae89277 --onto 836d7b703ac6b6c74892339785c20940e17fcd7f. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-08 11:14:00)
  • 💥 Mathlib branch lean-pr-testing-8106 build failed against this PR. (2025-05-14 11:14:01) View Log
  • 💥 Mathlib branch lean-pr-testing-8106 build failed against this PR. (2025-05-14 12:56:07) View Log
  • ✅ Mathlib branch lean-pr-testing-8106 has successfully built against this PR. (2025-05-14 15:17:19) View Log

Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, just two small comments and one reply.

declName := ref
defValue := false
group := "linterSet"
descr := ""
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(I have no idea if this should also be populated.)

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(I think this is a great idea, by the way.)

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Comment on lines +34 to +44
structure LinterOptions where
toOptions : Options
linterSets : LinterSets
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are you effectively extending Options? Just handle this in parallel, no?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added a comment to this definition, does that help?

@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented May 14, 2025

Thanks, this looks good. Please ping me once you have Batteries/Mathlib updated.

Vierkantor and others added 8 commits May 14, 2025 12:37
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>
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 14, 2025
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 14, 2025
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels May 14, 2025
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label May 14, 2025
@kim-em kim-em added this pull request to the merge queue May 14, 2025
Merged via the queue into master with commit e982bf9 May 15, 2025
27 checks passed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 3, 2025
#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>
joelriou pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 8, 2025
#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>
TOMILO87 pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 8, 2025
#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>
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants