coq-tools icon indicating copy to clipboard operation
coq-tools copied to clipboard

Support selectively avoiding inlining modules

Open JasonGross opened this issue 2 years ago • 1 comments

To work around https://github.com/coq/coq/issues/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 avatar Aug 17 '23 19:08 JasonGross

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 https://github.com/JasonGross/coq-tools/blob/7562bafc9b21cb34d74f869632455e67d11f5bc3/find-bug.py#L1502 to

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

JasonGross avatar Aug 17 '23 19:08 JasonGross