Lean4
@[inherit_doc Mathlib.Linter.linter.deprecated.module]
def moduleLinter : Linter where
run :=
withSetOptionIn fun stx ↦ do
unless getLinterValue linter.deprecated.module (← getLinterOptions) do
return
if (← get).messages.hasErrors then
return
let laterCommand ← IsLaterCommand.get
if laterCommand || (Parser.isTerminalCommand stx && !laterCommand) then
return
IsLaterCommand.set true
let deprecations := deprecatedModuleExt.getState (← getEnv)
if deprecations.isEmpty then
return
if stx.isOfKind ``Linter.deprecated_modules then
return
let fm ← getFileMap
let (importStx, _) ← Parser.parseHeader { inputString := fm.source, fileName := ← getFileName, fileMap := fm }
let modulesWithNames := (getImportIds importStx).map fun i ↦ (i, i.getId)
for (i, preferred, msg?) in deprecations do
for (nmStx, _) in modulesWithNames.filter (·.2 == i)do
Linter.logLint linter.deprecated.module nmStx
m!"{(msg?.getD "")}\n\
'{nmStx }' has been deprecated: please replace this import by\n\n\
{String.join (preferred.foldl (·.push s!"import {·}\n") #[]).toList}"
