Lean4
@[inherit_doc Mathlib.Linter.linter.style.longFile]
def longFileLinter : Linter where
run :=
withSetOptionIn fun stx ↦ do
let linterBound := linter.style.longFile.get (← getOptions)
if linterBound == 0 then
return
let defValue := linter.style.longFileDefValue.get (← getOptions)
let smallOption :=
match stx with
| `(set_option linter.style.longFile $x) => TSyntax.getNat ⟨x.raw⟩ ≤ defValue
| _ => false
if smallOption then
logLint0Disable linter.style.longFile stx
m! "The default value of the `longFile` linter is {defValue }.\n\
The current value of {linterBound } does not exceed the allowed bound.\n\
Please, remove the `set_option linter.style.longFile {linterBound}`."
else
-- Thanks to the above check, the linter option is either not set (and hence equal
-- to the default) or set to some value *larger* than the default.
-- `Parser.isTerminalCommand` allows `stx` to be `#exit`: this is useful for tests.
unless Parser.isTerminalCommand stx do
return
-- We exclude `Mathlib.lean` from the linter: it exceeds linter's default number of allowed
-- lines, and it is an auto-generated import-only file.
-- TODO: if there are more such files, revise the implementation.
if (← getMainModule) == `Mathlib then
return
if let some init := stx.getTailPos? then
-- the last line: we subtract 1, since the last line is expected to be empty
let lastLine := ((← getFileMap).toPosition init).line
if lastLine ≤ defValue && defValue < linterBound then
logLint0Disable linter.style.longFile stx
m! "The default value of the `longFile` linter is {defValue }.\n\
This file is {lastLine } lines long which does not exceed the allowed bound.\n\
Please, remove the `set_option linter.style.longFile {linterBound}`."
else
-- `candidate` is divisible by `100` and satisfies `lastLine + 100 < candidate ≤ lastLine + 200`
-- note that either `lastLine ≤ defValue` and `defValue = linterBound` hold or
-- `candidate` is necessarily bigger than `lastLine` and hence bigger than `defValue`
let candidate := (lastLine / 100) * 100 + 200
let candidate := max candidate defValue
if defValue ≤ linterBound && linterBound < lastLine then
logLint0Disable linter.style.longFile stx
m! "This file is {lastLine } lines long, but the limit is {linterBound }.\n\n\
You can extend the allowed length of the file using \
`set_option linter.style.longFile {candidate}`.\n\
You can completely disable this linter by setting the length limit to `0`."
else
-- Finally, the file exceeds the default value, but not the option: we only allow the value
-- of the option to be `candidate` or `candidate + 100`.
-- In particular, this flags any option that is set to an unnecessarily high value.
if linterBound == candidate || linterBound + 100 == candidate then
return
else
logLint0Disable linter.style.longFile stx
m! "This file is {lastLine } lines long. \
The current limit is {linterBound }, but it is expected to be {candidate }:\n\
`set_option linter.style.longFile {candidate}`."
