feat: rewrite the linter for spaces before semicolons in Lean (#16532)

A fix about 30 violations which have crept into mathlib in the mean-time.



Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: grunweg

Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

@@ -150,12 +150,12 @@ lemma fac_aux₂ {n : ℕ}
         match t with
         | 0 =>
             have : α.hom ≫ (mkOfSucc 0).op = α₂.hom :=
-              Quiver.Hom.unop_inj (by ext x ; fin_cases x <;> rfl)
+              Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)
             rw [this, h₂, ← congr_fun (s.w β₂) x]
             rfl
         | 1 =>
             have : α.hom ≫ (mkOfSucc 1).op = α₀.hom :=
-              Quiver.Hom.unop_inj (by ext x ; fin_cases x <;> rfl)
+              Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)
             rw [this, h₀, ← congr_fun (s.w β₀) x]
             rfl
       rw [← StructuredArrow.w β₁, FunctorToTypes.map_comp_apply, this, ← s.w β₁]

Mathlib/CategoryTheory/Comma/CardinalArrow.lean

@@ -86,7 +86,7 @@ noncomputable def Arrow.shrinkEquiv (C : Type u) [Category.{v} C] [Small.{w} C]
   toFun := (Shrink.equivalence C).inverse.mapArrow.obj
   invFun := (Shrink.equivalence C).functor.mapArrow.obj
   left_inv _ := Arrow.ext (Equiv.apply_symm_apply _ _)
-      ((Equiv.apply_symm_apply _ _)) (by simp ; rfl)
+      ((Equiv.apply_symm_apply _ _)) (by simp; rfl)
   right_inv _ := Arrow.ext (by simp [Shrink.equivalence])
     (by simp [Shrink.equivalence]) (by simp [Shrink.equivalence])
 

Mathlib/Combinatorics/Quiver/ReflQuiver.lean

@@ -33,7 +33,7 @@ scoped notation "𝟙rq" => ReflQuiver.id  -- type as \b1
 
 @[simp]
 theorem ReflQuiver.homOfEq_id {V : Type*} [ReflQuiver V] {X X' : V} (hX : X = X') :
-    Quiver.homOfEq (𝟙rq X) hX hX = 𝟙rq X' := by subst hX ; rfl
+    Quiver.homOfEq (𝟙rq X) hX hX = 𝟙rq X' := by subst hX; rfl
 
 instance catToReflQuiver {C : Type u} [inst : Category.{v} C] : ReflQuiver.{v+1, u} C :=
   { inst with }

Mathlib/Probability/CondVar.lean

@@ -34,23 +34,23 @@ following conditions is true:
 - `X - μ[X | m]` is not square-integrable. -/
 noncomputable def condVar : Ω → ℝ := μ[(X - μ[X | m]) ^ 2 | m]
 
-@[inherit_doc] scoped notation "Var[" X " ; " μ " | " m "]" => condVar m X μ
+@[inherit_doc] scoped notation "Var[" X "; " μ " | " m "]" => condVar m X μ
 
 /-- Conditional variance of a real-valued random variable. It is defined as `0` if any one of the
 following conditions is true:
 - `m` is not a sub-σ-algebra of `m₀`,
 - `volume` is not σ-finite with respect to `m`,
 - `X - 𝔼[X | m]` is not square-integrable. -/
-scoped notation "Var[" f "|" m "]" => Var[f ; MeasureTheory.volume | m]
+scoped notation "Var[" f "|" m "]" => Var[f; MeasureTheory.volume | m]
 
-lemma condVar_of_not_le (hm : ¬m ≤ m₀) : Var[X ; μ | m] = 0 := by rw [condVar, condExp_of_not_le hm]
+lemma condVar_of_not_le (hm : ¬m ≤ m₀) : Var[X; μ | m] = 0 := by rw [condVar, condExp_of_not_le hm]
 
 lemma condVar_of_not_sigmaFinite (hμm : ¬SigmaFinite (μ.trim hm)) :
-    Var[X ; μ | m] = 0 := by rw [condVar, condExp_of_not_sigmaFinite hm hμm]
+    Var[X; μ | m] = 0 := by rw [condVar, condExp_of_not_sigmaFinite hm hμm]
 
 open scoped Classical in
 lemma condVar_of_sigmaFinite [SigmaFinite (μ.trim hm)] :
-    Var[X ; μ | m] =
+    Var[X; μ | m] =
       if Integrable (fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) μ then
         if StronglyMeasurable[m] (fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) then
           fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2
@@ -59,51 +59,51 @@ lemma condVar_of_sigmaFinite [SigmaFinite (μ.trim hm)] :
 
 lemma condVar_of_stronglyMeasurable [SigmaFinite (μ.trim hm)]
     (hX : StronglyMeasurable[m] X) (hXint : Integrable ((X - μ[X | m]) ^ 2) μ) :
-    Var[X ; μ | m] = fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2 :=
+    Var[X; μ | m] = fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2 :=
   condExp_of_stronglyMeasurable _ ((hX.sub stronglyMeasurable_condExp).pow _) hXint
 
 lemma condVar_of_not_integrable (hXint : ¬ Integrable (fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) μ) :
-    Var[X ; μ | m] = 0 := condExp_of_not_integrable hXint
+    Var[X; μ | m] = 0 := condExp_of_not_integrable hXint
 
-@[simp] lemma condVar_zero : Var[0 ; μ | m] = 0 := by simp [condVar]
+@[simp] lemma condVar_zero : Var[0; μ | m] = 0 := by simp [condVar]
 
 @[simp]
-lemma condVar_const (hm : m ≤ m₀) (c : ℝ) : Var[fun _ ↦ c ; μ | m] = 0 := by
+lemma condVar_const (hm : m ≤ m₀) (c : ℝ) : Var[fun _ ↦ c; μ | m] = 0 := by
   obtain rfl | hc := eq_or_ne c 0
   · simp [← Pi.zero_def]
   by_cases hμm : IsFiniteMeasure μ
   · simp [condVar, hm, Pi.pow_def]
   · simp [condVar, condExp_of_not_integrable, integrable_const_iff_isFiniteMeasure hc,
       integrable_const_iff_isFiniteMeasure <| pow_ne_zero _ hc, hμm, Pi.pow_def]
 
-lemma stronglyMeasurable_condVar : StronglyMeasurable[m] (Var[X ; μ | m]) :=
+lemma stronglyMeasurable_condVar : StronglyMeasurable[m] (Var[X; μ | m]) :=
   stronglyMeasurable_condExp
 
-lemma condVar_congr_ae (h : X =ᵐ[μ] Y) : Var[X ; μ | m] =ᵐ[μ] Var[Y ; μ | m] :=
+lemma condVar_congr_ae (h : X =ᵐ[μ] Y) : Var[X; μ | m] =ᵐ[μ] Var[Y; μ | m] :=
   condExp_congr_ae <| by filter_upwards [h, condExp_congr_ae h] with ω hω hω'; dsimp; rw [hω, hω']
 
 lemma condVar_of_aestronglyMeasurable [hμm : SigmaFinite (μ.trim hm)]
     (hX : AEStronglyMeasurable[m] X μ) (hXint : Integrable ((X - μ[X | m]) ^ 2) μ) :
-    Var[X ; μ | m] =ᵐ[μ] (X - μ[X | m]) ^ 2 :=
+    Var[X; μ | m] =ᵐ[μ] (X - μ[X | m]) ^ 2 :=
   condExp_of_aestronglyMeasurable' _ ((continuous_pow _).comp_aestronglyMeasurable
     (hX.sub stronglyMeasurable_condExp.aestronglyMeasurable)) hXint
 
-lemma integrable_condVar : Integrable Var[X ; μ | m] μ := integrable_condExp
+lemma integrable_condVar : Integrable Var[X; μ | m] μ := integrable_condExp
 
 /-- The integral of the conditional variance `Var[X | m]` over an `m`-measurable set is equal to
 the integral of `(X - μ[X | m]) ^ 2` on that set. -/
 lemma setIntegral_condVar [SigmaFinite (μ.trim hm)] (hX : Integrable ((X - μ[X | m]) ^ 2) μ)
     (hs : MeasurableSet[m] s) :
-    ∫ ω in s, (Var[X ; μ | m]) ω ∂μ = ∫ ω in s, (X ω - (μ[X | m]) ω) ^ 2 ∂μ :=
+    ∫ ω in s, (Var[X; μ | m]) ω ∂μ = ∫ ω in s, (X ω - (μ[X | m]) ω) ^ 2 ∂μ :=
   setIntegral_condExp _ hX hs
 
 -- `(· ^ 2)` is a postfix operator called `_sq` in lemma names, but
 -- `condVar_ae_eq_condExp_sq_sub_condExp_sq` is a bit ridiculous, so we exceptionally denote it by
 -- `sq_` as it were a prefix.
 lemma condVar_ae_eq_condExp_sq_sub_sq_condExp (hm : m ≤ m₀) [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) :
-    Var[X ; μ | m] =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2 := by
+    Var[X; μ | m] =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2 := by
   calc
-    Var[X ; μ | m]
+    Var[X; μ | m]
     _ = μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] := by rw [condVar, sub_sq]
     _ =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 := by
       have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
@@ -122,51 +122,51 @@ lemma condVar_ae_eq_condExp_sq_sub_sq_condExp (hm : m ≤ m₀) [IsFiniteMeasure
     _ = μ[X ^ 2 | m] - μ[X | m] ^ 2 := by ring
 
 lemma condVar_ae_le_condExp_sq (hm : m ≤ m₀) [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) :
-    Var[X ; μ | m] ≤ᵐ[μ] μ[X ^ 2 | m] := by
+    Var[X; μ | m] ≤ᵐ[μ] μ[X ^ 2 | m] := by
   filter_upwards [condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX] with ω hω
   dsimp at hω
   nlinarith
 
 /-- **Law of total variance** -/
 lemma integral_condVar_add_variance_condExp (hm : m ≤ m₀) [IsProbabilityMeasure μ]
-    (hX : Memℒp X 2 μ) : μ[Var[X ; μ | m]] + Var[μ[X | m] ; μ] = Var[X ; μ] := by
+    (hX : Memℒp X 2 μ) : μ[Var[X; μ | m]] + Var[μ[X | m]; μ] = Var[X; μ] := by
   calc
-    μ[Var[X ; μ | m]] + Var[μ[X | m] ; μ]
+    μ[Var[X; μ | m]] + Var[μ[X | m]; μ]
     _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by
       congr 1
       · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
       · exact variance_def' hX.condExp
     _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by
       rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
       exact hX.condExp.integrable_sq
-    _ = Var[X ; μ] := by rw [variance_def' hX]; ring
+    _ = Var[X; μ] := by rw [variance_def' hX]; ring
 
 lemma condVar_bot' [NeZero μ] (X : Ω → ℝ) :
-    Var[X ; μ | ⊥] = fun _ => ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ := by
+    Var[X; μ | ⊥] = fun _ => ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ := by
   ext ω; simp [condVar, condExp_bot', average]
 
 lemma condVar_bot_ae_eq (X : Ω → ℝ) :
-    Var[X ; μ | ⊥] =ᵐ[μ] fun _ ↦ ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ := by
+    Var[X; μ | ⊥] =ᵐ[μ] fun _ ↦ ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ := by
   obtain rfl | hμ := eq_zero_or_neZero μ
   · rw [ae_zero]
     exact eventually_bot
   · exact .of_forall <| congr_fun (condVar_bot' X)
 
 lemma condVar_bot [IsProbabilityMeasure μ] (hX : AEMeasurable X μ) :
-    Var[X ; μ | ⊥] = fun _ω ↦ Var[X ; μ] := by
+    Var[X; μ | ⊥] = fun _ω ↦ Var[X; μ] := by
   simp [condVar_bot', average_eq_integral, variance_eq_integral hX]
 
-lemma condVar_smul (c : ℝ) (X : Ω → ℝ) : Var[c • X ; μ | m] =ᵐ[μ] c ^ 2 • Var[X ; μ | m] := by
+lemma condVar_smul (c : ℝ) (X : Ω → ℝ) : Var[c • X; μ | m] =ᵐ[μ] c ^ 2 • Var[X; μ | m] := by
   calc
-    Var[c • X ; μ | m]
+    Var[c • X; μ | m]
     _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m] := by
       rw [condVar]
       refine condExp_congr_ae ?_
       filter_upwards [condExp_smul (m := m) c X] with ω hω
       simp [hω, ← mul_sub, mul_pow]
-    _ =ᵐ[μ] c ^ 2 • Var[X ; μ | m] := condExp_smul ..
+    _ =ᵐ[μ] c ^ 2 • Var[X; μ | m] := condExp_smul ..
 
-@[simp] lemma condVar_neg (X : Ω → ℝ) : Var[-X ; μ | m] =ᵐ[μ] Var[X ; μ | m] := by
+@[simp] lemma condVar_neg (X : Ω → ℝ) : Var[-X; μ | m] =ᵐ[μ] Var[X; μ | m] := by
   refine condExp_congr_ae ?_
   filter_upwards [condExp_neg (m := m) X] with ω hω
   simp [condVar, hω]

Mathlib/Probability/Variance.lean

@@ -60,23 +60,23 @@ def variance : ℝ := (evariance X μ).toReal
 /-- The `ℝ≥0∞`-valued variance of the real-valued random variable `X` according to the measure `μ`.
 
 This is defined as the Lebesgue integral of `(X - 𝔼[X])^2`. -/
-scoped notation "eVar[" X " ; " μ "]" => ProbabilityTheory.evariance X μ
+scoped notation "eVar[" X "; " μ "]" => ProbabilityTheory.evariance X μ
 
 /-- The `ℝ≥0∞`-valued variance of the real-valued random variable `X` according to the volume
 measure.
 
 This is defined as the Lebesgue integral of `(X - 𝔼[X])^2`. -/
-scoped notation "eVar[" X "]" => eVar[X ; MeasureTheory.MeasureSpace.volume]
+scoped notation "eVar[" X "]" => eVar[X; MeasureTheory.MeasureSpace.volume]
 
 /-- The `ℝ`-valued variance of the real-valued random variable `X` according to the measure `μ`.
 
 It is set to `0` if `X` has infinite variance. -/
-scoped notation "Var[" X " ; " μ "]" => ProbabilityTheory.variance X μ
+scoped notation "Var[" X "; " μ "]" => ProbabilityTheory.variance X μ
 
 /-- The `ℝ`-valued variance of the real-valued random variable `X` according to the volume measure.
 
 It is set to `0` if `X` has infinite variance. -/
-scoped notation "Var[" X "]" => Var[X ; MeasureTheory.MeasureSpace.volume]
+scoped notation "Var[" X "]" => Var[X; MeasureTheory.MeasureSpace.volume]
 
 theorem evariance_lt_top [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) : evariance X μ < ∞ := by
   have := ENNReal.pow_lt_top (hX.sub <| memℒp_const <| μ[X]).2 2
@@ -125,7 +125,7 @@ theorem evariance_eq_lintegral_ofReal :
     evariance X μ = ∫⁻ ω, ENNReal.ofReal ((X ω - μ[X]) ^ 2) ∂μ := by
   simp [evariance, ← enorm_pow, Real.enorm_of_nonneg (sq_nonneg _)]
 
-lemma variance_eq_integral (hX : AEMeasurable X μ) : Var[X ; μ] = ∫ ω, (X ω - μ[X]) ^ 2 ∂μ := by
+lemma variance_eq_integral (hX : AEMeasurable X μ) : Var[X; μ] = ∫ ω, (X ω - μ[X]) ^ 2 ∂μ := by
   simp [variance, evariance, toReal_enorm, ← integral_toReal ((hX.sub_const _).enorm.pow_const _) <|
     .of_forall fun _ ↦ ENNReal.pow_lt_top enorm_lt_top _]
 

Mathlib/Tactic/Linter/TextBased.lean

@@ -58,6 +58,8 @@ inductive StyleError where
   | windowsLineEnding
   /-- A line contains trailing whitespace. -/
   | trailingWhitespace
+  /-- A line contains a space before a semicolon -/
+  | semicolon
 deriving BEq
 
 /-- How to format style errors -/
@@ -79,6 +81,7 @@ def StyleError.errorMessage (err : StyleError) : String := match err with
   | windowsLineEnding => "This line ends with a windows line ending (\r\n): please use Unix line\
     endings (\n) instead"
   | trailingWhitespace => "This line ends with some whitespace: please remove this"
+  | semicolon => "This line contains a space before a semicolon"
 
 /-- The error code for a given style error. Keep this in sync with `parse?_errorContext` below! -/
 -- FUTURE: we're matching the old codes in `lint-style.py` for compatibility;
@@ -87,6 +90,7 @@ def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.adaptationNote => "ERR_ADN"
   | StyleError.windowsLineEnding => "ERR_WIN"
   | StyleError.trailingWhitespace => "ERR_TWS"
+  | StyleError.semicolon => "ERR_SEM"
 
 /-- Context for a style error: the actual error, the line number in the file we're reading
 and the path to the file. -/
@@ -164,6 +168,7 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do
         -- Use default values for parameters which are ignored for comparing style exceptions.
         -- NB: keep this in sync with `compare` above!
         | "ERR_ADN" => some (StyleError.adaptationNote)
+        | "ERR_SEM" => some (StyleError.semicolon)
         | "ERR_TWS" => some (StyleError.trailingWhitespace)
         | "ERR_WIN" => some (StyleError.windowsLineEnding)
         | _ => none
@@ -220,6 +225,21 @@ def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
   return (errors, if errors.size > 0 then some fixedLines else none)
 
 
+/-- Lint a collection of input strings for a semicolon preceded by a space. -/
+def semicolonLinter : TextbasedLinter := fun lines ↦ Id.run do
+  let mut errors := Array.mkEmpty 0
+  let mut fixedLines := lines
+  for h : idx in [:lines.size] do
+    let line := lines[idx]
+    let pos := line.find (· == ';')
+    -- Future: also lint for a semicolon *not* followed by a space or ⟩.
+    if pos != line.endPos && line.get (line.prev pos) == ' ' then
+      errors := errors.push (StyleError.semicolon, idx + 1)
+      -- We spell the bad string pattern this way to avoid the linter firing on itself.
+      fixedLines := fixedLines.set! idx (line.replace (⟨[' ', ';']⟩ : String) ";")
+   return (errors, if errors.size > 0 then some fixedLines else none)
+
+
 /-- Whether a collection of lines consists *only* of imports, blank lines and single-line comments.
 In practice, this means it's an imports-only file and exempt from almost all linting. -/
 def isImportsOnlyFile (lines : Array String) : Bool :=
@@ -231,7 +251,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    adaptationNoteLinter, trailingWhitespaceLinter
+    adaptationNoteLinter, semicolonLinter, trailingWhitespaceLinter
   ]
 
 
@@ -265,6 +285,7 @@ def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
   for lint in allLinters do
     let (err, changes) := lint 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
       changed := c
       changes_made := true

scripts/lint-style.py

@@ -38,7 +38,6 @@
 
 ERR_IBY = 11 # isolated by
 ERR_IWH = 22 # isolated where
-ERR_SEM = 13 # the substring " ;"
 ERR_CLN = 16 # line starts with a colon
 ERR_IND = 17 # second line not correctly indented
 ERR_ARR = 18 # space after "←"
@@ -197,9 +196,6 @@ def isolated_by_dot_semicolon_check(lines, path):
                     line = f"{indent}{line.lstrip()[3:]}"
         elif line.lstrip() == "where":
             errors += [(ERR_IWH, line_nr, path)]
-        if " ;" in line:
-            errors += [(ERR_SEM, line_nr, path)]
-            line = line.replace(" ;", ";")
         if line.lstrip().startswith(":"):
             errors += [(ERR_CLN, line_nr, path)]
         newlines.append((line_nr, line))
@@ -236,8 +232,6 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_IBY", "Line is an isolated 'by'")
         if errno == ERR_IWH:
             output_message(path, line_nr, "ERR_IWH", "Line is an isolated where")
-        if errno == ERR_SEM:
-            output_message(path, line_nr, "ERR_SEM", "Line contains a space before a semicolon")
         if errno == ERR_CLN:
             output_message(path, line_nr, "ERR_CLN", "Put : and := before line breaks, not after")
         if errno == ERR_IND: