[ breaking ] change fieldname _≟_ to _≈?_ in IsDecEquivalence#2952
[ breaking ] change fieldname _≟_ to _≈?_ in IsDecEquivalence#2952jamesmckinna wants to merge 21 commits intoagda:masterfrom
_≟_ to _≈?_ in IsDecEquivalence#2952Conversation
| ≡?-≡-refl : (i : Fin n) → (i ≡? i) ≡ yes refl | ||
| ≡?-≡-refl _ = ≡?-≡ refl |
There was a problem hiding this comment.
Given all the new deprecations, there is an additional opportunity here to reconcile the inconsistent naming between Fin and Nat of this and other properties, but that may be too much additional weight for this PR to carry.
There was a problem hiding this comment.
I'd be in favour of doing this sort of thing in this PR
There was a problem hiding this comment.
Well, we need to agree on our preferred name, and I can't quite remember where we last discussed this! Maybe git blame is the answer...
There was a problem hiding this comment.
So... #2740 seems to establish the names in Data.Fin.Properties as canon/ical, with the names for Nat being legacy and up for renaming+deprecation... so let's try to do this here!
There was a problem hiding this comment.
Please check my recent commits carefully: I think that I've got the names, and the CHANGELOG correct, given that the last round of names were also part of v2.4!!!
| _≟_ = _≈?_ | ||
| {-# WARNING_ON_USAGE _≟_ | ||
| "Warning: _≟_ was deprecated in v2.4. | ||
| Please use _≈?_ instead. " | ||
| #-} |
There was a problem hiding this comment.
I assumed that this was the best way to keep the 'old' name around, but it does then entail some gymnastics in order to ensure that deprecated name is nevertheless correctly exported everywhere. Hopefully it all works in a non-breaking way!
There was a problem hiding this comment.
NB as usual, the warning doesn't seem to fire correctly in client modules...
| open IsDecPreorder isDecPreorder public | ||
| using (module Eq) | ||
|
|
||
| open Eq public using (_≟_) |
There was a problem hiding this comment.
This being an example of the need to re-export, in spite of the deprecation.
So perhaps this should have additional commentary to mark it for deprecation... later
| infix 4 _≟-Lit_ _≟-Name_ _≟-Meta_ _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_ | ||
| _≟-Pattern_ _≟-ArgPatterns_ | ||
|
|
There was a problem hiding this comment.
I hated modifying this whole block of v1.3-era deprecations, but hopefully once we remove them completely, this will all have been just a bad dream...
| ; pat-lit-injective to lit-injective | ||
| ; _≟-Patterns_ to _≟s_ | ||
| ; _≟-Pattern_ to _≟_ | ||
| ; _≡?-Patterns_ to _≟s_ |
There was a problem hiding this comment.
Should this renaming also be brought in line with the rest of the PR? AFAICT, this module ought perhaps to be stripped out in favour of the 'new' refactoring of the Reflection API under Reflection.AST.Term but I didn't want to break something which was already fixed, or vice versa!
It would be good if someone had another look at what's going on here...
There was a problem hiding this comment.
I've never really dug into any parts of Reflection, so I can't really say. This one line does rather stick out now.
|
Ugh. I didn't catch them all, esp. under |
|
While I agree this should be done, this is unavoidably a breaking change as you need to change how you define the Therefore according to our backwards compatibility policy, this definitely needs to be |
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
The tediousness of this PR, coupled with the fact that a handful of times in 188, really non-trivial decisions had to be made, made reviewing quite something.
I did not see anything that seemed incorrect.
|
I agree with @MatthewDaggitt 's analysis, so I do now wonder whether the 'simpler' PRs hanging off this one (such as #2955 , just merged) maybe ought to be paused, or should we carry on with migrating to the And, given that it's moving to v3.0, I'll try to lift out a |
Thanks for you patience @JacquesCarette ! It was pretty tedious to do, esp. as many many changes were not flagged as necessary by generating deprecation warnings... and yes, the few non-trivial changes, some of which being 'tricky' (under But maybe if we go wholesale for breaking v3.0 version, then we can try to be less accommodating wrt deprecations? UPDATED: @JacquesCarette reading your recent comments on LLM-generated content, apologies for making this PR harder to review than to write... but begging indulgence, on my own behalf, if nothing else ;-) |
|
Re-running the one failed job as it seemed like a temporary hiccup. And no worries @jamesmckinna : I accept the burden of being an Open Source maintainer willingly. And that includes sometimes reviewing tedious but important PRs. |
5 participants
This tackles the name change discussed in #2845 , plus a lot of knock-ons for consistency's sake.
I've tagged it
breaking, even though I think I've caught all the possible deprecations, because we change a fieldname. But maybe it's 'just' anon-backwards compatiblechange... ??? It seems as though it would be good to try to do this for v2.4, but perhaps it must wait for v3.0.No
CHANGELOGyet as a consequence... butstyle-guideupdated.UPDATED: now there are
CHANGELOGentries, but I just can't face writing out the deprecations for every module touched, so some kind of summary paragraph would (probably) be better. Plus: some of the 'deprecations' are for lemmas introduced in earlier v2.4 PRs, so I may well not have things quite right... yet.NB.
Algebra.Solver, I've also corrected the fixity of the definedDecidableEqualityonNormalforms from 5 to 4, but I hope that this is harmless!Relation.Binary.Construct.Intersection.decidableas discussed in Use consistent names forDecidablecombinators (#2842 redux) #2846 )