External linters this project opts into #
Importing these modules registers their @[linter]s and their register_options; the values
are set in lakefile.lean's linterOptions block, which is where the deliberate on/off choice
for each lives. This module only makes the linters reachable in the CLI's build closure.
Linters that are text-script (linter.trailingWhitespace, linter.style.longLine) rather than
@[linter], and the tacticAnalysis.* family (a simp/grind/aesop run at every proof
step), are deliberately not here — the Stop hook is a lake build, not a script runner.