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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore(data/nat/cast): remove spurious imports #17336

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - chore(data/nat/cast): remove spurious imports #17336

wants to merge 6 commits into from

Conversation

semorrison
Copy link
Collaborator

This removes some spurious dependencies on data.set.lattice and data.set.pointwise amongst others.

Open in Gitpod

@semorrison semorrison 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. labels Nov 4, 2022
@PatrickMassot
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Nov 4, 2022

✌️ 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.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed 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. labels Nov 4, 2022
@semorrison
Copy link
Collaborator Author

bors merge

@github-actions 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 4, 2022
@bors
Copy link

bors bot commented Nov 4, 2022

Canceled.

@semorrison semorrison added awaiting-CI The author would like to see what CI has to say before doing more work. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Nov 4, 2022
@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 4, 2022
@semorrison
Copy link
Collaborator Author

bors merge

@github-actions 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 5, 2022
bors bot pushed a commit that referenced this pull request Nov 5, 2022
@semorrison
chore(data/nat/cast): remove spurious imports (#17336)
864c489 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Nov 5, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 5, 2022
@semorrison
chore(data/nat/cast): remove spurious imports (#17336)
71493b3 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Nov 5, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 5, 2022
@semorrison
chore(data/nat/cast): remove spurious imports (#17336)
68d07fd 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Nov 5, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 5, 2022
@semorrison
chore(data/nat/cast): remove spurious imports (#17336)
d7e57d0 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Nov 5, 2022

Build failed (retrying...):

@bors
Copy link

bors bot commented Nov 5, 2022

Canceled.

@fpvandoorn
Copy link
Member

By elimination I'm quite sure that this PR caused the build failures.

@semorrison semorrison added awaiting-CI The author would like to see what CI has to say before doing more work. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Nov 5, 2022
@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 6, 2022
@fpvandoorn
Copy link
Member

fpvandoorn commented Nov 6, 2022 •
edited

Let's hope it's better now!

bors merge

(or are we trying to merge at higher priority?)

@github-actions 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 6, 2022
@semorrison semorrison mentioned this pull request Nov 6, 2022
Closed
bors bot pushed a commit that referenced this pull request Nov 6, 2022
@semorrison @fpvandoorn
chore(data/nat/cast): remove spurious imports (#17336)
0fa08d9 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link

bors bot commented Nov 6, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 6, 2022
@semorrison @fpvandoorn
chore(data/nat/cast): remove spurious imports (#17336)
c1c9455 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link

bors bot commented Nov 6, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 6, 2022
@semorrison @fpvandoorn
chore(data/nat/cast): remove spurious imports (#17336)
dc5a527 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link

bors bot commented Nov 6, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 6, 2022
@semorrison @fpvandoorn
chore(data/nat/cast): remove spurious imports (#17336)
e67f58c 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link

bors bot commented Nov 6, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 6, 2022
@semorrison @fpvandoorn
chore(data/nat/cast): remove spurious imports (#17336)
ed04b51 
This removes some spurious dependencies on `data.set.lattice` and `data.set.pointwise` amongst others. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link

bors bot commented Nov 6, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(data/nat/cast): remove spurious imports [Merged by Bors] - chore(data/nat/cast): remove spurious imports Nov 6, 2022
@bors bors bot closed this Nov 6, 2022
@bors bors bot deleted the data_nat_cast branch November 6, 2022 19:07
bors bot pushed a commit that referenced this pull request Nov 6, 2022
@semorrison @urkud @YaelDillies
refactor(*): supremum of several recent refactoring PRs (#17381)
87489e9 
This is the supremum of

* #17376
* #17375
* #17374
* #17362
* #17355
* #17349
* #17347
* #17338
* #17336

with imports fixed up to accommodate all the overlapping changes to imports.





Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
bors bot pushed a commit that referenced this pull request Nov 6, 2022
@semorrison @urkud @YaelDillies
refactor(*): supremum of several recent refactoring PRs (#17381)
f770787 
This is the supremum of

* #17376
* #17375
* #17374
* #17362
* #17355
* #17349
* #17347
* #17338
* #17336

with imports fixed up to accommodate all the overlapping changes to imports.





Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@semorrison @PatrickMassot @fpvandoorn