[primitive floats] Deprecate frexp and ldexp

[proux01]

Now that we have signed primitive integers, we would like to use them
in frexp and ldexp but the name was taken by functions with exponent
in Z. These functions are renamed Z.frexp and Z.ldexp so that frexp and
ldexp could later be added with signed primitive integer exponent.

• Added changelog.

[proux01]

Cc @erikmd and @silene who may have an opinion.

[silene]

I am confused. I thought frexp and ldexp were using biased primitive integers. It was not as good as signed primitive integers, but certainly not as bad as Z numbers.

[proux01]

Those are called frshiftexp and ldshiftexp.

[erikmd]

Thanks @proux01 for opening this.
I agree with the fact that it'll be nice to put forth the primitive signed integers over mere Z integers!

However, I am wondering whether one such renaming could be done in a more "modular" way (like the BinInt theory)?

I mean, renaming FloatOps.frexp to something like FloatOps.Z.frexp

[proux01]

Indeed, done.

[erikmd]

Thanks @proux01, this looks fine (except two lines that needs an update)

[erikmd]

Thanks, it seems the changelog is the last missing part

[proux01]

@erikmd done, would you be the assignee?

[erikmd]

Sure. If no one objects, I propose to merge this cleanup PR on tomorrow Wednesday evening.

[erikmd]

@coqbot merge now

[coqbot-app]

@erikmd: You can't merge this PR because you're not a member of the @coq/pushers team.

[erikmd]

@silene can you be the assignee then?

[ejgallego]

Oh, let us fix this @erikmd

[ejgallego]

@erikmd not sure what's the best team for "primitive floats maintainers", I've added you to the vm-native-maintainers for now, but let's refine this if needed; please try again.

[ejgallego]

And sorry for the annoyance.

[erikmd]

@erikmd not sure what's the best team for "primitive floats maintainers", I've added you to the vm-native-maintainers for now, but let's refine this if needed

Indeed; thank you @ejgallego!

And sorry for the annoyance.

No worries! (I think the infrastructure was refactored since my last merge - #14688 (comment))

[erikmd]

@coqbot merge now

[proux01]

Thanks @erikmd (and thanks @ejgallego )