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

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

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/

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.)

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?

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?

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?

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.

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: Feb 05 2023 at 07:03 UTC