coq-min-imports

This script will try to remove unnecessary module imports from Coq sources. It examines modules listed in "Require Import" statements one by one and tries to recompile to see if their removal would cause compilation errors.

Running

The easy way to run it is to replace COQC variable in Makefile generated by coq_makefile with:

COQC=coq-min-imports -cmi-verbose -cmi-wrap

And run the make. For each .v file where some imports where removed, a modified version will be saved with .v.new extension. If want to overwrite .v files rather than generate new versions, use -cmi-replace option.

Sometimes removing an import will not cause the compilation to fail immediately but rather makes coqc to run for a very long time. One workaround is to add a timeout to coqc invocation. This could be done using timeout(1) shell wrapper. For example, using the following command line option with coq-min-imports: -cmi-coqc="timeout 10s coqc" will impose 10 seconds compilation timout.

Example:

$ coq-min-imports -cmi-verbose -cmi-wrap  -q  -R "." Top -I "."   CarrierType.v
Processing CarrierType.v
    -MathClasses.orders.orders
    +MathClasses.interfaces.orders
    +MathClasses.theory.rings
    +MathClasses.interfaces.abstract_algebra
    +CoLoR.Util.Vector.VecUtil
    -Ring
    -Coq.Bool.Bool
Writing modified copy of CarrierType.v as CarrierType.v.new with 3 imports removed

In the verbose mode, used above, it prints each imported module it attempts to remove. Modules marked with + could not be removed, and modules marked with - will be removed.

Usage:

coq-min-imports <coq_flags> [-cmi-verbose] [-cmi-replace] [-cmi-wrap] <files...>

where

• <coq_flags> - any of optoins supported by 'coqc'
• <files> - list of .v files to process
• -cmi-verbose - enable verbose reporting
• -cmi-replace - replace processed files with optmized versions (orignals are saved with the ".bak" suffix). Otherwise, the optimized versions are written as a new files with the same name as the input but adding ".new" suffix
• -cmi-wrap - run in a coqc-wrapper mode, compiling the files as the side-effect
• -cmi-coqc=<command> - use the <command> instead of coqc

Author

Vadim Zaliva [email protected]