search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

Fix w.r.t. math-comp/math-comp#601 which renames `eq_sorted(_irr)` to `sorted_eq(_irr)` #24

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

We are about to rename eq_sorted lemmas to sorted_eq to address a naming inconsistency in MathComp (see https://github.com/math-comp/math-comp/pull/601#issuecomment-705046342). Unfortunately, this deprecation breaks fcsl-pcm and lemma-overloading because the deprecation facility of MathComp does not support the (ident := term) syntax for explicit applications. As a workaround, I propose to use @ syntax instead.

clayrat commented 3 years ago

Looks sensible, any reason this is marked as a draft?

Also, do you have an estimate of which version of mathcomp the deprecation will take place in, will that be 1.12 already?

pi8027 commented 3 years ago

Looks sensible, any reason this is marked as a draft?

Since I finished documentation work for math-comp/math-comp#601 (but I'm still waiting for review there), I marked this PR as ready for review.

Also, do you have an estimate of which version of mathcomp the deprecation will take place in, will that be 1.12 already?

Since now it targets 1.12, I hope it will be included in 1.12.

germanD commented 3 years ago

Since now it targets 1.12, I hope it will be included in 1.12.

Hi @pi8027. Let me clarify the meaning of deprecation in your answer: do you mean that you just intend to merge #601 for the 1.12 milestone, or that, once it is merged, you also expect to remove the corresponding deprecate notations, e.g.:

Notation "@ 'eq_sorted_lt'" := (deprecate eq_sorted_lt sorted_eq_lt)
  (at level 10, only parsing) : fun_scope.

for the same release milestone?

germanD commented 3 years ago

LGTM!

pi8027 commented 3 years ago

@germanD No. These deprecation notations such as "@ 'eq_sorted_lt'" will be included in the 1.12 release so that libraries depending on MathComp can support both ~1.11 and 1.12. Then it will be removed at some point between 1.12 and 1.13.

clayrat commented 3 years ago

@pi8027 thank you!

germanD commented 3 years ago

Indeed, thanks @pi8027!