feat: control environment linters with Lean.Options

[wkrozowski]

This PR makes environment linters (the declaration-level checks run by lake lint --builtin-lint) controlled by Lean.Options, just like ordinary linters. Each environment linter is tied to a boolean option, so you enable or disable it per declaration with set_option linter.X false in ... and across a lint run with the new lake lint --linters=linter.X,-linter.Y flag. The previous lake lint flags --extra, --lint-all, and --lint-only, and the builtin_nolint attribute, are removed in favour of this option-based control.

Whether a linter applies to a declaration is decided by the value of its controlling option at the time that declaration was elaborated. Lean.addDecl snapshots the resolved value of every registered environment-linter option for each new declaration (also from Elab.MutualDef, where the inner addDecl runs on an async environment) and stores it in an environment extension that lake builtin-lint reads. The @[builtin_env_linter linter.X] attribute now takes the controlling option name, and the registry maps option name to linter declaration. --linters is translated into weak option overrides applied to the lint build. isAutoDecl moves to a new Lean.AutoDecl module so Lean.addDecl can use it.

Builds on #13852 (builtin linter sets); linter.extra becomes a linter set whose members are the existing extra linters.

@claude was used to update the help string in Lake CLI, readapt the tests (that were then manually cleaned) and to write this PR description.

[wkrozowski]

@Kha could you please have a look at this PR? In particular I would like to hear your input about my approach to persisting the state of options associated with environment linters while adding declarations, that are not picked by isAutoDecl. One of the potential pain points I might be getting wrong is asynchronous environments.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cc503a50de7fcc8c3325df6b93647e6a4088f7ee --onto c47a0c7cf035381a2bcdd4cdf2442782eb4a5214. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-29 17:02:02)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cc503a50de7fcc8c3325df6b93647e6a4088f7ee --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-29 17:02:03)