I am trying to make
coq.extraction work and could not make it work for the simplest example. I just have one module (.v) and want to extract and compile OCaml from it. If Is there a simple example of how this is supposed to work? Thanks!
Internal error I am getting https://github.com/ocaml/dune/issues/6105. Then according to https://github.com/ocaml/dune/issues/4158 the coq.theor and coq.extraction should be in separate directories. If I put them side-by side, the extraction could not find theory. If I create extraction directory under coq theory directory it complains abut "remapped to DuneExtraction" and that generated files not found.
Phew, I made it work but I think documentation may use an example.
@Vadim Zaliva If you could come up with a small example and make a PR to ocaml/dune that would be most welcome!
Last updated: Mar 02 2024 at 14:01 UTC