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(Algebra): add missing deprecation dates #12598

Closed
wants to merge 27 commits into from
Closed

[Merged by Bors] - chore(Algebra): add missing deprecation dates #12598

wants to merge 27 commits into from

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented May 2, 2024

@grunweg
chore(Algebra/BigOperators): add missing deprecation dates
0fa79be 
One additivised lemma was missing a deprecation.
@grunweg
chore(Algebra): more deprecation dates
a6a4bb4
@grunweg
chore(Algebra): more dates; reformat one lemma
d754203 
Many of these are long-deprecated declarations which are still around in mathlib.
In one instance, the additivised version wasn't deprecated yet.

This is exhaustive in this directory --- with one exception: I'm not adding explicit dates
to all deprecated lemmas involving bit0/1 (which were deprecated during the port).
@grunweg
fixup! Algebra dates; 2022-12-03 had a typo
393e239
@grunweg
fix(Algebra), typo in dates (2022 -> 2024)
4deac3c
@grunweg
chore: silence new deprecation following to_additive;
35dcbf2 
fixing this is slightly too hard right now
@grunweg
chore: silence new deprecation following to_additive;
b7aecdb 
fixing this is slightly too hard right now
@grunweg
Fixup
68dd62e
@grunweg grunweg added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) tech debt tracking cross-cutting technical debt labels May 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label May 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 14, 2024
@grunweg grunweg mentioned this pull request May 16, 2024
Closed
@grunweg grunweg removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 17, 2024
@grunweg grunweg mentioned this pull request May 24, 2024
Closed
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label May 24, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@urkud
Copy link
Member

urkud commented May 26, 2024

Thanks! 🎉
bors merge

mathlib-bors bot pushed a commit that referenced this pull request May 26, 2024
@grunweg
chore(Algebra): add missing deprecation dates (#12598)
f3612d5
@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 26, 2024
@grunweg
Copy link
Collaborator Author

grunweg commented May 26, 2024

Thanks for the fast review!

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 26, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Algebra): add missing deprecation dates [Merged by Bors] - chore(Algebra): add missing deprecation dates May 26, 2024
@mathlib-bors mathlib-bors bot closed this May 26, 2024
@mathlib-bors mathlib-bors bot deleted the MR-deprecates-dates-algebra branch May 26, 2024 07:11
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@grunweg @callesonne
chore(Algebra): add missing deprecation dates (#12598)
87de653
js2357 pushed a commit that referenced this pull request Jun 18, 2024
@grunweg @js2357
chore(Algebra): add missing deprecation dates (#12598)
6525a07
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
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc) tech debt tracking cross-cutting technical debt
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@grunweg @leanprover-community-mathlib4-bot @urkud