[Coq-Club] big.ml

[Vadim Zaliva]

I have a question about using ExtrOcamlBigIntConv. The generated code
depends on big.ml wrapper which is also mentioned in the documentation. Am
I supposed to copy big.ml from Coq source tree to my project? It is not
installed via OPAM as part of Coq package.

--
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: [phone]

[Enrico Tassi]

Am I supposed to copy big.ml from Coq source tree to my project?

As of today, this is the only solution :-/

You may also try to give a look at

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

that will let you write

ocamlfind opt -package coq.extraction.runtime yourcode.ml

in order to compile your extracted code.

The PR is promising, but seems to need some more work. Showing your
interest in there may help motivating the authors.

Best,

[Ana]

For what it's worth, my team is also interested in this library.

Best,
Ana Borges

Post by Enrico Tassi

Am I supposed to copy big.ml from Coq source tree to my project?

As of today, this is the only solution :-/
You may also try to give a look at
https://github.com/coq/coq/pull/8252
that will let you write
ocamlfind opt -package coq.extraction.runtime yourcode.ml
in order to compile your extracted code.
The PR is promising, but seems to need some more work. Showing your
interest in there may help motivating the authors.
Best,
--
Enrico Tassi