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?
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
RefinedC uses this to wrap coqc with a timing command; that’s reasonable.
My horrible question is “could you wrap ocamlc to patch sources if needed”?
(Or maybe coqc?)
I hope somebody has better ideas…
I see... I do hope that another option exists indeed, but that's an interesting thought, thanks!
is applying patches to extracted files a common practice? perhaps we should have first class support for it in dune then
Yes extraction is a rather unreliable process, so some amount of postprocessing is to be expected.
In our case, it is due to this issue: https://github.com/coq/coq/issues/6614
What if we add a
(patches ..) field to
coq.extraction to take care of it?
Well from my perspective that would be the dream for sure!
Okay, could you please make a dune issue with examples of the patch files you use? Should be easy to fix.
I opened the following: https://github.com/ocaml/dune/issues/5832
Last updated: Jan 30 2023 at 18:04 UTC