From 0634fac03bbeabf412fd6007b25aed6c1b8a63f6 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 12 Jul 2024 09:58:40 -0400 Subject: [PATCH] feat: Add double empty Lint --- HepLean/AnomalyCancellation/Basic.lean | 12 ++++++------ HepLean/AnomalyCancellation/GroupActions.lean | 2 +- HepLean/AnomalyCancellation/MSSMNu/B3.lean | 2 +- HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 4 ++-- scripts/double_line_lint.lean | 11 ++++++++++- 5 files changed, 20 insertions(+), 11 deletions(-) diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index 1a298cf..8ea1866 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -108,7 +108,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) : add_zero S := by apply LinSols.ext exact χ.chargesAddCommMonoid.add_zero _ - nsmul n S := ⟨n • S.val, by + nsmul n S := ⟨n • S.val, by intro i rw [nsmul_eq_smul_cast ℚ] erw [(χ.linearACCs i).map_smul, S.linearSol i] @@ -122,7 +122,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) : /-- An instance providing the operations and properties for `LinSols` to form an module over `ℚ`. -/ @[simps!] -instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where +instance linSolsModule (χ : ACCSystemLinear) : Module ℚ χ.LinSols where smul a S := ⟨a • S.val, by intro i rw [(χ.linearACCs i).map_smul, S.linearSol i] @@ -177,13 +177,13 @@ structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where @[ext] lemma QuadSols.ext {χ : ACCSystemQuad} {S T : χ.QuadSols} (h : S.val = T.val) : S = T := by - have h := ACCSystemLinear.LinSols.ext h + have h := ACCSystemLinear.LinSols.ext h cases' S simp_all only /-- An instance giving the properties and structures to define an action of `ℚ` on `QuadSols`. -/ instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols where - smul a S := ⟨a • S.toLinSols , by + smul a S := ⟨a • S.toLinSols , by intro i erw [(χ.quadraticACCs i).map_smul] rw [S.quadSol i] @@ -198,7 +198,7 @@ instance quadSolsMulAction (χ : ACCSystemQuad) : MulAction ℚ χ.QuadSols wher /-- The inclusion of quadratic solutions into linear solutions. -/ def quadSolsInclLinSols (χ : ACCSystemQuad) : χ.QuadSols →[ℚ] χ.LinSols where - toFun := QuadSols.toLinSols + toFun := QuadSols.toLinSols map_smul' _ _ := rfl /-- If there are no quadratic equations (i.e. no U(1)'s in the underlying gauge group. The inclusion @@ -239,7 +239,7 @@ def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop := /-- An instance giving the properties and structures to define an action of `ℚ` on `Sols`. -/ instance solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols where - smul a S := ⟨a • S.toQuadSols , by + smul a S := ⟨a • S.toQuadSols, by erw [(χ.cubicACC).map_smul] rw [S.cubicSol] simp⟩ diff --git a/HepLean/AnomalyCancellation/GroupActions.lean b/HepLean/AnomalyCancellation/GroupActions.lean index 2ed7378..6f63edd 100644 --- a/HepLean/AnomalyCancellation/GroupActions.lean +++ b/HepLean/AnomalyCancellation/GroupActions.lean @@ -100,7 +100,7 @@ instance quadSolAction {χ : ACCSystem} (G : ACCSystemGroupAction χ) : rfl lemma linSolRep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) - (S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun S g) = + (S : χ.QuadSols) : χ.quadSolsInclLinSols (G.quadSolAction.toFun S g) = G.linSolRep g (χ.quadSolsInclLinSols S) := rfl lemma rep_quadSolAction_commute {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) diff --git a/HepLean/AnomalyCancellation/MSSMNu/B3.lean b/HepLean/AnomalyCancellation/MSSMNu/B3.lean index 7bb1bfc..b2a3b46 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/B3.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/B3.lean @@ -37,7 +37,7 @@ def B₃AsCharge : MSSMACC.Charges := toSpecies.symm | 1, 2 => 1 | 2, 0 => - 1 | 2, 1 => - 1 - | 2, 2 => 1 + | 2, 2 => 1 | 3, 0 => - 3 | 3, 1 => - 3 | 3, 2 => 3 diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean index 58632ea..2355fa4 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean @@ -50,7 +50,7 @@ def splitSMPlusH : (Fin 18 ⊕ Fin 2 → ℚ) ≃ (Fin 18 → ℚ) × (Fin 2 → /-- An equivalence between `MSSMCharges.charges` and `(Fin 18 → ℚ) × (Fin 2 → ℚ)`. This splits the charges up into the SM and the additional ones for the MSSM. -/ @[simps!] -def toSplitSMPlusH : MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) := +def toSplitSMPlusH : MSSMCharges.Charges ≃ (Fin 18 → ℚ) × (Fin 2 → ℚ) := toSMPlusH.trans splitSMPlusH /-- An equivalence between `(Fin 18 → ℚ)` and `(Fin 6 → Fin 3 → ℚ)`. -/ @@ -74,7 +74,7 @@ def toSMSpecies (i : Fin 6) : MSSMCharges.Charges →ₗ[ℚ] MSSMSpecies.Charge map_add' _ _ := by rfl map_smul' _ _ := by rfl -lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) : +lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : (Fin 6 → Fin 3 → ℚ) × (Fin 2 → ℚ)) : (toSMSpecies i) (toSpecies.symm f) = f.1 i := by change (Prod.fst ∘ toSpecies ∘ toSpecies.symm ) _ i= f.1 i simp diff --git a/scripts/double_line_lint.lean b/scripts/double_line_lint.lean index 3b04875..b39e7d8 100644 --- a/scripts/double_line_lint.lean +++ b/scripts/double_line_lint.lean @@ -31,6 +31,15 @@ def doubleEmptyLineLinter : HepLeanTextLinter := fun lines ↦ Id.run do else none) errors.toArray +/-- Checks if there is a souble space in the line, which is not at the start. -/ +def doubleSpaceLinter : HepLeanTextLinter := fun lines ↦ Id.run do + let enumLines := (lines.toList.enumFrom 1) + let errors := enumLines.filterMap (fun (lno, l) ↦ + if String.containsSubstr l.trimLeft " " then + some (s!" Non-initial double space in line. ", lno) + else none) + errors.toArray + structure HepLeanErrorContext where /-- The underlying `message`. -/ error : String @@ -47,7 +56,7 @@ def hepLeanLintFile (path : FilePath) : IO Bool := do let lines ← IO.FS.lines path let allOutput := (Array.map (fun lint ↦ (Array.map (fun (e, n) ↦ HepLeanErrorContext.mk e n path)) (lint lines))) - #[doubleEmptyLineLinter] + #[doubleEmptyLineLinter, doubleSpaceLinter] let errors := allOutput.flatten printErrors errors return errors.size > 0