lean4-htt/tests/pkg
Anne Baanen e982bf9472
feat: implement "linter sets" that can be turned on as a group (#8106)
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>
2025-05-14 23:30:42 +00:00
..
builtin_attr fix: make sure monad lift coercion elaborator has no side effects (#6024) 2024-11-13 16:22:31 +00:00
debug feat: debug_assert! (#7256) 2025-03-03 16:34:44 +00:00
deriving chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
frontend feat: lake: support plugins (#7001) 2025-02-14 04:57:31 +00:00
initialize fix: missing unboxing in interpreter when loading initialized value (#4512) 2024-06-20 10:06:24 +00:00
linter_set feat: implement "linter sets" that can be turned on as a group (#8106) 2025-05-14 23:30:42 +00:00
misc feat: allow duplicate theorems to be imported 2024-03-13 12:57:41 -07:00
module feat: private import and import all (#8159) 2025-04-30 10:06:54 +00:00
path with spaces fix: calling programs with spaces on Windows (#4515) 2024-07-26 17:35:05 +00:00
prv feat: structure instance notation elaboration improvements (#7717) 2025-03-30 17:40:36 +00:00
setup feat: lean --setup (#8024) 2025-05-03 23:57:37 +00:00
test_extern test: disable flaky test 2025-04-29 17:34:10 +02:00
user_attr chore: upstream Nat material from mathlib (#7971) 2025-04-16 06:55:32 +00:00
user_attr_app feat: importModules without loading environment extensions (#6325) 2025-04-02 08:37:11 +00:00
user_ext chore: disable nondeterministic test 2025-04-24 11:30:26 +02:00
user_opt feat: accept user-defined options on the cmdline (#4741) 2024-08-02 12:24:56 +00:00
user_plugin feat: smarter plugin loading (#7090) 2025-02-18 23:03:52 +00:00
.gitignore chore: ignore forgotten Lake test artifacts 2023-11-17 21:25:41 -05:00