[Merged by Bors] - feat: add by how many modules imports grew #18303
Conversation
PR summary 894f7a8ec9Import 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 |
| def importsBelow (ig : NameMap (Array Name)) (ms : NameSet) : NameSet := | ||
| (ig.upstreamOf ms).fold (σ := NameSet) (fun _ ↦ ·.insert ·) {} |
There was a problem hiding this comment.
We could avoid recalculating here, too. Rather than stashing env.importGraph in the state, stash (← env.importGraph).transitiveClosure.
There was a problem hiding this comment.
I'm not sure that I understand here: importGraph is a NameMap (Array Name), while transitiveClosure returns a NameMap NameSet. I do not really know how to then use upstreamOf, since that function wants an importGraph as an input.
There was a problem hiding this comment.
You wouldn't even need upstreamOf. You'd just take the union over ms of the values from the transitiveClosure map.
There was a problem hiding this comment.
Ah, I understand now, thanks! I updated the PR.
| def importsBelow (ig : NameMap (Array Name)) (ms : NameSet) : NameSet := | ||
| (ig.upstreamOf ms).fold (σ := NameSet) (fun _ ↦ ·.insert ·) {} |
There was a problem hiding this comment.
I'm not sure that I understand here: importGraph is a NameMap (Array Name), while transitiveClosure returns a NameMap NameSet. I do not really know how to then use upstreamOf, since that function wants an importGraph as an input.
|
bors merge |
This PR makes the `minImports` linter report more information: * the number of increase imports, * which previously minimal imports became redundant, * which new minimal imports should be added. Prompted by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/minImports.20linter.20request).
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
This PR makes the
minImportslinter report more information:Prompted by this Zulip thread.