Stream: Dune devs & users

Topic: confused by coq.extraction


view this post on Zulip Vadim Zaliva (Aug 25 2022 at 22:36):

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!

view this post on Zulip Vadim Zaliva (Aug 25 2022 at 22:40):

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.

view this post on Zulip Vadim Zaliva (Aug 25 2022 at 23:10):

Phew, I made it work but I think documentation may use an example.

view this post on Zulip Ali Caglayan (Aug 30 2022 at 11:43):

@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: Jan 30 2023 at 17:03 UTC