Lean4
/-- Lint a collection of modules for style violations.
Print formatted errors for all unexpected style violations to standard output;
correct automatically fixable style errors if configured so.
Return the number of files which had new style errors.
`opts` contains the options defined in the Lakefile, determining which linters to enable.
`nolints` is a list of style exceptions to take into account.
`moduleNames` are the names of all the modules to lint,
`mode` specifies what kind of output this script should produce,
`fix` configures whether fixable errors should be corrected in-place. -/
def lintModules (opts : LinterOptions) (nolints : Array String) (moduleNames : Array Lean.Name) (style : ErrorFormat)
(fix : Bool) : IO UInt32 := do
let styleExceptions := parseStyleExceptions nolints
let mut numberErrorFiles : UInt32 := 0
let mut allUnexpectedErrors := #[]
for module in moduleNames do
-- Convert the module name to a file name, then lint that file.
let path := mkFilePath (module.components.map toString) |>.addExtension "lean"
let (errors, changed) := ← lintFile opts path styleExceptions
if let some c := changed then
if fix then
let _ := ← IO.FS.writeFile path ("\n".intercalate c.toList)
if errors.size > 0 then
allUnexpectedErrors := allUnexpectedErrors.append errors
numberErrorFiles :=
numberErrorFiles +
1
-- Passing Lean options to Python files seems like a lot of work for something we want to
-- run entirely inside of Lean in the end anyway.
-- So for now, we enable/disable all of them with a single switch.
if getLinterValue linter.pythonStyle opts then
-- Run the remaining python linters. It is easier to just run on all files.
-- If this poses an issue, I can either filter the output
-- or wait until lint-style.py is fully rewritten in Lean.
let args := if fix then #["--fix"] else #[]
let output ← IO.Process.output { cmd := "./scripts/print-style-errors.sh", args := args }
if output.exitCode != 0 then
numberErrorFiles := numberErrorFiles + 1
IO.eprintln s! "error: `print-style-error.sh` exited with code {output.exitCode}"
IO.eprint output.stderr
else if output.stdout != "" then
numberErrorFiles := numberErrorFiles + 1
IO.eprint output.stdout
formatErrors allUnexpectedErrors style
if allUnexpectedErrors.size > 0 then
IO.eprintln s! "error: found {allUnexpectedErrors.size} new style error(s)"
return numberErrorFiles
