Stream: Miscellaneous

Topic: Extraction to Ocaml ints


view this post on Zulip Bas Spitters (Sep 08 2020 at 16:41):

I understand that ocaml moved to zarith and away from num
https://github.com/ocaml/num
https://github.com/ocaml/Zarith
However, these still seem to extract to num:
https://coq.inria.fr/distrib/current/stdlib//Coq.extraction.ExtrOcamlZBigInt.html
Is my understanding correct? Does anyone have a translation to Zarith laying around?

List of Extraction layers:
https://coq.inria.fr/library/index_global_E.html

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 16:41):

Indeed there is a PR open

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 16:42):

https://github.com/coq/coq/pull/8252

view this post on Zulip Bas Spitters (Sep 08 2020 at 16:56):

Thanks! A very timely question I see :-)

view this post on Zulip Théo Zimmermann (Sep 08 2020 at 17:12):

The PR has been opened for 2 years though...

view this post on Zulip Bas Spitters (Sep 09 2020 at 11:52):

We've managed to convert our code to Int63 . How to extract those to ocaml? Is there a template available? @Maxime Dénès ?

view this post on Zulip Bas Spitters (Sep 09 2020 at 11:52):

Sorry found it:
https://coq.inria.fr/library/Coq.extraction.ExtrOCamlInt63.html


Last updated: Aug 14 2022 at 11:02 UTC