chore: Double line linter
This commit is contained in:
jstoobysmith
parent
bd9f796110
commit
ae18a2196d
8 changed files with 75 additions and 17 deletions
|
|
@ -22,7 +22,6 @@ universe v u
|
|||
open Nat
|
||||
open BigOperators
|
||||
|
||||
|
||||
/-- The vector space of charges corresponding to the MSSM fermions. -/
|
||||
@[simps!]
|
||||
def MSSMCharges : ACCSystemCharges := ACCSystemChargesMk 20
|
||||
|
|
@ -314,7 +313,6 @@ def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂ (
|
|||
ring
|
||||
ring)
|
||||
|
||||
|
||||
/-- The quadratic ACC. -/
|
||||
@[simp]
|
||||
def accQuad : HomogeneousQuadratic MSSMCharges.Charges := quadBiLin.toHomogeneousQuad
|
||||
|
|
@ -335,7 +333,6 @@ lemma accQuad_ext {S T : (MSSMCharges).Charges}
|
|||
repeat rw [h1]
|
||||
rw [hd, hu]
|
||||
|
||||
|
||||
/-- The function underlying the symmetric trilinear form used to define the cubic ACC. -/
|
||||
@[simp]
|
||||
def cubeTriLinToFun
|
||||
|
|
@ -363,7 +360,6 @@ lemma cubeTriLinToFun_map_smul₁ (a : ℚ) (S T R : MSSMCharges.Charges) :
|
|||
simp only [map_smul, Hd_apply, Fin.reduceFinMk, Fin.isValue, smul_eq_mul, Hu_apply]
|
||||
ring
|
||||
|
||||
|
||||
lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
|
||||
cubeTriLinToFun (S + T, R, L) = cubeTriLinToFun (S, R, L) + cubeTriLinToFun (T, R, L) := by
|
||||
simp only [cubeTriLinToFun]
|
||||
|
|
@ -382,7 +378,6 @@ lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
|
|||
rw [Hd.map_add, Hu.map_add]
|
||||
ring
|
||||
|
||||
|
||||
lemma cubeTriLinToFun_swap1 (S T R : MSSMCharges.Charges) :
|
||||
cubeTriLinToFun (S, T, R) = cubeTriLinToFun (T, S, R) := by
|
||||
simp only [cubeTriLinToFun, MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue, Hd_apply,
|
||||
|
|
|
|||
|
|
@ -50,5 +50,4 @@ def YAsCharge : MSSMACC.Charges := toSpecies.invFun
|
|||
def Y : MSSMACC.Sols :=
|
||||
MSSMACC.AnomalyFreeMk YAsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
|
||||
|
||||
|
||||
end MSSMACC
|
||||
|
|
|
|||
|
|
@ -78,8 +78,6 @@ lemma Y₃_plus_B₃_plus_proj (T : MSSMACC.LinSols) (a b c : ℚ) :
|
|||
funext i
|
||||
linarith
|
||||
|
||||
|
||||
|
||||
lemma quad_Y₃_proj (T : MSSMACC.LinSols) :
|
||||
quadBiLin Y₃.val (proj T).val = dot Y₃.val B₃.val * quadBiLin Y₃.val T.val := by
|
||||
rw [proj_val]
|
||||
|
|
@ -119,7 +117,6 @@ lemma quad_proj (T : MSSMACC.Sols) :
|
|||
rw [quad_Y₃_proj, quad_B₃_proj, quad_self_proj]
|
||||
ring
|
||||
|
||||
|
||||
lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
|
||||
cubeTriLin (proj T).val (proj T).val Y₃.val =
|
||||
(dot Y₃.val B₃.val)^2 * cubeTriLin T.val T.val Y₃.val := by
|
||||
|
|
@ -186,6 +183,4 @@ lemma cube_proj (T : MSSMACC.Sols) :
|
|||
rw [cube_proj_proj_Y₃, cube_proj_proj_B₃, cube_proj_proj_self]
|
||||
ring
|
||||
|
||||
|
||||
|
||||
end MSSMACC
|
||||
|
|
|
|||
|
|
@ -44,7 +44,6 @@ lemma planeY₃B₃_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
|
|||
rw [smul_add, smul_add]
|
||||
rw [smul_smul, smul_smul, smul_smul]
|
||||
|
||||
|
||||
lemma planeY₃B₃_eq (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h : a = a' ∧ b = b' ∧ c = c') :
|
||||
(planeY₃B₃ R a b c) = (planeY₃B₃ R a' b' c') := by
|
||||
rw [h.1, h.2.1, h.2.2]
|
||||
|
|
|
|||
|
|
@ -137,7 +137,6 @@ def InCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
|
|||
cubeTriLin R.val R.val R.val = 0 ∧ cubeTriLin R.val R.val B₃.val = 0 ∧
|
||||
cubeTriLin R.val R.val Y₃.val = 0
|
||||
|
||||
|
||||
instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := by
|
||||
apply And.decidable
|
||||
|
||||
|
|
|
|||
|
|
@ -70,14 +70,11 @@ def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := Tri
|
|||
ring
|
||||
)
|
||||
|
||||
|
||||
|
||||
/-- The cubic anomaly equation. -/
|
||||
@[simp]
|
||||
def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).Charges) :=
|
||||
(accCubeTriLinSymm).toCubic
|
||||
|
||||
|
||||
lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).Charges) :
|
||||
accCube n S = ∑ i : Fin n, S i ^ 3:= by
|
||||
rw [accCube, TriLinearSymm.toCubic]
|
||||
|
|
@ -177,5 +174,4 @@ lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j
|
|||
erw [← hlt]
|
||||
simp
|
||||
|
||||
|
||||
end PureU1
|
||||
|
|
|
|||
|
|
@ -37,3 +37,7 @@ srcDir = "scripts"
|
|||
[[lean_exe]]
|
||||
name = "type_former_lint"
|
||||
srcDir = "scripts"
|
||||
|
||||
[[lean_exe]]
|
||||
name = "double_line_lint"
|
||||
srcDir = "scripts"
|
||||
71
scripts/double_line_lint.lean
Normal file
71
scripts/double_line_lint.lean
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import Lean
|
||||
import Mathlib.Tactic.Linter.TextBased
|
||||
/-!
|
||||
|
||||
# Double line Lint
|
||||
|
||||
This linter double empty lines in files.
|
||||
|
||||
## Note
|
||||
|
||||
Parts of this file are adapted from `Mathlib.Tactic.Linter.TextBased`,
|
||||
authored by Michael Rothgang.
|
||||
-/
|
||||
open Lean System Meta
|
||||
|
||||
/-- Given a list of lines, outputs an error message and a line number. -/
|
||||
def HepLeanTextLinter : Type := Array String → Array (String × ℕ)
|
||||
|
||||
/-- Checks if there are two consecutive empty lines. -/
|
||||
def doubleEmptyLineLinter : HepLeanTextLinter := fun lines ↦ Id.run do
|
||||
let enumLines := (lines.toList.enumFrom 1)
|
||||
let pairLines := List.zip enumLines (List.tail! enumLines)
|
||||
let errors := pairLines.filterMap (fun ((lno1, l1), _, l2) ↦
|
||||
if l1.length == 0 && l2.length == 0 then
|
||||
some (s!" Double empty line. ", lno1)
|
||||
else none)
|
||||
errors.toArray
|
||||
|
||||
structure HepLeanErrorContext where
|
||||
/-- The underlying `message`. -/
|
||||
error : String
|
||||
/-- The line number -/
|
||||
lineNumber : ℕ
|
||||
/-- The file path -/
|
||||
path : FilePath
|
||||
|
||||
def printErrors (errors : Array HepLeanErrorContext) : IO Unit := do
|
||||
for e in errors do
|
||||
IO.println (s!"error: {e.path}:{e.lineNumber}: {e.error}")
|
||||
|
||||
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]
|
||||
let errors := allOutput.flatten
|
||||
printErrors errors
|
||||
return errors.size > 0
|
||||
|
||||
def main (_ : List String) : IO UInt32 := do
|
||||
initSearchPath (← findSysroot)
|
||||
let mods : Name := `HepLean
|
||||
let imp : Import := {module := mods}
|
||||
let mFile ← findOLean imp.module
|
||||
unless (← mFile.pathExists) do
|
||||
throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist"
|
||||
let (hepLeanMod, _) ← readModuleData mFile
|
||||
let mut warned := false
|
||||
for imp in hepLeanMod.imports do
|
||||
if imp.module == `Init then continue
|
||||
let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean"
|
||||
if ← hepLeanLintFile filePath then
|
||||
warned := true
|
||||
if warned then
|
||||
throw <| IO.userError s!"Errors found."
|
||||
return 0
|
||||
Loading…
Add table
Add a link
Reference in a new issue