v4.32.0 のリリースノートより
Environment Linters via Options🔗
#13893 (building on #13852's builtin linter sets) makes environment linters controlled by Lean options (Lean.Option), just like ordinary linters. Each environment linter is tied to a boolean option, so you can 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. Using --lint-only with the same syntax collects information only from the specified linters. Breaking change: the previous lake lint flags --extra, --lint-all, and the builtin_nolint attribute are removed in favour of this option-based control. linter.extra becomes a linter set whose members are the existing extra linters.
v4.32.0 のリリースノートより
Environment Linters via Options🔗
#13893 (building on #13852's builtin linter sets) makes environment linters controlled by Lean options (Lean.Option), just like ordinary linters. Each environment linter is tied to a boolean option, so you can 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. Using --lint-only with the same syntax collects information only from the specified linters. Breaking change: the previous lake lint flags --extra, --lint-all, and the builtin_nolint attribute are removed in favour of this option-based control. linter.extra becomes a linter set whose members are the existing extra linters.