[Caml-list] Connecting extracted OCaml code from Rocq to zarith library

[Caml-list] Connecting extracted OCaml code from Rocq to zarith library

[mukesh tiwari]

Hi all, 

I am hoping to find some Dune experts. I am currently working on a Rocq project [1] that builds with Dune, and I am trying to extract it into OCaml where Rocq integer (Z) is mapped to ExtrOcamlZBigInt [2]. However, I am getting the following error and wondering how to resolve this. 

File "src/Extraction/dune", lines 2-7, characters 1-197:
2 |  (coq.extraction
3 |   (prelude Extraction)
4 |   (extracted_modules SigmaIns Sigma Datatypes Vector
5 |    VectorDef Zpstar BigInt)
6 |   (theories ExtLib Stdlib Utility Crypto Algebra
7 |    Probability Examples))
Error: Rule failed to generate the following targets:
- src/Extraction/Sigmalib/BigInt.ml
- src/Extraction/Sigmalib/BigInt.mli

In the past, I have used Makefile [3] where I linked a Big.ml [4] file to num or zarith library but I don’t know how to do this with Dune. I have also posted this question on Zulip so feel free to answer there as well [5]. 

Best, 
Mukesh 

[1] https://github.com/mukeshtiwari/SigmaProtocol/blob/master/src/Extraction/dune 
[2] https://github.com/mukeshtiwari/SigmaProtocol/blob/master/src/Extraction/Sigmalib/Extraction.v#L3
[3] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/Makefile#L34
[4] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/big.ml
[5] https://rocq-prover.zulipchat.com/#narrow/channel/237977-Rocq-users/topic/Unbound.20value.20iff_reflect