-
Notifications
You must be signed in to change notification settings - Fork 330
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, I understand now, thanks! I updated the PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Kim, thank you for your comments! I accepted the ones that I understood and left a question for the one that I did not follow.
def importsBelow (ig : NameMap (Array Name)) (ms : NameSet) : NameSet := | ||
(ig.upstreamOf ms).fold (σ := NameSet) (fun _ ↦ ·.insert ·) {} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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: |
This PR makes the
minImports
linter report more information:Prompted by this Zulip thread.