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

Support selectively avoiding inlining modules #161

Open
JasonGross opened this issue Aug 17, 2023 · 1 comment
Open

Support selectively avoiding inlining modules #161

JasonGross opened this issue Aug 17, 2023 · 1 comment

Comments

@JasonGross
Copy link
Owner

To work around rocq-prover/rocq#17968, it would be nice to support things like --no-inline-module-regexp '^Ltac2\..*' or --no-inline-modules-under Ltac2, maybe also --no-inline-module Ltac2.Ltac for exact matching as well.

@JasonGross
Copy link
Owner Author

JasonGross commented Aug 17, 2023

This should be a pretty local change. Probably the thing to do is add a new file for handling this suite of arguments a la custom_arguments.py, add a function that adds the relevant arguments to the arg parser, also adding a function to the parsed object (or having a function that takes in the parsed object?) that checks if an absolute file/module path is blacklisted. Then just invoke that function changing

if req_module in libname_blacklist:

to

 if req_module in libname_blacklist or is_blacklisted(args, req_module):

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant