Lean4
/-- Read a file and apply all text-based linters.
Return a list of all unexpected errors, and, if some errors could be fixed automatically,
the collection of all lines with every automatic fix applied.
`exceptions` are any pre-existing style exceptions for this file. -/
def lintFile (opts : LinterOptions) (path : FilePath) (exceptions : Array ErrorContext) :
IO (Array ErrorContext × Option (Array String)) := do
let mut errors :=
#[]
-- Whether any changes were made by auto-fixes.
let mut changes_made := false
let contents ← IO.FS.readFile path
let replaced := contents.crlfToLf
if replaced != contents then
changes_made := true
errors := errors.push (ErrorContext.mk StyleError.windowsLineEnding 1 path)
let lines := (replaced.splitOn "\n").toArray
if isImportsOnlyFile lines then
return
(errors, if changes_made then some lines else none)
-- All further style errors raised in this file.
let mut allOutput :=
#[]
-- A working copy of the lines in this file, modified by applying the auto-fixes.
let mut changed := lines
for lint in allLinters do
let (err, changes) := lint opts changed
allOutput :=
allOutput.append
(Array.map (fun (e, n) ↦ #[(ErrorContext.mk e n path)]) err)
-- TODO: auto-fixes do not take style exceptions into account
if let some c := changes then
changed := c
changes_made := true
errors := errors.append (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))
return (errors, if changes_made then some changed else none)
