Skip to content
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
executable file 76 lines (68 sloc) 4.28 KB
#!/usr/bin/env python
import argparse, shutil, os, os.path, sys
from custom_arguments import add_libname_arguments, update_env_with_libnames, add_logging_arguments, process_logging_arguments
from replace_imports import include_imports
# {Windows,Python,coqtop} is terrible; we fail to write to (or read
# from?) coqtop. But we can wrap it in a batch scrip, and it works
# fine.
SCRIPT_DIRECTORY = os.path.dirname(os.path.realpath(__file__))
DEFAULT_COQTOP = 'coqtop' if != 'nt' else os.path.join(SCRIPT_DIRECTORY, 'coqtop.bat')
parser = argparse.ArgumentParser(description='Inline the imports of a file')
parser.add_argument('input_file', metavar='IN_FILE', type=argparse.FileType('r'),
help='a .v file to inline the imports of')
parser.add_argument('output_file', metavar='OUT_FILE', type=argparse.FileType('w'),
help='a .v file to write to')
parser.add_argument('--fast-merge-imports', dest='fast_merge_imports',
action='store_const', const=True, default=False,
help='Use a faster method for combining imports')
parser.add_argument('--no-deps', dest='walk_tree',
action='store_const', const=False, default=True,
help=("Don't do dependency analysis on all files in the current " +
"file tree."))
parser.add_argument('--no-wrap-modules', dest='wrap_modules',
action='store_const', const=False, default=True,
help=("Don't wrap imports in Modules. By default, the " +
"contents of each file is wrapped in its own " +
"module to deal with renaming issues. This " +
"can cause issues with subdirectories."))
parser.add_argument('--absolutize-constants', dest='absolutize',
action='store_const', default=IMPORT_ABSOLUTIZE_TUPLE, const=ALL_ABSOLUTIZE_TUPLE,
help=("Replace constants with fully qualified versions. " +
"By default, all constants are not fully qualified. If you have " +
"many overlapping file names in different directories " +
"and use partially qualified names that differ depending " +
"on which files have been Required, not absolutizing constants " +
"may cause name resolution to fail."))
parser.add_argument('--coqbin', metavar='COQBIN', dest='coqbin', type=str, default='',
help='The path to a folder containing the coqc and coqtop programs.')
parser.add_argument('--coqc', metavar='COQC', dest='coqc', type=str, default='coqc',
help='The path to the coqc program.')
parser.add_argument('--coqtop', metavar='COQTOP', dest='coqtop', type=str, default=DEFAULT_COQTOP,
help=('The path to the coqtop program (default: %s).' % DEFAULT_COQTOP))
parser.add_argument('--coqc-args', metavar='ARG', dest='coqc_args', type=str, nargs='?',
help='Arguments to pass to coqc; e.g., " -indices-matter" (leading and trailing spaces are stripped)')
parser.add_argument('--coqtop-args', metavar='ARG', dest='coqtop_args', type=str, nargs='?',
help='Arguments to pass to coqtop; e.g., " -indices-matter" (leading and trailing spaces are stripped)')
parser.add_argument('--coq_makefile', metavar='COQ_MAKEFILE', dest='coq_makefile', type=str, default='coq_makefile',
help='The path to the coq_makefile program.')
if __name__ == '__main__':
args = process_logging_arguments(parser.parse_args())
env = {
'verbose': args.verbose,
'log': args.log,
'coqc': (args.coqc if args.coqbin == '' else os.path.join(args.coqbin, args.coqc)),
'absolutize': args.absolutize,
'as_modules': args.wrap_modules,
'fast': args.fast_merge_imports,
'coq_makefile': args.coq_makefile,
'walk_tree': args.walk_tree
update_env_with_libnames(env, args)
filename =
rtn = include_imports(filename, **env)
You can’t perform that action at this time.