Commit 2025-05-19 09:39 19337f2b

feat(scripts/lint-style): select linters with Lakefile options (#24953) This PR modifies the lint-style script to enable or disable specific linters by specifying them with Lean options, just like the other style linters. Linters can be selected by setting the corresponding option in the lakefile of the project. (Since we don't actually run any of the code in the project to be linted, set_option calls will be ignored.) More precisely, we use Lake to parse the Lean options from the root project and any default libs and executables. This should correspond to the most common way linter options are set, project-wide. This PR uses a single option to enable/disable all of the Python-based linters. Passing options to the Python program could also work, but sounds like a lot of work for something we want to get rid of in the longer term. Testing routine for this PR:

touch scripts/undocumented.lean
lake exe lint-style -- Receive style linter error
$EDITOR lakefile.lean -- Remove the line ⟨`linter.allScriptsDocumented, true⟩,
lake exe lint-style -- See that the style linter error is gone.