Lean4
/-- 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 (opts : LinterOptions) (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, `Mathlib.Analysis.InnerProductSpace.l2Space,
`Mathlib.Analysis.Normed.Lp.lpSpace]
-- We allow only names in UpperCamelCase, possibly with a trailing underscore.
let badNames :=
modules.filter fun name ↦
let upperCamelName := Lake.toUpperCamelCase name
!exceptions.contains name && upperCamelName != name && (s! "{upperCamelName}_") != name.toString
for bad in badNames do
let upperCamelName := Lake.toUpperCamelCase bad
let good := if bad.toString.endsWith "_" then s! "{upperCamelName}_" else upperCamelName.toString
IO.eprintln s! "error: module name '{bad }' is not in 'UpperCamelCase': it should be '{good}' instead"
return badNames.size
