Yannick Zakowski (Jun 05 2022 at 13:03): Yannick Zakowski (Jun 05 2022 at 13:03):Hello,
We have tried some time ago to get the Vellvm project to compile entirely with Dune --- in this branch https://github.com/vellvm/vellvm/tree/opam-release . The project has a Coq theory, performs some relatively heavy extraction, and links the extracted file with some OCaml.
It is quite close to work (although we have to accept to statically list over a 100 modules for extraction --- https://github.com/vellvm/vellvm/blob/opam-release/src/ml/extracted/dune ), but we still have one wrinkle: due to a bug in the extraction mechanism, an extracted .mli file mismatches its .ml, so we have to manually patch it.
We used to simply apply this patch in our Makefile (https://github.com/vellvm/vellvm/blob/opam-release/src/CRelationClasses.mli.patch), but now that dune chains the three compilation steps itself, it freaks out and I have no idea how to insert the patch in this chain.
Would anyone know if it's possible, and if so how to do it?
Paolo Giarrusso (Jun 05 2022 at 13:36):Here’s an horrible trick: you can wrap binaries to modify their behavior: https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/dune#L2 https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/tools/coqc_timing.sh#L8
Paolo Giarrusso (Jun 05 2022 at 13:37):RefinedC uses this to wrap coqc with a timing command; that’s reasonable.
Paolo Giarrusso (Jun 05 2022 at 13:38):My horrible question is “could you wrap ocamlc to patch sources if needed”?
Paolo Giarrusso (Jun 05 2022 at 13:38):(Or maybe coqc?)
Paolo Giarrusso (Jun 05 2022 at 13:39):I hope somebody has better ideas…
Yannick Zakowski (Jun 05 2022 at 13:56):I see... I do hope that another option exists indeed, but that's an interesting thought, thanks!
Rudi Grinberg (Jun 05 2022 at 13:57):is applying patches to extracted files a common practice? perhaps we should have first class support for it in dune then
Li-yao (Jun 05 2022 at 14:11):Yes extraction is a rather unreliable process, so some amount of postprocessing is to be expected.
Yannick Zakowski (Jun 05 2022 at 14:13):In our case, it is due to this issue: https://github.com/coq/coq/issues/6614
Rudi Grinberg (Jun 05 2022 at 14:22):What if we add a (patches ..) field to coq.extraction to take care of it?
Yannick Zakowski (Jun 05 2022 at 14:24):Well from my perspective that would be the dream for sure!
Rudi Grinberg (Jun 05 2022 at 14:29):Okay, could you please make a dune issue with examples of the patch files you use? Should be easy to fix.
Yannick Zakowski (Jun 05 2022 at 14:46):I opened the following: https://github.com/ocaml/dune/issues/5832
Last updated: Jan 30 2023 at 18:04 UTC