Vadim Zaliva (Nov 01 2022 at 02:05): Vadim Zaliva (Nov 01 2022 at 02:05):Is it possible to extract from PrimFloat value to IEEE 64-bit binary representation and convert back 64 bits to PrimFloat? For example, using Z as a bit sequence and assuming the correct length I need:
Definition float_of_bits: Z -> float.
Definition bits_of_float: float -> Z.
I know how to do this in Flocq but I was hoping to avoid additional dependency and use PrimFloat instead.
Pierre Roux (Nov 01 2022 at 08:12):No, the goal when adding primitive floats was to copy the minimum amount of material from Flocq to the stdlib, everything else remains in Flocq. Note that your functions are not bijective as NaN has multiple binary representations.
Vadim Zaliva (Nov 01 2022 at 19:07):That unfortunate. So if I need binary serialization, I need to use flocq instead?
Pierre Roux (Nov 01 2022 at 20:03):Not instead, on top. There is a compatibility layer in Flocq.
Karl Palmskog (Nov 01 2022 at 20:05):@Vadim Zaliva genuine question, do you think there is any general issue with depending on packages besides stdlib nowadays? One of our goals with the Coq Platform is to lower barriers for depending on things like Flocq in Coq projects
Karl Palmskog (Nov 01 2022 at 20:06):(so for example, each release of the Platform will have a corresponding Flocq that doesn't radically diverge from the last, so library devs who depend on Flocq can simply tell their users to install the latest Coq Platform)
Vadim Zaliva (Nov 01 2022 at 22:29):@Karl Palmskog how much of a problem a new dependency is, in my experience, depends on how well-maintained/supported the package is. It is manageable if it is included in OPAM and updated to support recent releases of Coq. In this particular case, it is a pity to bring such new dependency for a such a simple basic feature. Since PrimeFloat is based on IEEE 64-binary, the omission of external encoding/decoding functions sounds like an oversight. I am pretty sure they are already present in the internal implementation. Exposing them should be OK, as the binary64 format is well standardized.
Pierre Roux (Nov 01 2022 at 22:52):Well, I would consider Flocq as one of the most well maintained, long lasting compatibility library after the stdlib. I'm not sure you got the purpose of primitive floats: they are not here to provide a formalization of floats (that's what Flocq is for), their only goal is to provide efficient computation for reflexive proofs. If you don't need that, just go for Flocq.
Karl Palmskog (Nov 02 2022 at 10:51):I think it's accurate to say that how we work in the Coq Platform and elsewhere in the ecosystem is mainly by not growing the Stdlib with new theories or making big changes to existing theories, but rather by adding libraries to the Coq Platform and consolidating existing libraries and functionality there.
Last updated: Sep 30 2023 at 06:01 UTC