[Tracking PR] feat: rewrite most style linters in Lean

.github/workflows/bors.yml

@@ -166,6 +166,10 @@ jobs:
           lean --version
           lake --version
 
+      - name: run text-based style linters in Lean
+        run: |
+          lake exe lint_style
+
       - name: build cache
         run: |
           lake build cache

.github/workflows/build.yml

@@ -173,6 +173,10 @@ jobs:
           lean --version
           lake --version
 
+      - name: run text-based style linters in Lean
+        run: |
+          lake exe lint_style
+
       - name: build cache
         run: |
           lake build cache

.github/workflows/build.yml.in

@@ -152,6 +152,10 @@ jobs:
           lean --version
           lake --version
 
+      - name: run text-based style linters in Lean
+        run: |
+          lake exe lint_style
+
       - name: build cache
         run: |
           lake build cache

.github/workflows/build_fork.yml

@@ -170,6 +170,10 @@ jobs:
           lean --version
           lake --version
 
+      - name: run text-based style linters in Lean
+        run: |
+          lake exe lint_style
+
       - name: build cache
         run: |
           lake build cache

Mathlib.lean

@@ -3787,6 +3787,7 @@ import Mathlib.Tactic.Linter
 import Mathlib.Tactic.Linter.AttributeInstanceIn
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Lint
+import Mathlib.Tactic.Linter.TextBased
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp
@@ -3860,6 +3861,7 @@ import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SlimCheck
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Spread
+import Mathlib.Tactic.StyleLinters
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Tactic.SudoSetOption

Mathlib/Data/QPF/Multivariate/Basic.lean

@@ -72,7 +72,8 @@ each proves that some operations on functors preserves the QPF structure
 
 ## Reference
 
-! * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
+* [Jeremy Avigad, Mario M. Carneiro and Simon Hudon,
+   *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/
 
 

Mathlib/Tactic.lean

@@ -115,6 +115,7 @@ import Mathlib.Tactic.Linter
 import Mathlib.Tactic.Linter.AttributeInstanceIn
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Lint
+import Mathlib.Tactic.Linter.TextBased
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp
@@ -188,6 +189,7 @@ import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SlimCheck
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Spread
+import Mathlib.Tactic.StyleLinters
 import Mathlib.Tactic.Substs
 import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Tactic.SudoSetOption

Mathlib/Tactic/StyleLinters.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Rothgang
+-/
+
+import Lean.Elab.Command
+import Lean.Linter.Util
+import Batteries.Data.String.Basic
+
+/-!
+## Style linters
+
+Linters which are purely about stylistic things: ported from the `lint-style.py` script.
+-/
+
+open Lean Elab Command
+
+namespace Mathlib.Linter.Style.SetOption
+
+/-- Whether a syntax element is a `set_option` call:
+Return the name of the option being set, if any. -/
+def parse_set_option : Syntax → Option (Ident)
+  -- This handles all four cases: string, number, true and false
+  | `(command|set_option $name:ident $_val) => some name
+  | `(set_option $name:ident $_val in $_x) => some name
+  | `(tactic|set_option $name:ident $_val in $_x) => some name
+  | _ => none
+
+/-- Whether a given piece of syntax is a `set_option` command, tactic or term. -/
+def is_set_option : Syntax → Bool :=
+  fun stx ↦ parse_set_option stx matches some _name
+
+/-- The `setOption` linter emits a warning on a `set_option ...`. -/
+register_option linter.setOption : Bool := {
+  defValue := true
+  descr := "enable the `setOption` linter"
+}
+
+/-- Gets the value of the `linter.setOption` option. -/
+def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.setOption o
+
+/-- The `setOption` linter: this lints any `set_option` command, term or tactic
+which sets a `pp`, `profiler` or `trace` option.
+
+**Why is this bad?** These options are good for debugging, but should not be
+used in production code.
+-/
+def setOptionLinter : Linter where
+  run := withSetOptionIn fun stx => do
+    unless getLinterHash (← getOptions) do
+      return
+    if (← MonadState.get).messages.hasErrors then
+      return
+    match stx.findStack? (fun _ ↦ true) is_set_option with
+    | some ((head, _n)::_chain) =>
+      match parse_set_option head with
+      | some (name) =>
+        -- Drop a leading `
+        let name := (toString name).drop 1
+        if name.startsWith "pp." || name.startsWith "profiler." || name.startsWith "trace." then
+          Linter.logLint linter.setOption head m!"Forbidden set_option `{name}`; please remove"
+      | _ => return
+    | _ => return
+
+initialize addLinter setOptionLinter
+
+end Mathlib.Linter.Style.SetOption

lakefile.lean

@@ -61,6 +61,14 @@ lean_exe shake where
   root := `Shake.Main
   supportInterpreter := true
 
+/-- `lake exe lint_style` runs text-based style lints. -/
+lean_exe lint_style where
+  root := `Mathlib.Tactic.Linter.TextBased
+
+/-- `lake exe update_style_exceptions` update the style exceptions file. -/
+lean_exe update_style_exceptions where
+  srcDir := "scripts"
+
 /--
 `lake exe pole` queries the Mathlib speedcenter for build times for the current commit,
 and then calculates the longest pole