[Merged by Bors] - refactor(*): scrub imports #17568

semorrison · 2022-11-16T15:09:33Z

For each file, we read each declaration and find the files containing each referenced declaration. This is the "needed" set. We then replace the imports with

imports which are needed
other needed files which would not otherwise be transitively imported

Thus we don't remove any imports merely because they are transitively redundant. Instead we remove imports only if they are genuinely unnecessary. We also have to add back in imports (because they have been removed from higher up the import hierarchy).

I've committed the Lean script (thanks Mario!) that generates the underlying data, but not the Mathematica notebook that does that import calculations and text replacement (because it's a mess, and I want this merged quickly before it rots).

We try not to reorder imports unnecessarily.
But we don't sort: anything new that needs to be added just comes after the existing imports.
This drops a few comments on import lines.
It replaces a few import X with import X.default. (I think this is not bad: we probably want to remove all the .default files anyway at some point.)

Vierkantor · 2022-11-16T15:21:01Z

src/algebra/category/Module/biproducts.lean

+    fac' := by { rintros s (⟨⟩|⟨⟩); { ext x, simp only
+      [binary_fan.π_app_right, binary_fan.π_app_left, Module.coe_comp, function.comp_app,
+        linear_map.fst_apply, linear_map.snd_apply, linear_map.prod_apply, pi.prod], }, },


Is this an intended part of the diff?

Yes, this mysteriously slowed down. 🤷

src/group_theory/order_of_element.lean

Vierkantor

I checked all the non-import changes with git diff c34a1aa4263bdf585dd705508c11d3b75836049e | grep '^[+-]' | grep -v '^[-+]import', and the imports should be fine as long as everything still builds. So let's get this merged quickly!

bors d+

bors · 2022-11-16T15:30:38Z

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

src/analysis/inner_product_space/projection.lean

src/algebra/order/lattice_group.lean

src/algebraic_topology/simplex_category.lean

semorrison · 2022-11-16T22:28:05Z

Thanks for the reviews. I have a local build success so I'm going to optimistically try this in bors. (I haven't yet built after merging the last master, so it may well fail.)

semorrison · 2022-11-16T22:28:18Z

bors merge p=10

For each file, we read each declaration and find the files containing each referenced declaration. This is the "needed" set. We then replace the imports with * imports which are needed * other needed files which would not otherwise be transitively imported Thus we don't remove any imports merely because they are transitively redundant. Instead we remove imports only if they are genuinely unnecessary. We also have to add back in imports (because they have been removed from higher up the import hierarchy). I've committed the Lean script (thanks Mario!) that generates the underlying data, but not the Mathematica notebook that does that import calculations and text replacement (because it's a mess, and I want this merged quickly before it rots). * We try not to reorder imports unnecessarily. * But we don't sort: anything new that needs to be added just comes after the existing imports. * This drops a few comments on `import` lines. * It replaces a few `import X` with `import X.default`. (I think this is not bad: we probably want to remove all the .default files anyway at some point.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2022-11-17T00:49:34Z

Build failed:

Run tests

semorrison · 2022-11-17T01:58:07Z

bors merge p=10

For each file, we read each declaration and find the files containing each referenced declaration. This is the "needed" set. We then replace the imports with * imports which are needed * other needed files which would not otherwise be transitively imported Thus we don't remove any imports merely because they are transitively redundant. Instead we remove imports only if they are genuinely unnecessary. We also have to add back in imports (because they have been removed from higher up the import hierarchy). I've committed the Lean script (thanks Mario!) that generates the underlying data, but not the Mathematica notebook that does that import calculations and text replacement (because it's a mess, and I want this merged quickly before it rots). * We try not to reorder imports unnecessarily. * But we don't sort: anything new that needs to be added just comes after the existing imports. * This drops a few comments on `import` lines. * It replaces a few `import X` with `import X.default`. (I think this is not bad: we probably want to remove all the .default files anyway at some point.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2022-11-17T04:16:34Z

Build failed:

Run tests

semorrison · 2022-11-17T04:38:04Z

bors merge p=10

For each file, we read each declaration and find the files containing each referenced declaration. This is the "needed" set. We then replace the imports with * imports which are needed * other needed files which would not otherwise be transitively imported Thus we don't remove any imports merely because they are transitively redundant. Instead we remove imports only if they are genuinely unnecessary. We also have to add back in imports (because they have been removed from higher up the import hierarchy). I've committed the Lean script (thanks Mario!) that generates the underlying data, but not the Mathematica notebook that does that import calculations and text replacement (because it's a mess, and I want this merged quickly before it rots). * We try not to reorder imports unnecessarily. * But we don't sort: anything new that needs to be added just comes after the existing imports. * This drops a few comments on `import` lines. * It replaces a few `import X` with `import X.default`. (I think this is not bad: we probably want to remove all the .default files anyway at some point.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

bors · 2022-11-17T07:53:16Z

Pull request successfully merged into master.

Build succeeded:

This is another run of #17568, scrubbing unnecessary imports. Like last time we only remove genuinely unneeded imports, and leave merely transitively redundant imports alone. (I *still* disagree with the objectors to removing transitively redundant imports Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

semorrison added 3 commits November 16, 2022 23:43

does it finally build?

424f5da

fix up tactic imports

de0db98

cleanup

9819a8f

semorrison requested review from a team as code owners November 16, 2022 15:09

semorrison added 2 commits November 17, 2022 02:10

fix

c5cc9d8

Merge remote-tracking branch 'origin/master' into imports

9d4893f

Vierkantor reviewed Nov 16, 2022

View reviewed changes

Vierkantor self-assigned this Nov 16, 2022

Vierkantor reviewed Nov 16, 2022

View reviewed changes

src/group_theory/order_of_element.lean Show resolved Hide resolved

Vierkantor approved these changes Nov 16, 2022

View reviewed changes

leanprover-community-bot-assistant added the delegated The PR author may merge after reviewing final suggestions. label Nov 16, 2022

hrmacbeth reviewed Nov 16, 2022

View reviewed changes

src/analysis/inner_product_space/projection.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Nov 16, 2022

View reviewed changes

src/algebra/order/lattice_group.lean Outdated Show resolved Hide resolved

src/algebraic_topology/simplex_category.lean Outdated Show resolved Hide resolved

semorrison added 2 commits November 17, 2022 09:25

build failure from merging master, and review comments

f659136

Merge remote-tracking branch 'origin/master' into imports

16889e9

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Nov 16, 2022

fixes

5056588

fix test

7e42b6d

bors bot changed the title ~~refactor(*): scrub imports~~ [Merged by Bors] - refactor(*): scrub imports Nov 17, 2022

bors bot closed this Nov 17, 2022

bors bot deleted the imports branch November 17, 2022 07:53

eric-wieser mentioned this pull request May 2, 2023

chore(analysis): remove lots more unnecessary imports #18914

Closed

semorrison mentioned this pull request May 3, 2023

[Merged by Bors] - chore(*): removed unneeded imports #18926

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(*): scrub imports #17568

[Merged by Bors] - refactor(*): scrub imports #17568

semorrison commented Nov 16, 2022

Vierkantor Nov 16, 2022

semorrison Nov 16, 2022

Vierkantor left a comment

bors bot commented Nov 16, 2022

semorrison commented Nov 16, 2022

semorrison commented Nov 16, 2022

bors bot commented Nov 17, 2022

semorrison commented Nov 17, 2022

bors bot commented Nov 17, 2022

semorrison commented Nov 17, 2022

bors bot commented Nov 17, 2022

[Merged by Bors] - refactor(*): scrub imports #17568

[Merged by Bors] - refactor(*): scrub imports #17568

Conversation

semorrison commented Nov 16, 2022

Vierkantor Nov 16, 2022

Choose a reason for hiding this comment

semorrison Nov 16, 2022

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

bors bot commented Nov 16, 2022

semorrison commented Nov 16, 2022

semorrison commented Nov 16, 2022

bors bot commented Nov 17, 2022

semorrison commented Nov 17, 2022

bors bot commented Nov 17, 2022

semorrison commented Nov 17, 2022

bors bot commented Nov 17, 2022