Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[coq] Adding a "patch" field to coq.extraction #5832

Open
YaZko opened this issue Jun 5, 2022 · 2 comments
Open

[coq] Adding a "patch" field to coq.extraction #5832

YaZko opened this issue Jun 5, 2022 · 2 comments
Labels

Comments

@YaZko
Copy link

YaZko commented Jun 5, 2022

It seems to be fairly common for Coq projects relying on extraction to need to patch some of the extracted files before proceeding to the OCaml side of the compilation.

One example of such a process is encountered in the Vellvm project where the issue described in (coq/coq#6614) is encountered. As a fix, the following patch is applied by the Makefile right after extraction, before building the OCaml side of the project.
This problem is an obstacle to moving the project completely to a dune-based build, as attempted in this branch: we do not know how to tell dune to apply the patch at the right moment.

@rgrinberg has suggested that a dedicated field in the coq.extraction stanza could be the way to go: it indeed would be ideal as a user.

@ejgallego
Copy link
Collaborator

Yes, this is a problem we all have, but it'd be great if we could fix the Coq bug. It is so unfortunate we need to do this patch field.

But I guess that's easy.

Myself, I've been workaround this with a user-defined rule and copy_files....

@rgrinberg
Copy link
Member

The issue is analogous to preprocessing imo, so there's no reason to support one and not the other. For example, you can already do something like:

(library
 (preprocessor_deps p1.patch p2.patch...)
 (preprocess (action ./foo.sh)) ;; foo.sh decided which patches to apply (if at all)
 ..)

The solution I have in mind is just to make the above a little easier.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
Status: Todo
Development

No branches or pull requests

4 participants