Rudi Grinberg (May 31 2022 at 16:09): Rudi Grinberg (May 31 2022 at 16:09):@Li-yao dune now has support for extraction. I noticed that you extract some tests in InteractionTrees with makefiles, perhaps you can do it in dune now
Karl Palmskog (May 31 2022 at 16:39):I think you mean: "Dune now has support for composition with user-contrib-installed Coq libraries"?
Ali Caglayan (May 31 2022 at 17:49):@Karl Palmskog I think he meant extraction, we didn't support user-contrib yet.
Li-yao (May 31 2022 at 19:13):I already use that part of dune :) There is one annoyance with recursive separate extraction, where all extracted modules have to be listed, but the fault really lies with extraction rather than dune.
Ali Caglayan (May 31 2022 at 19:36):I am in favor of supporting an output directory for extraction in Coq.
Ali Caglayan (May 31 2022 at 19:37):What is dumb today is that we cannot do this since extraction is a plugin and therefore has no business asking for command line args.
Ali Caglayan (May 31 2022 at 19:37):We could instead ask for an env var
Ali Caglayan (May 31 2022 at 19:37):or absorb extraction as core coq finally and support it from the cli
Ali Caglayan (May 31 2022 at 19:38):On the dune side, we can support directory targets for extraction
Ali Caglayan (May 31 2022 at 19:38):So you just have to say: my extracted code will go in this dir.
Ali Caglayan (May 31 2022 at 19:38):Dune will be able to use all the ml files that get generated in there
Rudi Grinberg (May 31 2022 at 20:11):you could also consider making extraction a separate binary if it would be possible to strip many dependencies from it
Ali Caglayan (May 31 2022 at 20:16):I don't know if it would be possible to separate an extraction binary. The extraction commands are quite complicated: https://coq.inria.fr/refman/addendum/extraction.html
Rudi Grinberg (May 31 2022 at 21:05):Sure, it was just a thought.
Emilio Jesús Gallego Arias (Jun 01 2022 at 12:07):It is possible to make extraction a binary, it should not be hard unless I'm missing something. Similiar to coqnative
Last updated: Oct 13 2024 at 01:02 UTC