Skip to content

Commit

Permalink
chore: adjustments to runLinter so it can be used downstream (#370)
Browse files Browse the repository at this point in the history
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
  • Loading branch information
kim-em and digama0 authored Nov 17, 2023
1 parent 0c29911 commit 385b5f9
Showing 1 changed file with 7 additions and 5 deletions.
12 changes: 7 additions & 5 deletions scripts/runLinter.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,19 @@ unsafe def main (args : List String) : IO Unit := do
let some module :=
match args with
| [] => some `Std
| [mod] => Syntax.decodeNameLit s!"`{mod}"
| [mod] => match mod.toName with
| .anonymous => none
| name => some name
| _ => none
| IO.eprintln "Usage: runLinter [--update] [Std.Data.Nat.Basic]" *> IO.Process.exit 1
let nolintsFile := "scripts/nolints.json"
let nolints ← readJsonFile NoLints nolintsFile
searchPathRef.set compile_time_search_path%
withImportModules #[{module}] {} (trustLevel := 1024) fun env =>
let ctx := {fileName := "", fileMap := default}
let state := {env}
let ctx := { fileName := "", fileMap := default }
let state := { env }
Prod.fst <$> (CoreM.toIO · ctx state) do
let decls ← getDeclsInPackage `Std
let decls ← getDeclsInPackage module.getRoot
let linters ← getChecks (slow := true) (useOnly := false)
let results ← lintCore decls linters
if update then
Expand All @@ -56,7 +58,7 @@ unsafe def main (args : List String) : IO Unit := do
if failed then
let fmtResults ←
formatLinterResults results decls (groupByFilename := true) (useErrorFormat := true)
"in Std" (runSlowLinters := true) .medium linters.size
s!"in {module}" (runSlowLinters := true) .medium linters.size
IO.print (← fmtResults.toString)
IO.Process.exit 1
else
Expand Down

0 comments on commit 385b5f9

Please sign in to comment.