Skip to content
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] - chore(algebra/algebra): reduce imports for algebra.algebra.tower #17476

Closed
wants to merge 5 commits into from

Conversation

Vierkantor
Copy link
Collaborator

@Vierkantor Vierkantor commented Nov 11, 2022

This splits algebra.algebra.tower into two files: algebra.algebra.tower.basic and algebra.algebra.subalgebra.tower.

The motivation behind this PR is that algebra.algebra.tower is a relatively fundamental and popular file to import (especially since it used to contain is_scalar_tower), but its import tree also includes relatively complicated files such as ring_theory.ideal.operations. By splitting off these less popular dependencies we can save quite a bit of complexity in the import graph.


Open in Gitpod

@Vierkantor Vierkantor added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. t-algebra Algebra (groups, rings, fields etc) labels Nov 11, 2022
Vierkantor and others added 4 commits November 14, 2022 15:19
This splits `algebra.algebra.tower` into three files: `algebra.algebra.tower.basic`, `algebra.algebra.tower.bilinear` and `algebra.algebra.subalgebra.tower`
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Nov 14, 2022
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 14, 2022
This rename is unneeded now that the other files in that folder have been moved out.
@Vierkantor Vierkantor added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 15, 2022
@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 15, 2022
bors bot pushed a commit that referenced this pull request Nov 15, 2022
…17476)

This splits `algebra.algebra.tower` into two files: `algebra.algebra.tower.basic` and `algebra.algebra.subalgebra.tower`.

The motivation behind this PR is that `algebra.algebra.tower` is a relatively fundamental and popular file to import (especially since it used to contain `is_scalar_tower`), but its import tree also includes relatively complicated files such as `ring_theory.ideal.operations`. By splitting off these less popular dependencies we can save quite a bit of complexity in the import graph.



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
@bors
Copy link

bors bot commented Nov 15, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/algebra): reduce imports for algebra.algebra.tower [Merged by Bors] - chore(algebra/algebra): reduce imports for algebra.algebra.tower Nov 15, 2022
@bors bors bot closed this Nov 15, 2022
@bors bors bot deleted the split-algebra-tower branch November 15, 2022 21:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants