Yannick Zakowski (Feb 06 2022 at 20:35): 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?
Notification Bot (Feb 06 2022 at 20:52):This topic was moved here from #Coq users > Extraction with dune by Karl Palmskog
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?
Karl Palmskog (Feb 07 2022 at 08:23):not to my knowledge.
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
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
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:29):It is not hard to do at all
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:30):The reason it works like this now
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
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
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:30):as to preserve the soundness of the incremental build
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
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)
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)
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:32):the build language is not very smart, just a list of rules
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:32):then we have sugar in form of stanzas that for OCaml or Coq
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:32):generate a set of rules
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:33):stanzas indeed have access to the filesystem
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:33):including the set of generated files
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
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
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)
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
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
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:37):to determine the list of modules to be generated
Emilio Jesús Gallego Arias (Feb 07 2022 at 21:37):does it make sense?
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 :)
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
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
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!
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
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?
Ali Caglayan (May 16 2022 at 21:33):So the extraction doesn't declare the targets of the file?
Rudi Grinberg (May 16 2022 at 21:34):Yes, that's what we want to avoid doing
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
Ali Caglayan (May 16 2022 at 21:35):If you sandbox both these rules there are no issues, but together they cause issues
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
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.
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
Ali Caglayan (May 16 2022 at 21:38):@Karl Palmskog Which plugin was it that you mentioned was built from extracted code?
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: Jun 03 2023 at 18:01 UTC