Bas Spitters (Mar 28 2021 at 14:26): Bas Spitters (Mar 28 2021 at 14:26):The stdlib provides two ways of extracting Zarith to Ocaml. The first to Int (which is crude), the second to Num (which I understand is deprecated)
https://coq.inria.fr/library/Coq.extraction.ExtrOcamlZInt.html
https://coq.inria.fr/library/Coq.extraction.ExtrOcamlZBigInt.html
Why not extract to Zarith?
https://github.com/ocaml/Zarith
https://github.com/ocaml/num
Guillaume Melquiond (Mar 28 2021 at 14:29):The comment is outdated. The second file actually targets Zarith.
Bas Spitters (Mar 28 2021 at 14:31):Thanks! Will you fix the comment, or shall I report it somewhere?
BTW Extraction seems to be lacking from the index:
https://coq.inria.fr/library/
Guillaume Melquiond (Mar 28 2021 at 14:56):Bas Spitters said:
BTW Extraction seems to be lacking from the index:
That is on purpose. (But I have no idea what that purpose is.)
Bas Spitters (Mar 28 2021 at 15:50):We're running a 10h computation of extracted ocaml code. These are big numbers, so we're using Zarith (GMP) in an essential way.
Did anyone try to make a crude version of GMP in Coq based on the machine integers?
Guillaume Melquiond (Mar 28 2021 at 16:06):Bas Spitters said:
Did anyone try to make a crude version of GMP in Coq based on the machine integers?
That is what the Bignums library is, isn't it?
Bas Spitters (Mar 28 2021 at 16:45):Yes, of course. :face_palm:
I believe they've been developed after the machine integer paper.
Did anyone ever write a paper, or a short report on them?
Extraction files, like for Zarith, seem to be missing, but I guess they are not hard to write.
Are there any statistics relating their performance to the ocaml numbers?
Guillaume Melquiond (Mar 28 2021 at 17:06):Why do you need extraction files? If you are going to extract BigZ to Zarith, then there is not much point in using BigZ in the first place, just use plain Z.
Bas Spitters (Mar 28 2021 at 17:19):We'd like to compute in Coq, but are not sure it is feasible. So, as a first approximation we extracted Zarith. Now, we'd like to move to BigZ, but then it would still be nice to experiment with the extracted code. So, it's just convenience. In any case, it should be easy to write.
Last updated: Nov 29 2023 at 21:01 UTC