Stream: Dune devs & users

Topic: Applying a patch onto an extracted file


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

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

view this post on Zulip Paolo Giarrusso (Jun 05 2022 at 13:37):

RefinedC uses this to wrap coqc with a timing command; that’s reasonable.

view this post on Zulip Paolo Giarrusso (Jun 05 2022 at 13:38):

My horrible question is “could you wrap ocamlc to patch sources if needed”?

view this post on Zulip Paolo Giarrusso (Jun 05 2022 at 13:38):

(Or maybe coqc?)

view this post on Zulip Paolo Giarrusso (Jun 05 2022 at 13:39):

I hope somebody has better ideas…

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

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

view this post on Zulip Li-yao (Jun 05 2022 at 14:11):

Yes extraction is a rather unreliable process, so some amount of postprocessing is to be expected.

view this post on Zulip Yannick Zakowski (Jun 05 2022 at 14:13):

In our case, it is due to this issue: https://github.com/coq/coq/issues/6614

view this post on Zulip Rudi Grinberg (Jun 05 2022 at 14:22):

What if we add a (patches ..) field to coq.extraction to take care of it?

view this post on Zulip Yannick Zakowski (Jun 05 2022 at 14:24):

Well from my perspective that would be the dream for sure!

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

view this post on Zulip Yannick Zakowski (Jun 05 2022 at 14:46):

I opened the following: https://github.com/ocaml/dune/issues/5832


Last updated: Jun 03 2023 at 17:29 UTC