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] - refactor(*): rename some declarations ending with '' #9504

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - refactor(*): rename some declarations ending with '' #9504

wants to merge 11 commits into from

Conversation

semorrison
Copy link
Collaborator

Open in Gitpod

eric-wieser
eric-wieser reviewed Oct 2, 2021
View reviewed changes
src/algebra/algebra/basic.lean

-- from now on, we don't want to use the following instance anymore
attribute [instance, priority 0] algebra.to_has_scalar

lemma smul_def (r : R) (x : A) : r • x = algebra_map R A r * x :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it might be important that this appears after attribute [instance, priority 0] algebra.to_has_scalar, as it affects which instance appears in the statement.

Perhaps the solution is just to make the double-primed version private?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure how it could be important, if it has no effect downstream. I think historically this did matter, but the definitions have changed since. In fact, I think we can just remove the priority 0 statement here, so I've pushed this change for CI to check. If it works I'll mention this in the PR description.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok. Leaving this instance in places causes painful deterministic timeouts downstream, that I don't want to debug. Instead I've made this private as you suggest, and left some comments. This is pretty gross. :-(

@bryangingechen bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 6, 2021
@semorrison semorrison added the awaiting-CI The author would like to see what CI has to say before doing more work. label Oct 9, 2021
@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 Oct 18, 2021
@semorrison semorrison 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 Oct 18, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 19, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 19, 2021
jcommelin
jcommelin approved these changes Oct 19, 2021
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 Oct 19, 2021
bors bot pushed a commit that referenced this pull request Oct 19, 2021
@semorrison
refactor(*): rename some declarations ending with '' (#9504)
e004360 




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

bors bot commented Oct 19, 2021

Build failed:

@bryangingechen
Copy link
Collaborator

Failure seems spurious.
bors r+

@bryangingechen
Copy link
Collaborator

bors somehow crashed.
bors r+

bors bot pushed a commit that referenced this pull request Oct 19, 2021
@semorrison
refactor(*): rename some declarations ending with '' (#9504)
72cb2e8 




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

bors bot commented Oct 19, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(*): rename some declarations ending with '' [Merged by Bors] - refactor(*): rename some declarations ending with '' Oct 19, 2021
@bors bors bot closed this Oct 19, 2021
@bors bors bot deleted the double_primes branch October 19, 2021 23:27
@eric-wieser eric-wieser added the hacktoberfest-accepted Without this label hacktoberfest is scared off by bors label Oct 26, 2021
ericrbg pushed a commit that referenced this pull request Nov 9, 2021
@semorrison @ericrbg
refactor(*): rename some declarations ending with '' (#9504)
3a2527b 




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
hacktoberfest-accepted Without this label hacktoberfest is scared off by bors 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
4 participants
@semorrison @bryangingechen @eric-wieser @jcommelin