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.
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.
That unfortunate. So if I need binary serialization, I need to use flocq instead?
Not instead, on top. There is a compatibility layer in Flocq.
@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
(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)
@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.
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.
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: Jan 27 2023 at 01:03 UTC