Connecting extracted OCaml code from Rocq to zarith library
mukesh tiwari <[email protected]> Mon, 18 Aug 2025 10:07:35 +0100
| Newsgroups | gmane.comp.lang.caml.inria,gmane.science.mathematics.logic.coq.club |
|---|---|
| Message-ID | <[email protected]> |
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