Stream: Miscellaneous

Topic: Extraction of Zarith


view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Mar 28 2021 at 14:29):

The comment is outdated. The second file actually targets Zarith.

view this post on Zulip 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/

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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: Aug 14 2022 at 12:03 UTC