Stream: Dune devs & users

Topic: Extraction with dune


view this post on Zulip Yannick Zakowski (Feb 06 2022 at 20:35):

Hi everyone,
I'm trying to port Vellvm (https://github.com/vellvm/vellvm/tree/opam-release) to build using dune, and have little experience with it.
I am a bit confused when it comes to extraction: monolithic extraction is not an option for us, and Recursive Extraction Library leads to the extraction of 148 ml modules.
However, the coq.extraction stanza requests "an exhaustive list of OCaml modules extracted", and seems to mean it from my early attempts. Am I really expected to list the 148 modules? Is there no other way?

view this post on Zulip Notification Bot (Feb 06 2022 at 20:52):

This topic was moved here from #Coq users > Extraction with dune by Karl Palmskog

view this post on Zulip Yannick Zakowski (Feb 07 2022 at 07:27):

Ah I have been pointed out to this thread from two years ago that seems to confirm that indeed that was the situation: https://github.com/ocaml/dune/issues/2178
Are there been any evolution on this front by any chance?

view this post on Zulip Karl Palmskog (Feb 07 2022 at 08:23):

not to my knowledge.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:29):

Not yet indeed, unfortunately we didn't implement support to find the list of modules automatically

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:29):

however that would be a great topic to work on in the upcoming Hackathon

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:29):

It is not hard to do at all

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:30):

The reason it works like this now

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:30):

is because dune needs to learn what files are generated, as to prevent "stale" files

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:30):

so for example, if you are doing bisect, Dune will clean up files that are not generated anymore

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:30):

as to preserve the soundness of the incremental build

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:31):

A workaround for now is to generate the dune file with a little sed script that creates the list of targets

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:31):

in Dune 3.0 it should be possible to actually use (:include gen_modules.sexp)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:32):

Dune in this regard is a bit low-level (as to enjoy some better properties)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:32):

the build language is not very smart, just a list of rules

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:32):

then we have sugar in form of stanzas that for OCaml or Coq

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:32):

generate a set of rules

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:33):

stanzas indeed have access to the filesystem

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:33):

including the set of generated files

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:33):

thus to implement this feature, we need to tweak the part of dune that informs the "virtual" filesystem on what files are generated

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:35):

That's the code https://github.com/ocaml/dune/blob/8e155da034f1f1c10fed88bdba4887ac26be9bcf/src/dune_rules/dir_contents.ml#L145

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:36):

          | Coq_stanza.Extraction.T s ->
            Memo.Build.return (Coq_stanza.Extraction.ml_target_fnames s)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:36):

so as you can see, we inform dune's virtual filesystem (in dir_contents.ml) that an extraction stanza will generate the modules listed on the stanza

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:37):

see how this is already inside the build monad, so we can call coqc or whatever method we want

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:37):

to determine the list of modules to be generated

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:37):

does it make sense?

view this post on Zulip Yannick Zakowski (Feb 09 2022 at 14:20):

Thanks for the detailed answer Emilio! I lack a global understanding as to how dune works in general, but from what I gather what you are saying makes a lot of sense, yes. I signed-up for the hackaton, notably to follow your dune session, I would be happy to give a shot at this, absolutely :)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 14:22):

Cool! Actually I find the source code of Dune pretty easy to understand and hack, once you learn to navigate it, but indeed, as with many projects, documentation is an issue

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 14:22):

But the patch we need for this will be in the end a few lines of code

view this post on Zulip Yannick Zakowski (Feb 09 2022 at 14:25):

Perfect, that sounds like a great way for me to get into the code base. Thanks again!

view this post on Zulip Rudi Grinberg (Feb 11 2022 at 22:25):

It should indeed be possible to lift this limitation going forward. Feel free to ask here for help on how to do it

view this post on Zulip Rudi Grinberg (May 16 2022 at 21:25):

I just remembered this issue glancing over the coq code, and there's a bit of a complication that we haven't yet accounted for. Consider the following:

(coq.extraction
 (prelude foo.v))
(rule
 (with-stdout-to bar.ml (echo "")))

it's clear that extraction cannot produce a bar.ml here, but how do we know that without running the extraction rule?

view this post on Zulip Ali Caglayan (May 16 2022 at 21:33):

So the extraction doesn't declare the targets of the file?

view this post on Zulip Rudi Grinberg (May 16 2022 at 21:34):

Yes, that's what we want to avoid doing

view this post on Zulip Ali Caglayan (May 16 2022 at 21:34):

I guess you will have to be explicit with the extraction stanza, i.e. declare the targets

view this post on Zulip Ali Caglayan (May 16 2022 at 21:35):

If you sandbox both these rules there are no issues, but together they cause issues

view this post on Zulip Rudi Grinberg (May 16 2022 at 21:36):

Ali Caglayan said:

If you sandbox both these rules there are no issues, but together they cause issues

You can sandbox the rules (at least one of them) to run them, but you will need to combine the results carefully

view this post on Zulip Rudi Grinberg (May 16 2022 at 21:37):

Ali Caglayan said:

I guess you will have to be explicit with the extraction stanza, i.e. declare the targets

Actually, not all hope is lost. What you can do is something like have the extraction stanza produce the output into some subdirectory and then copy the sources from the sub directory back to where the extraction stanza was.

view this post on Zulip Rudi Grinberg (May 16 2022 at 21:38):

A bit of a headache, but should be doable. I would only go down that route if this is really an important feature

view this post on Zulip Ali Caglayan (May 16 2022 at 21:38):

@Karl Palmskog Which plugin was it that you mentioned was built from extracted code?

view this post on Zulip Karl Palmskog (May 16 2022 at 21:43):

https://github.com/coq-community/stalmarck/tree/master/tactic (only works on Coq 8.14 though)


Last updated: Feb 04 2023 at 02:03 UTC