Vadim Zaliva (Aug 25 2022 at 22:36): 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!
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.
Vadim Zaliva (Aug 25 2022 at 23:10):Phew, I made it work but I think documentation may use an example.
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: Oct 13 2024 at 01:02 UTC