feat: a linter to deprecate imported modules #20987
Conversation
PR summary 5191403211Import changes exceeding 2%
Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
Maybe |
github-actions
bot
added
the
large-import
|
!bench |
1 similar comment
|
!bench |
| `addModuleDeprecation` adds to the `deprecateModuleExt` extension the pair consisting of the | ||
| current module name and the array of its direct imports. | ||
| It ignores `Init`, since this is a special module that is expected to be imported by all files. |
There was a problem hiding this comment.
Perhaps: "It ignores direct imports in Init"? (I was thinking whether you meant "the current module name in Init"... but that doesn't make much sense.)
There was a problem hiding this comment.
I wrote "It ignores the Init import", since usually Init is not explicitly written and it is implicitly imported anyway.
| elab "show_deprecated_modules" : command => do | ||
| let directImports := deprecateModuleExt.getState (← getEnv) | ||
| logInfo <| "\n".intercalate <| | ||
| directImports.fold (init := ["Deprecated modules\n"]) fun nms (i, deps) => |
There was a problem hiding this comment.
I'm pretty sure there's room for bikeshedding this formatting. I think we can land something and iterate.
| let fm ← getFileMap | ||
| let md := (getMainModuleDoc (← getEnv)).toArray | ||
| -- The end of the first module doc-string, or the end of the file if there is none. | ||
| let firstDocModPos := match md[0]? with | ||
| | none => fm.positions.back! | ||
| | some doc => fm.ofPosition doc.declarationRange.endPos | ||
| unless stx.getTailPos?.getD default ≤ firstDocModPos do | ||
| return | ||
| -- We try to parse the file up to `firstDocModPos`. | ||
| let upToStx ← parseUpToHere firstDocModPos <|> (do | ||
| -- If parsing failed, there is some command which is not a module docstring. | ||
| -- In that case, we parse until the end of the modules and add an extra `section` afterwards, | ||
| -- so we trigger a "no module doc-string" warning. | ||
| let fil ← getFileName | ||
| let (stx, _) ← Parser.parseHeader { input := fm.source, fileName := fil, fileMap := fm } | ||
| parseUpToHere (stx.getTailPos?.getD default) "\nsection") | ||
| let importIds := getImportIds upToStx |
There was a problem hiding this comment.
These lines are also present in the headerLinter. Can you factor them into a common function?
(I think it's fine if this linter imports the Header linter: didn't we soft-decide that anyway at some point?)
Co-authored-by: grunweg <[email protected]>
…over-community/mathlib4 into adomani/deprecated_imports_linter
|
Here are the benchmark results for commit c2b50b2. |
|
|
|
||
| /-- | ||
| The `deprecateModule` linter emits a warning when a file that has been renamed or split | ||
| is imported. |
| `addModuleDeprecation` adds to the `deprecateModuleExt` extension the pair consisting of the | ||
| current module name and the array of its direct imports. | ||
| It ignores `Init`, since this is a special module that is expected to be imported by all files. |
There was a problem hiding this comment.
I wrote "It ignores the Init import", since usually Init is not explicitly written and it is implicitly imported anyway.
|
!bench |
|
Here are the benchmark results for commit 5191403. |
|
This is still a prototype, but writing
in file
A.leanmeans that any file that importsAwill haveimport Aflagged with a suggestion to importBar1andBar2instead.Zulip discussion