Stream: Dune devs & users

Topic: Extraction support


view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 31 2022 at 16:39):

I think you mean: "Dune now has support for composition with user-contrib-installed Coq libraries"?

view this post on Zulip Ali Caglayan (May 31 2022 at 17:49):

@Karl Palmskog I think he meant extraction, we didn't support user-contrib yet.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 31 2022 at 19:36):

I am in favor of supporting an output directory for extraction in Coq.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 31 2022 at 19:37):

We could instead ask for an env var

view this post on Zulip Ali Caglayan (May 31 2022 at 19:37):

or absorb extraction as core coq finally and support it from the cli

view this post on Zulip Ali Caglayan (May 31 2022 at 19:38):

On the dune side, we can support directory targets for extraction

view this post on Zulip Ali Caglayan (May 31 2022 at 19:38):

So you just have to say: my extracted code will go in this dir.

view this post on Zulip Ali Caglayan (May 31 2022 at 19:38):

Dune will be able to use all the ml files that get generated in there

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (May 31 2022 at 21:05):

Sure, it was just a thought.

view this post on Zulip 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: Mar 29 2024 at 14:01 UTC