[Merged by Bors] - chore(Init): add deprecation dates; remove long-deprecated items #12347
Conversation
Bitte geben Sie eine Commit-Beschreibung für Ihre Änderungen ein. Zeilen,
trans_rel_left was used slightly, but there were easy to rewrite.
grunweg
added
the
awaiting-review
|
@YaelDillies I hope this didn't create duplicate work. In any case, I guess you may find this interesting. |
| def nthLe (l : List α) (n) (h : n < l.length) : α := get l ⟨n, h⟩ | ||
| #align list.nth_le List.nthLe | ||
|
|
||
| set_option linter.deprecated false in | ||
| @[deprecated] | ||
| @[deprecated] -- 2023-01-05 |
There was a problem hiding this comment.
I think anything that's been deprecated for > 6 months is fair game to remove
There was a problem hiding this comment.
I wasn't sure if this one was still used. (There are many uses of deprecated lists stuff still.) Let me check...
There was a problem hiding this comment.
It turns out this one can be removed; I've split these into #12350.
There was a problem hiding this comment.
(That PR is now ready for review :-))
| @[deprecated and_comm] theorem and_comm' (a b) : a ∧ b ↔ b ∧ a := and_comm | ||
| #align and.comm and_comm | ||
| #align and_comm and_comm' | ||
| #align and_comm and_comm | ||
|
|
||
| @[deprecated and_assoc] theorem and_assoc' (a b) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := and_assoc | ||
| #align and_assoc and_assoc' | ||
| #align and_assoc and_assoc |
There was a problem hiding this comment.
I think these two you should keep simply because they help teach people how the deprecation system works. Certainly this is how I learned about it.
Maybe @digama0 has a different opinion, though.
There was a problem hiding this comment.
In general, I'd rather have documentation in more discoverable places (than some undiscoverable corner of mathlib). I'm not sure if such a standard place already exists, though.
There was a problem hiding this comment.
Nono, this is not about documentation. This is about the fact that ported code often contains and_comm' or and_assoc' and therefore the people porting the code are confronted with an (easy) task of undeprecation which teaches them how it works.
There was a problem hiding this comment.
We're going to need to do something special if we want specific deprecations to last past the cutoff date.
There was a problem hiding this comment.
To be fair, I'm not sure how much more code we're going to port. So maybe this is moot.
There was a problem hiding this comment.
💡 Could the porting wiki be a place to mention this? After all, this is where I'd look if I were to port code and want advice.
There was a problem hiding this comment.
Sure yeah, I'm happy with that!
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
All removed items are virtually unused in mathlib and have been deprecated for over a year.
Each commit can be reviewed individually; note that deprecation dates are first added
for all lemmas; and subsequently some deprecated lemmas are removed.
This change overlaps with #12350 (which removes a bunch of deprecated items about lists); this PR can go in regardless.