Stream: Coq users

Topic: Extraction using ExtrOcamlNatBigInt


view this post on Zulip Rudy Peterson (Sep 07 2021 at 22:15):

To extract my program I'm using ExtrOcamlNatBigInt.

However upon compilation I get errors such as:

File "coq/extract/Datatypes.mli", line 2, characters 25-36:
2 | val length : 'a1 list -> Big.big_int
                             ^^^^^^^^^^^
Error: Unbound module Big

I'm not sure how to import module Big; when I list it in the libraries stanza in my dune file it doesn't know what Big is.

How does one use ExtrOcamlNatBigInt?

Thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2021 at 22:17):

I think that module is supposed to extract to zarith, tho you may need to include a copy of the big.ml file that lives in plugins/extraction

view this post on Zulip Rudy Peterson (Sep 07 2021 at 22:20):

Emilio Jesús Gallego Arias said:

I think that module is supposed to extract to zarith, tho you may need to include a copy of the big.ml file that lives in plugins/extraction

Is there a way to import big.ml or should I just create it and copy & paste the its contents?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2021 at 22:27):

I seems to recall that there was a bug open about it, I'd recommend just dropping the big.ml for now

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2021 at 22:27):

other option would be to link the plugin, which seems to include it, but I don't recommend that, I'm checking Coq's bug tracker

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2021 at 22:28):

You can see it is a really minimal wrapper

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2021 at 22:28):

https://github.com/coq/coq/blob/master/plugins/extraction/big.ml

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2021 at 22:33):

That's the relevant PR https://github.com/coq/coq/pull/8252


Last updated: Oct 13 2024 at 01:02 UTC