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:
```bash
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.
```

Author: Vierkantor

Mathlib/Tactic/Linter/TextBased.lean

@@ -32,7 +32,7 @@ or for downstream projects to allow a gradual adoption of this linter.
 An executable running all these linters is defined in `scripts/lint-style.lean`.
 -/
 
-open System
+open Lean.Linter System
 
 namespace Mathlib.Linter.TextBased
 
@@ -195,23 +195,33 @@ return an array of all style errors with line numbers. If possible,
 also return the collection of all lines, changed as needed to fix the linter errors.
 (Such automatic fixes are only possible for some kinds of `StyleError`s.)
 -/
-abbrev TextbasedLinter := Array String → Array (StyleError × ℕ) × (Option (Array String))
+abbrev TextbasedLinter := Lean.Options → Array String →
+  Array (StyleError × ℕ) × (Option (Array String))
 
 /-! Definitions of the actual text-based linters. -/
 section
 
 /-- Lint on any occurrences of the string "Adaptation note:" or variants thereof. -/
-def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do
+register_option linter.adaptationNote : Bool := { defValue := true }
+
+@[inherit_doc linter.adaptationNote]
+def adaptationNoteLinter : TextbasedLinter := fun opts lines ↦ Id.run do
+  unless getLinterValue linter.adaptationNote opts do return (#[], none)
+
   let mut errors := Array.mkEmpty 0
   for h : idx in [:lines.size] do
     -- We make this shorter to catch "Adaptation note", "adaptation note" and a missing colon.
     if lines[idx].containsSubstr "daptation note" then
       errors := errors.push (StyleError.adaptationNote, idx + 1)
   return (errors, none)
 
-
 /-- Lint a collection of input strings if one of them contains trailing whitespace. -/
-def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
+register_option linter.trailingWhitespace : Bool := { defValue := true }
+
+@[inherit_doc linter.trailingWhitespace]
+def trailingWhitespaceLinter : TextbasedLinter := fun opts lines ↦ Id.run do
+  unless getLinterValue linter.trailingWhitespace opts do return (#[], none)
+
   let mut errors := Array.mkEmpty 0
   let mut fixedLines : Vector String lines.size := lines.toVector
   for h : idx in [:lines.size] do
@@ -221,9 +231,13 @@ def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
       fixedLines := fixedLines.set idx line.trimRight
   return (errors, if errors.size > 0 then some fixedLines.toArray else none)
 
-
 /-- Lint a collection of input strings for a semicolon preceded by a space. -/
-def semicolonLinter : TextbasedLinter := fun lines ↦ Id.run do
+register_option linter.whitespaceBeforeSemicolon : Bool := { defValue := true }
+
+@[inherit_doc linter.whitespaceBeforeSemicolon]
+def semicolonLinter : TextbasedLinter := fun opts lines ↦ Id.run do
+  unless getLinterValue linter.whitespaceBeforeSemicolon opts do return (#[], none)
+
   let mut errors := Array.mkEmpty 0
   let mut fixedLines := lines
   for h : idx in [:lines.size] do
@@ -256,7 +270,7 @@ def allLinters : Array TextbasedLinter := #[
 Return a list of all unexpected errors, and, if some errors could be fixed automatically,
 the collection of all lines with every automatic fix applied.
 `exceptions` are any pre-existing style exceptions for this file. -/
-def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
+def lintFile (opts : Lean.Options) (path : FilePath) (exceptions : Array ErrorContext) :
     IO (Array ErrorContext × Option (Array String)) := do
   let mut errors := #[]
   -- Whether any changes were made by auto-fixes.
@@ -280,7 +294,7 @@ def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
   let mut changed := lines
 
   for lint in allLinters do
-    let (err, changes) := lint changed
+    let (err, changes) := lint opts changed
     allOutput := allOutput.append (Array.map (fun (e, n) ↦ #[(ErrorContext.mk e n path)]) err)
     -- TODO: auto-fixes do not take style exceptions into account
     if let some c := changes then
@@ -291,52 +305,65 @@ def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
     (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))
   return (errors, if changes_made then some changed else none)
 
+/-- Enables the old Python-based style linters. -/
+register_option linter.pythonStyle : Bool := { defValue := true }
+
 /-- Lint a collection of modules for style violations.
 Print formatted errors for all unexpected style violations to standard output;
 correct automatically fixable style errors if configured so.
 Return the number of files which had new style errors.
+`opts` contains the options defined in the Lakefile, determining which linters to enable.
 `nolints` is a list of style exceptions to take into account.
 `moduleNames` are the names of all the modules to lint,
 `mode` specifies what kind of output this script should produce,
 `fix` configures whether fixable errors should be corrected in-place. -/
-def lintModules (nolints : Array String) (moduleNames : Array Lean.Name) (style : ErrorFormat)
-    (fix : Bool) : IO UInt32 := do
+def lintModules (opts : Lean.Options) (nolints : Array String) (moduleNames : Array Lean.Name)
+    (style : ErrorFormat) (fix : Bool) : IO UInt32 := do
   let styleExceptions := parseStyleExceptions nolints
   let mut numberErrorFiles : UInt32 := 0
   let mut allUnexpectedErrors := #[]
   for module in moduleNames do
     -- Convert the module name to a file name, then lint that file.
     let path := mkFilePath (module.components.map toString)|>.addExtension "lean"
 
-    let (errors, changed) := ← lintFile path styleExceptions
+    let (errors, changed) := ← lintFile opts path styleExceptions
     if let some c := changed then
       if fix then
         let _ := ← IO.FS.writeFile path ("\n".intercalate c.toList)
     if errors.size > 0 then
       allUnexpectedErrors := allUnexpectedErrors.append errors
       numberErrorFiles := numberErrorFiles + 1
 
-  -- Run the remaining python linters. It is easier to just run on all files.
-  -- If this poses an issue, I can either filter the output
-  -- or wait until lint-style.py is fully rewritten in Lean.
-  let args := if fix then #["--fix"] else #[]
-  let output ← IO.Process.output { cmd := "./scripts/print-style-errors.sh", args := args }
-  if output.exitCode != 0 then
-    numberErrorFiles := numberErrorFiles + 1
-    IO.eprintln s!"error: `print-style-error.sh` exited with code {output.exitCode}"
-    IO.eprint output.stderr
-  else if output.stdout != "" then
-    numberErrorFiles := numberErrorFiles + 1
-    IO.eprint output.stdout
+  -- Passing Lean options to Python files seems like a lot of work for something we want to
+  -- run entirely inside of Lean in the end anyway.
+  -- So for now, we enable/disable all of them with a single switch.
+  if getLinterValue linter.pythonStyle opts then
+    -- Run the remaining python linters. It is easier to just run on all files.
+    -- If this poses an issue, I can either filter the output
+    -- or wait until lint-style.py is fully rewritten in Lean.
+    let args := if fix then #["--fix"] else #[]
+    let output ← IO.Process.output { cmd := "./scripts/print-style-errors.sh", args := args }
+    if output.exitCode != 0 then
+      numberErrorFiles := numberErrorFiles + 1
+      IO.eprintln s!"error: `print-style-error.sh` exited with code {output.exitCode}"
+      IO.eprint output.stderr
+    else if output.stdout != "" then
+      numberErrorFiles := numberErrorFiles + 1
+      IO.eprint output.stdout
   formatErrors allUnexpectedErrors style
   if allUnexpectedErrors.size > 0 then
     IO.eprintln s!"error: found {allUnexpectedErrors.size} new style error(s)"
   return numberErrorFiles
 
+/-- Verify that all modules are named in `UpperCamelCase` -/
+register_option linter.modulesUpperCamelCase : Bool := { defValue := true }
+
 /-- Verifies that all modules in `modules` are named in `UpperCamelCase`
 (except for explicitly discussed exceptions, which are hard-coded here).
 Return the number of modules violating this. -/
-def modulesNotUpperCamelCase (modules : Array Lean.Name) : IO Nat := do
+def modulesNotUpperCamelCase (opts : Lean.Options) (modules : Array Lean.Name) : IO Nat := do
+  unless getLinterValue linter.modulesUpperCamelCase opts do return 0
+
   -- Exceptions to this list should be discussed on zulip!
   let exceptions := [
     `Mathlib.Analysis.CStarAlgebra.lpSpace,

MathlibTest/ModuleCasing.lean

@@ -8,16 +8,19 @@ open Mathlib.Linter.TextBased
 
 /-- Some unit tests for `modulesNotUpperCamelCase` -/
 def testModulesNotUpperCamelCase : IO Unit := do
-  assert!((← modulesNotUpperCamelCase #[]) == 0)
-  assert!((← modulesNotUpperCamelCase #[`Mathlib.Fine]) == 0)
-  assert!((← modulesNotUpperCamelCase #[`Mathlib.AlsoFine_]) == 0)
-  assert!((← modulesNotUpperCamelCase #[`Mathlib.NotFine_.Foo]) == 1)
+  -- Explicitly enable the linter, although it is enabled by default.
+  let opts : Lean.Options := linter.modulesUpperCamelCase.set {} true
 
-  assert!((← modulesNotUpperCamelCase #[`bad_module]) == 1)
-  assert!((← modulesNotUpperCamelCase #[`GoodName, `bad_module, `bad_module]) == 2)
-  assert!((← modulesNotUpperCamelCase #[`Mathlib.BadModule__]) == 1)
-  assert!((← modulesNotUpperCamelCase #[`Mathlib.lowerCase]) == 1)
-  assert!((← modulesNotUpperCamelCase #[`Mathlib.snake_case]) == 1)
+  assert!((← modulesNotUpperCamelCase opts #[]) == 0)
+  assert!((← modulesNotUpperCamelCase opts #[`Mathlib.Fine]) == 0)
+  assert!((← modulesNotUpperCamelCase opts #[`Mathlib.AlsoFine_]) == 0)
+  assert!((← modulesNotUpperCamelCase opts #[`Mathlib.NotFine_.Foo]) == 1)
+
+  assert!((← modulesNotUpperCamelCase opts #[`bad_module]) == 1)
+  assert!((← modulesNotUpperCamelCase opts #[`GoodName, `bad_module, `bad_module]) == 2)
+  assert!((← modulesNotUpperCamelCase opts #[`Mathlib.BadModule__]) == 1)
+  assert!((← modulesNotUpperCamelCase opts #[`Mathlib.lowerCase]) == 1)
+  assert!((← modulesNotUpperCamelCase opts #[`Mathlib.snake_case]) == 1)
 
 /--
 info: error: module name 'Mathlib.NotFine_.Foo' is not in 'UpperCamelCase': it should be 'Mathlib.NotFine.Foo' instead

lakefile.lean

@@ -26,6 +26,8 @@ require "leanprover-community" / "plausible" @ git "main"
 /-- These options are used as `leanOptions`, prefixed by `` `weak``, so that
 `lake build` uses them, as well as `Archive` and `Counterexamples`. -/
 abbrev mathlibOnlyLinters : Array LeanOption := #[
+  ⟨`linter.allScriptsDocumented, true⟩,
+  ⟨`linter.checkInitImports, true⟩,
   -- The `docPrime` linter is disabled: https://github.com/leanprover-community/mathlib4/issues/20560
   ⟨`linter.docPrime, false⟩,
   ⟨`linter.hashCommand, true⟩,
@@ -44,7 +46,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.style.multiGoal, true⟩,
   ⟨`linter.style.openClassical, true⟩,
   ⟨`linter.style.refine, true⟩,
-  ⟨`linter.style.setOption, true⟩
+  ⟨`linter.style.setOption, true⟩,
 ]
 
 /-- These options are passed as `leanOptions` to building mathlib, as well as the
@@ -129,6 +131,9 @@ lean_exe shake where
 /-- `lake exe lint-style` runs text-based style linters. -/
 lean_exe «lint-style» where
   srcDir := "scripts"
+  supportInterpreter := true
+  -- Executables which import `Lake` must set `-lLake`.
+  weakLinkArgs := #["-lLake"]
 
 /--
 `lake exe pole` queries the Mathlib speedcenter for build times for the current commit,

scripts/lint-style.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Rothgang
 -/
 
+import Lake.CLI.Main
 import Lean.Elab.ParseImportsFast
 import Batteries.Data.String.Basic
 import Mathlib.Tactic.Linter.TextBased
@@ -20,7 +21,7 @@ In addition, this checks that
 - every file in `scripts` is documented in its top-level README.
 -/
 
-open Cli Mathlib.Linter.TextBased System.FilePath
+open Cli Lean.Linter Mathlib.Linter.TextBased System.FilePath
 
 /-- Parse all imports in a text file at `path` and return just their names:
 this is just a thin wrapper around `Lean.parseImports'`.
@@ -36,12 +37,57 @@ def explicitImports : Array Lean.Name := #[`Batteries, `Std]
 def eraseExplicitImports (names : Array Lean.Name) : Array Lean.Name :=
   explicitImports.foldl Array.erase names
 
+/-- Get the root package of the Lake workspace we are running in. -/
+def getWorkspaceRoot : IO Lake.Package := do
+  let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
+  let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
+  let some workspace ← Lake.loadWorkspace config |>.toBaseIO
+    | throw <| IO.userError "failed to load Lake workspace"
+  return workspace.root
+
+/-- Convert the options that Lake knows into the option that Lean knows. -/
+def toLeanOptions (opts : Array Lake.LeanOption) : Lean.Options :=
+  opts.foldl (init := Lean.Options.empty) fun opts o =>
+    -- Strip off the `weak.` prefix, like Lean does when parsing command line arguments.
+    if o.name.getRoot == `weak
+    then
+      opts.insert (o.name.replacePrefix `weak Lean.Name.anonymous) o.value.toDataValue
+    else
+      opts.insert o.name o.value.toDataValue
+
+/-- Determine the `Lean.Options` from the Lakefile of the current project.
+
+We have to do this since style linters do not run in the `CoreM`/`CommandElabM` monads,
+and so they do not get access to the options in scope.
+
+Please do not confuse this with the Lean options at the moment that `lint-style` was compiled.
+-/
+def getLakefileLeanOptions : IO Lean.Options := do
+  let root ← getWorkspaceRoot
+  -- Some projects declare options in the root package.
+  let rootOpts := root.leanOptions
+  -- Other projects, like Mathlib, declare options in the targets.
+  -- Here we use the default targets, since that probably contains the modules we'll be linting.
+  let defaultOpts := root.defaultTargets.flatMap fun target ↦
+    if let some lib := root.findLeanLib? target then
+      lib.config.leanOptions
+    else if let some exe := root.findLeanExe? target then
+      exe.config.leanOptions
+    else
+      #[]
+  return toLeanOptions (rootOpts ++ defaultOpts)
+
+/-- Check that `Mathlib.Init` is transitively imported in all of Mathlib -/
+register_option linter.checkInitImports : Bool := { defValue := false }
+
 /-- Check that `Mathlib.Init` is transitively imported in all of Mathlib.
 Moreover, every file imported in `Mathlib.Init` should in turn import the `Header` linter
 (except for the header linter itself, of course).
 Return the number of modules which violated one of these rules.
 -/
-def missingInitImports : IO Nat := do
+def missingInitImports (opts : Lean.Options) : IO Nat := do
+  unless getLinterValue linter.checkInitImports opts do return 0
+
   -- Find any file in the Mathlib directory which does not contain any Mathlib import.
   -- We simply parse `Mathlib.lean`, as CI ensures this file is up to date.
   let allModuleNames := eraseExplicitImports (← findImports "Mathlib.lean")
@@ -82,10 +128,14 @@ def missingInitImports : IO Nat := do
     return missing.size
   return 0
 
+/-- Verify that every file in the `scripts` directory is documented in `scripts/README.md` -/
+register_option linter.allScriptsDocumented : Bool := { defValue := false }
 
 /-- Verifies that every file in the `scripts` directory is documented in `scripts/README.md`.
 Return the number of undocumented scripts. -/
-def undocumentedScripts : IO Nat := do
+def undocumentedScripts (opts : Lean.Options) : IO Nat := do
+  unless getLinterValue linter.allScriptsDocumented opts do return 0
+
   -- Retrieve all scripts (except for the `bench` directory).
   let allScripts ← (walkDir "scripts" fun p ↦ pure (p.components.getD 1 "" != "bench"))
   let allScripts := allScripts.erase ("scripts" / "bench")|>.erase ("scripts" / "README.md")
@@ -105,6 +155,8 @@ def undocumentedScripts : IO Nat := do
 
 /-- Implementation of the `lint-style` command line program. -/
 def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
+  let opts ← getLakefileLeanOptions
+
   let style : ErrorFormat := match args.hasFlag "github" with
     | true => ErrorFormat.github
     | false => ErrorFormat.humanReadable
@@ -124,8 +176,8 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   -- (For syntax linters, such a bug actually occurred in mathlib.)
   -- This script is re-run each time, hence is immune to such issues.
   let nolints ← IO.FS.lines ("scripts" / "nolints-style.txt")
-  let numberErrors := (← lintModules nolints allModuleNames style fix)
-    + (← missingInitImports) + (← undocumentedScripts) + (← modulesNotUpperCamelCase allModuleNames)
+  let numberErrors := (← lintModules opts nolints allModuleNames style fix)
+    + (← missingInitImports opts) + (← undocumentedScripts opts) + (← modulesNotUpperCamelCase opts allModuleNames)
   -- If run with the `--fix` argument, return a zero exit code.
   -- Otherwise, make sure to return an exit code of at most 125,
   -- so this return value can be used further in shell scripts.