def include_imports(filename, as_modules=True, fast=False, log=DEFAULT_LOG, coqc='coqc', absolutize=ALL_ABSOLUTIZE_TUPLE, coq_makefile='coq_makefile', **kwargs):
    """Return the contents of filename, with any top-level imports inlined.

If as_modules == True, then the imports will be wrapped in modules.

This method requires access to the coqdep program if fast == False.
Without it, it will fall back to manual parsing of the imports,
which may change behavior.

>>> import tempfile, os
>>> f = tempfile.NamedTemporaryFile(dir='.', suffix='.v', delete=False)
>>> g = tempfile.NamedTemporaryFile(dir='.', suffix='.v', delete=False)
>>> g_name = os.path.relpath(g.name, '.')[:-2]
>>> f.write("  Require  Import %s Coq.Init.Logic Arith.\\n  Require  Export \tPArith\t Coq.Init.Logic.\\n  Require Bool.\\n Import Bool. (* asdf *)\\n Require Import QArith\\n  ZArith\\n  Setoid.\\nRequire Import %s.\\n Require\\n  Import\\n%s\\n\\n\t.\t(*foo*)\\n\\nInductive t := a | b.\\n\\n(*asdf*)" % (g_name, g_name, g_name))
>>> g.write(r"Require Export Ascii String.\\n\\nInductive q := c | d.")
>>> f.close()
>>> g.close()
>>> print(include_imports(f.name, as_modules=False))
Require Import Coq.Arith.Arith Coq.Bool.Bool Coq.Init.Logic Coq.PArith.PArith Coq.QArith.QArith Coq.Setoids.Setoid Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String.

Inductive q := c | d.
(* asdf *)


Inductive t := a | b.

(*asdf*)

>>> print(include_imports(f.name, as_modules=False, fast=True))
Require Import Arith Bool Coq.Init.Logic PArith QArith Setoid ZArith Ascii String.

Inductive q := c | d.
(* asdf *)


Inductive t := a | b.

(*asdf*)
>>> exts = ('.v', '.v.d', '.glob', '.vo', '.o', '.cmi', '.cmxs', '.native', '.cmx', '.vok', '.vos')
>>> names = [f.name[:-2] + ext for ext in exts] + [g.name[:-2] + ext for ext in exts]
>>> names = [i for i in names if os.path.exists(i)]
>>> for name in names: os.remove(name)
"""
    if 'make_coqc' in kwargs.keys():
        coqc = kwargs['make_coqc']
    if filename[-2:] != '.v': filename += '.v'
    lib = lib_of_filename(filename, **kwargs)
    all_imports = recursively_get_imports(lib, fast=fast, log=log, coqc=coqc, coq_makefile=coq_makefile, **kwargs)
    remaining_imports = []
    rtn = ''
    imports_done = []
    for import_name in all_imports:
        try:
            if as_modules:
                rtn += contents_as_module(import_name, imports_done, log=log, absolutize=absolutize, without_require=True, **kwargs) + '\n'
            else:
                rtn += contents_without_imports(import_name, log=log, absolutize=tuple(), **kwargs) + '\n'
            imports_done.append(import_name)
        except IOError:
            remaining_imports.append(import_name)
    if len(remaining_imports) > 0:
        log('remaining imports:', level=2)
        log(remaining_imports, level=2)
        if as_modules:
            pattern = 'Require %s.\n%s'
        else:
            pattern = 'Require Import %s.\n%s'
        for imp in reversed(remaining_imports):
            rtn = pattern % (imp, rtn)
    return rtn def normalize_requires(filename, **kwargs):
    """Return the contents of filename, with all [Require]s split out and ordered at the top.

Preserve any leading whitespace/comments.
"""
    if filename[-2:] != '.v': filename += '.v'
    kwargs = fill_kwargs(kwargs)
    lib = lib_of_filename(filename, **kwargs)
    all_imports = run_recursively_get_imports(lib, **kwargs)

    v_name = filename_of_lib(lib, ext='.v', **kwargs)
    contents = get_file(v_name, **kwargs)
    header, contents = split_leading_comments_and_whitespace(contents)
    contents = strip_requires(contents)
    contents = ''.join('Require %s.\n' % i for i in all_imports[:-1]) + '\n' + contents.strip() + '\n'
    return header + contents def get_required_contents(libname, **kwargs):
    return contents_as_module(libname, other_imports=[], export=True, **fill_kwargs(kwargs)) def recursively_get_requires_from_file(filename, **kwargs):
    if filename[-2:] != '.v': filename += '.v'
    kwargs = fill_kwargs(kwargs)
    lib = lib_of_filename(filename, **kwargs)
    return tuple(run_recursively_get_imports(lib, **kwargs)[:-1]) def absolutize_and_mangle_libname(lib, first_wrap_then_include=False):
    module_name, mangled_module_name, lib_parts, full_module_name = get_module_name_and_lib_parts(lib, first_wrap_then_include=first_wrap_then_include)
    return full_module_name def get_file(*args, **kwargs):
    return util.normalize_newlines(get_file_as_bytes(*args, **kwargs).decode('utf-8')) def get_recursive_require_names(libname, **kwargs):
    return tuple(i for i in get_recursive_requires(libname, **kwargs).keys() if i != libname) def run_recursively_get_imports(lib, recur=recursively_get_imports, fast=False, **kwargs):
    kwargs = fill_kwargs(kwargs)
    lib = norm_libname(lib, **kwargs)
    glob_name = filename_of_lib(lib, ext='.glob', **kwargs)
    v_name = filename_of_lib(lib, ext='.v', **kwargs)
    if os.path.isfile(v_name):
        imports = get_imports(lib, fast=fast, **kwargs)
        if kwargs['inline_coqlib'] and 'Coq.Init.Prelude' not in imports:
            mykwargs = dict(kwargs)
            coqlib_libname = (os.path.join(kwargs['inline_coqlib'], 'theories'), 'Coq')
            if coqlib_libname not in mykwargs['libnames']:
                mykwargs['libnames'] = tuple(list(kwargs['libnames']) + [coqlib_libname])
            try:
                coqlib_imports = get_imports('Coq.Init.Prelude', fast=fast, **mykwargs)
                if imports and not any(i in imports for i in coqlib_imports):
                    imports = tuple(list(coqlib_imports) + list(imports))
            except IOError as e:
                kwargs['log']("WARNING: --inline-coqlib passed, but no Coq.Init.Prelude found on disk.\n  Searched in %s\n  (Error was: %s)\n\n" % (repr(mykwargs['libnames']), repr(e)), level=LOG_ALWAYS)
        if not fast: make_globs(imports, **kwargs)
        imports_list = [recur(k, fast=fast, **kwargs) for k in imports]
        return merge_imports(tuple(map(tuple, imports_list + [[lib]])), **kwargs)
    return [lib] def strip_comments(contents):
    """Strips the comments from coq code in contents.

    The strings in contents are only preserved if there are no
    comment-like tokens inside of strings.  Stripping should be
    successful and correct, regardless of whether or not there are
    comment-like tokens in strings.

    The behavior of this method is undefined if there are any
    notations which change the meaning of '(*', '*)', or '"'.

    Note that we take some extra care to leave *) untouched when it
    does not terminate a comment.
    """
    contents = contents.replace('(*', ' (* ').replace('*)', ' *) ')
    tokens = contents.split(' ')
    rtn = []
    is_string = False
    comment_level = 0
    for token in tokens:
        do_append = (comment_level == 0)
        if is_string:
            if token.count('"') % 2 == 1: # there are an odd number of '"' characters, indicating that we've ended the string
                is_string = False
        elif token.count('"') % 2 == 1: # there are an odd number of '"' characters, so we're starting a string
            is_string = True
        elif token == '(*':
            comment_level += 1
            do_append = False
        elif comment_level > 0 and token == '*)':
            comment_level -= 1
        if do_append:
            rtn.append(token)
    return ' '.join(rtn).replace(' (* ', '(*').replace(' *) ', '*)').strip('\n\t ') def strip_newlines(contents, max_consecutive_newlines):
    """Removes consecutive newlines in excess of max_consecutive_newlines.

    If max_consecutive_newlines < 0, the contents is returned
    unchanged.

    If max_consecutive_newlines == 0, all strings of consecutive
    newlines are replaced by a single space.

    If max_consecutive_newlines > 0, all strings of consecutive
    newlines in excess of max_consecutive_newlines are replaced by
    max_consecutive_newlines newlines.
    """
    if max_consecutive_newlines < 0:
        return contents
    elif max_consecutive_newlines == 0:
        return re.sub(r'\n+', ' ', contents)
    else:
        newlines = r'\n' * max_consecutive_newlines
        return re.sub(newlines + '+', newlines, contents) def split_coq_file_contents(contents):
    """Splits the contents of a coq file into multiple statements.

    This is done by finding one or three periods followed by
    whitespace.  This is a dumb algorithm, but it seems to be (nearly)
    the one that ProofGeneral and CoqIDE use.

    We additionally merge lines inside of quotations."""
    return list(merge_quotations(re.split('(?<=[^\.]\.\.\.)\s|(?<=[^\.]\.)\s', strip_comments(contents)))) def split_leading_comments_and_whitespace(text):
    comment_level = 0
    in_str = False
    skip = False
    for i, (ch, next_ch) in enumerate(zip(text, text[1:] + '\0')):
        if skip:
            skip = False
        elif in_str:
            if ch in '"': in_str = False
        elif ch == '(' and next_ch == '*':
            comment_level += 1
            skip = True
        elif ch == '*' and next_ch == ')':
            comment_level -= 1
            skip = True
        elif comment_level > 0:
            if ch in '"': in_str = True
        elif ch.isspace():
            pass
        else:
            return text[:i], text[i:]
    return text, '' def split_statements_to_definitions(statements, log=DEFAULT_LOG, coqtop='coqtop', coqtop_args=tuple(), **kwargs):
    """Splits a list of statements into chunks which make up
    independent definitions/hints/etc."""
    def fallback():
        log("Your version of coqtop doesn't support -time.  Falling back to more error-prone method.")
        return split_definitions_old.split_statements_to_definitions(statements, log=log, coqtop=coqtop, coqtop_args=coqtop_args)
    # check for -time
    if not get_coq_accepts_time(coqtop, log=log):
        return fallback()
    if not get_proof_term_works_with_time(coqtop, is_coqtop=True, log=log, **kwargs):
        statements = postprocess_split_proof_term(statements, log=log, **kwargs)
    p = Popen([coqtop, '-q', '-emacs', '-time'] + list(coqtop_args), stdout=PIPE, stderr=STDOUT, stdin=PIPE)
    chars_time_reg = re.compile(r'Chars ([0-9]+) - ([0-9]+) [^\s]+'.replace(' ', r'\s*'))
    prompt_reg = re.compile(r'^(.*)<prompt>([^<]*?) < ([0-9]+) ([^<]*?) ([0-9]+) < ([^<]*)$'.replace(' ', r'\s*'),
                            flags=re.DOTALL)
    defined_reg = re.compile(r'^(?:<infomsg>)?([^\s]+) is (?:defined|assumed|declared)(?:</infomsg>)?$', re.MULTILINE)
    # goals and definitions are on stdout, prompts are on stderr
    statements_string = '\n'.join(statements) + '\n\n'
    statements_bytes = statements_string.encode('utf-8')
    log('Sending statements to coqtop...')
    log(statements_string, level=3)
    (stdout, stderr) = p.communicate(input=statements_bytes)
    stdout = util.s(stdout)
    if 'know what to do with -time' in stdout.strip().split('\n')[0]:
        # we're using a version of coqtop that doesn't support -time
        return fallback()
    log('Done.  Splitting to definitions...')

    rtn = []
    cur_definition = {}
    last_definitions = '||'
    cur_definition_names = '||'
    last_char_end = 0

    #log('re.findall(' + repr(r'Chars ([0-9]+) - ([0-9]+) [^\s]+ (.*?)<prompt>([^<]*?) < ([0-9]+) ([^<]*?) ([0-9]+) < ([^<]*?)</prompt>'.replace(' ', r'\s*')) + ', ' + repr(stdout) + ', ' + 'flags=re.DOTALL)', level=3)
    for i, prompt in enumerate(stdout.split('</prompt>')):
        log('Processing:\n%s' % prompt, level=4)
        if prompt.strip() == '': continue
        times = chars_time_reg.findall(prompt)
        if len(times) == 0:
            if i == 0:
                log('Warning: ignoring %s' % repr(prompt), level=3)
            else:
                log('Warning: Could not find timing info in %s' % repr(prompt), level=1)
            continue
        elif len(times) > 1:
            log('Warning: found multiple timing info in %s: %s' % (repr(prompt), repr(times)), level=1)
        full_response_text = chars_time_reg.sub(' ', prompt)
        for char_start, char_end in times:
            char_start, char_end = int(char_start), int(char_end)
            # if we've travelled backwards in time, as in
            # COQBUG(https://github.com/coq/coq/issues/14475); we just
            # ignore this statement
            if char_end <= last_char_end: continue
            match = prompt_reg.match(full_response_text)
            if not match:
                log('Warning: Could not find statements in %d:%d: %s' % (char_start, char_end, full_response_text), level=LOG_ALWAYS)
                continue
            response_text, cur_name, line_num1, cur_definition_names, line_num2, unknown = match.groups()
            statement = strip_newlines(statements_bytes[last_char_end:char_end].decode('utf-8'))
            last_char_end = char_end

            terms_defined = defined_reg.findall(response_text.strip())

            definitions_removed, definitions_shared, definitions_added = get_definitions_diff(last_definitions, cur_definition_names)

            # first, to be on the safe side, we add the new
            # definitions key to the dict, if it wasn't already there.
            if cur_definition_names.strip('|') and cur_definition_names not in cur_definition:
                cur_definition[cur_definition_names] = {'statements':[], 'terms_defined':[]}


            log((statement, (char_start, char_end), definitions_removed, terms_defined, 'last_definitions:', last_definitions, 'cur_definition_names:', cur_definition_names, cur_definition.get(last_definitions, []), cur_definition.get(cur_definition_names, []), response_text), level=2)


            # first, we handle the case where we have just finished
            # defining something.  This should correspond to
            # len(definitions_removed) > 0 and len(terms_defined) > 0.
            # If only len(definitions_removed) > 0, then we have
            # aborted something (or we're in Coq >= 8.11; see
            # https://github.com/coq/coq/issues/15201).  If only
            # len(terms_defined) > 0, then we have defined something
            # with a one-liner.
            if definitions_removed:
                cur_definition[last_definitions]['statements'].append(statement)
                cur_definition[last_definitions]['terms_defined'] += terms_defined
                if cur_definition_names.strip('|'):
                    # we are still inside a definition.  For now, we
                    # flatten all definitions.
                    #
                    # TODO(jgross): Come up with a better story for
                    # nested definitions.
                    cur_definition[cur_definition_names]['statements'] += cur_definition[last_definitions]['statements']
                    cur_definition[cur_definition_names]['terms_defined'] += cur_definition[last_definitions]['terms_defined']
                    del cur_definition[last_definitions]
                else:
                    # we're at top-level, so add this as a new
                    # definition
                    rtn.append({'statements':tuple(cur_definition[last_definitions]['statements']),
                                'statement':'\n'.join(cur_definition[last_definitions]['statements']),
                                'terms_defined':tuple(cur_definition[last_definitions]['terms_defined'])})
                    del cur_definition[last_definitions]
                    # print('Adding:')
                    # print(rtn[-1])
            elif terms_defined:
                if cur_definition_names.strip('|'):
                    # we are still inside a definition.  For now, we
                    # flatten all definitions.
                    #
                    # TODO(jgross): Come up with a better story for
                    # nested definitions.
                    cur_definition[cur_definition_names]['statements'].append(statement)
                    cur_definition[cur_definition_names]['terms_defined'] += terms_defined
                else:
                    # we're at top level, so add this as a new
                    # definition
                    rtn.append({'statements':(statement,),
                                'statement':statement,
                                'terms_defined':tuple(terms_defined)})

            # now we handle the case where we have just opened a fresh
            # definition.  We've already added the key to the
            # dictionary.
            elif definitions_added:
                # print(definitions_added)
                cur_definition[cur_definition_names]['statements'].append(statement)
            else:
                # if we're in a definition, append the statement to
                # the queue, otherwise, just add it as it's own
                # statement
                if cur_definition_names.strip('|'):
                    cur_definition[cur_definition_names]['statements'].append(statement)
                else:
                    rtn.append({'statements':(statement,),
                                'statement':statement,
                                'terms_defined':tuple()})

            last_definitions = cur_definition_names

    log((last_definitions, cur_definition_names), level=2)
    if last_definitions.strip('||'):
        rtn.append({'statements':tuple(cur_definition[cur_definition_names]['statements']),
                    'statement':'\n'.join(cur_definition[cur_definition_names]['statements']),
                    'terms_defined':tuple(cur_definition[cur_definition_names]['terms_defined'])})
        del cur_definition[last_definitions]

    if last_char_end + 1 < len(statements_bytes):
        last_statement = statements_bytes[last_char_end:].decode('utf-8')
        log('Appending end of code from %d to %d: %s' % (last_char_end, len(statements_bytes), last_statement), level=2)
        last_statement = strip_newlines(last_statement)
        rtn.append({'statements':tuple(last_statement,),
                    'statement':last_statement,
                    'terms_defined':tuple()})

    return rtn def join_definitions(definitions):
    return '\n'.join(i['statement'] for i in definitions) def transform_abstract_to_admit(cur_definition, rest_definitions, **kwargs):
    # shallow copy
    cur_definition = dict(cur_definition)
    cur_definition['statements'] = tuple(transform_abstract_to_admit_statement(i, **kwargs)
                                         for i in cur_definition['statements'])
    cur_definition['statement'] = '\n'.join(cur_definition['statements'])
    return cur_definition def lib_of_filename(filename, exts=('.v', '.glob'), **kwargs):
    kwargs = fill_kwargs(kwargs)
    filename, libname = lib_of_filename_helper(filename, libnames=tuple(kwargs['libnames']), non_recursive_libnames=tuple(kwargs['non_recursive_libnames']), exts=exts)
#    if '.' in filename:
#        # TODO: Do we still need this warning?
#        kwargs['log']("WARNING: There is a dot (.) in filename %s; the library conversion probably won't work." % filename)
    return libname def clear_libimport_cache(libname):
    if libname in lib_imports_fast.keys():
        del lib_imports_fast[libname]
    if libname in lib_imports_slow.keys():
        del lib_imports_slow[libname] IMPORT_ABSOLUTIZE_TUPLE = ('lib', 'mod') ALL_ABSOLUTIZE_TUPLE = ('lib', 'proj', 'rec', 'ind', 'constr', 'def', 'syndef', 'class', 'thm', 'lem', 'prf', 'ax', 'inst', 'prfax', 'coind', 'scheme', 'vardef', 'mod')# , 'modtype') def split_requires_of_statements(annotated_contents, types=('lib',), appends=('<>',), **kwargs):
    already_required = set()
    prefix, postfix = '\nRequire ', '.'
    for statement, references in annotated_contents:
        statement_str = statement.decode('utf-8')
        if not references:
            yield (statement, references)
            continue
        rkind = classify_require_kind(statement, references)
        if rkind not in (REQUIRE, REQUIRE_IMPORT, REQUIRE_EXPORT) or len(references) == 1 and rkind == REQUIRE:
            yield (statement, references)
            continue
        remaining_references = []
        emitted_require = False
        for start, end, loc, append, ty in references:
            if ty in types and append in appends:
                if loc not in already_required:
                    already_required.add(loc)
                    emitted_require = True
                    yield ((prefix + loc + postfix).encode('utf-8'),
                           (len(prefix), len(prefix) - start + end, loc, append, ty))
            else:
                remaining_references.append((start - len('Require '), end - len('Require '), loc, append, ty))
        if rkind == REQUIRE: continue
        statement_str = re.sub(r'Require\s', '', statement_str, count=1)
        if emitted_require and not re.match(r'\s', statement_str[0]): yield ('\n'.encode('utf-8'), tuple()) # we need an extra newline
        yield (statement_str.encode('utf-8'), tuple(remaining_references)) def get_file_statements_insert_references(filename, **kwargs):
    ranges = get_coq_statement_byte_ranges(filename, **kwargs)
    contents = get_file_as_bytes(filename, **kwargs)
    refs = get_byte_references_for(filename, **kwargs)
    if refs is None: return None
    return insert_references(contents, ranges, refs, **kwargs) def memoize(f):
    """ Memoization decorator for a function taking one or more arguments. """
    class memodict(dict):
        def __getitem__(self, *key, **kwkey):
            return dict.__getitem__(self, (tuple(key), tuple((k, kwkey[k]) for k in sorted(kwkey.keys()))))

        def __missing__(self, key):
            args, kwargs = key
            self[key] = ret = f(*args, **dict(kwargs))
            return ret

    return memodict().__getitem__ def get_coqc_version(coqc_prog, **kwargs):
    kwargs['log']('Running command: "%s"' % '" "'.join([coqc_prog, "-q", "-v"]), level=2)
    return get_coqc_version_helper(coqc_prog) def get_coqtop_version(coqtop_prog, **kwargs):
    kwargs['log']('Running command: "%s"' % '" "'.join([coqtop_prog, "-q", "-v"]), level=2)
    return get_coqtop_version_helper(coqtop_prog) def get_coqc_help(coqc_prog, **kwargs):
    kwargs['log']('Running command: "%s"' % '" "'.join([coqc_prog, "-q", "--help"]), level=2)
    return get_coqc_help_helper(coqc_prog) @memoize
def get_coq_accepts_top(coqc):
    temp_file = tempfile.NamedTemporaryFile(suffix='.v', dir='.', delete=True)
    temp_file_name = temp_file.name
    p = subprocess.Popen([coqc, "-q", "-top", "Top", temp_file_name], stderr=subprocess.STDOUT, stdout=subprocess.PIPE)
    (stdout, stderr) = p.communicate()
    temp_file.close()
    clean_v_file(temp_file_name)
    return '-top: no such file or directory' not in util.s(stdout) def get_coq_native_compiler_ondemand_fragment(coqc_prog, **kwargs):
    help_lines = get_coqc_help(coqc_prog, **kwargs).split('\n')
    if any('ondemand' in line for line in help_lines if line.strip().startswith('-native-compiler')):
        if get_coq_accepts_w(coqc_prog, **kwargs):
            return ('-w', '-deprecated-native-compiler-option,-native-compiler-disabled', '-native-compiler', 'ondemand')
        elif not get_coqc_native_compiler_ondemand_errors(coqc_prog):
            return ('-native-compiler', 'ondemand')
    return tuple() def group_coq_args(args, coqc_help, topname=None, is_coq_makefile=False):
    bindings, unrecognized_bindings = group_coq_args_split_recognized(args, coqc_help, topname=topname, is_coq_makefile=is_coq_makefile)
    return bindings + [tuple([v]) for v in unrecognized_bindings] def get_coqc_coqlib(coqc_prog, **kwargs):
    return [line[len('COQLIB='):] for line in get_coqc_config(coqc_prog, **kwargs).split('\n') if line.startswith('COQLIB=')][0] @memoize
def get_coq_accepts_compile(coqtop):
    temp_file = tempfile.NamedTemporaryFile(suffix='.v', dir='.', delete=True)
    temp_file_name = temp_file.name
    p = subprocess.Popen([coqtop, "-q", "-compile", temp_file_name], stderr=subprocess.STDOUT, stdout=subprocess.PIPE)
    (stdout, stderr) = p.communicate()
    rc = p.returncode
    temp_file.close()
    clean_v_file(temp_file_name)
    return rc == 0 def get_ltac_support_snippet(coqc, **kwargs):
    if coqc in LTAC_SUPPORT_SNIPPET.keys():
        return LTAC_SUPPORT_SNIPPET[coqc]
    test = r'''Inductive False : Prop := .
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Goal False. admit. Qed.'''
    errinfo = {}
    native_ondemand_args = list(get_coq_native_compiler_ondemand_fragment(coqc, **kwargs))
    for before, after in (('Declare ML Module "coq-core.plugins.ltac".\n', ''),
                          ('Declare ML Module "coq-core.plugins.ltac".\n', 'Global Set Default Proof Mode "Classic".\n'),
                          ('Declare ML Module "ltac_plugin".\n', ''),
                          ('Declare ML Module "ltac_plugin".\n', 'Global Set Default Proof Mode "Classic".\n'),
                          ('Require Coq.Init.Ltac.\n', 'Import Coq.Init.Ltac.\n'),
                          ('Require Coq.Init.Notations.\n', 'Import Coq.Init.Notations.\n')):
        contents = '%s\n%s\n%s' % (before, after, test)
        output, cmds, retcode, runtime = get_coq_output(coqc, tuple(['-q', '-nois'] + native_ondemand_args), contents, timeout_val=None, verbose_base=3, is_coqtop=kwargs['coqc_is_coqtop'], **kwargs)
        if retcode == 0:
            LTAC_SUPPORT_SNIPPET[coqc] = (before, after)
            return (before, after)
        else:
            errinfo[contents] = {'output': output, 'cmds': cmds, 'retcode': retcode, 'runtime': runtime}
    raise Exception('No valid ltac support snipped found.  Debugging info: %s' % repr(errinfo)) def add_libname_arguments(parser): add_libname_arguments_gen(parser, passing='') def add_passing_libname_arguments(parser):
    add_libname_arguments_gen(parser, 'passing')
    add_libname_arguments_gen(parser, 'nonpassing') def update_env_with_libnames(env, args, default=(('.', 'Top'), ), include_passing=False, use_default=True, use_passing_default=True):
    all_keys = ('libnames', 'non_recursive_libnames', 'ocaml_dirnames', '_CoqProject', '_CoqProject_v_files', '_CoqProject_unknown')
    passing_opts = ('', ) if not include_passing else ('', 'passing_', 'nonpassing_')
    for passing in passing_opts:
        for key in all_keys:
            env[passing + key] = []
        if getattr(args, passing + 'CoqProjectFile'):
            for f in getattr(args, passing + 'CoqProjectFile'):
                env[passing + '_CoqProject'] = f.read()
                f.close()
        process_CoqProject(env, env[passing + '_CoqProject'], passing=passing)
        env[passing + 'libnames'].extend(getattr(args, passing + 'libnames'))
        env[passing + 'non_recursive_libnames'].extend(getattr(args, passing + 'non_recursive_libnames'))
        env[passing + 'ocaml_dirnames'].extend(getattr(args, passing + 'ocaml_dirnames'))
    if include_passing:
        # The nonpassing_ prefix is actually temporary; the semantics
        # are that, e.g., libnames = libnames + nonpassing_libnames,
        # while passing_libnames = libnames + passing_libnames
        for key in all_keys:
            env['passing_' + key] = env[key] + env['passing_' + key]
            env[key] = env[key] + env['nonpassing_' + key]
            del env['nonpassing_' + key]
    if use_default:
        update_env_with_libname_default(env, args, default=default)
    if use_passing_default and include_passing:
        update_env_with_libname_default(env, args, default=default, passing='passing_') def update_env_with_coqpath_folders(passing_prefix, env, *coqpaths):
    def do_with_path(path):
        env.get(passing_prefix + 'non_recursive_libnames', []).extend((os.path.join(path, d), d) for d in sorted(os.listdir(path)))
    for coqpath in coqpaths:
        if os.path.isdir(coqpath):
            do_with_path(coqpath)
        elif ';' in coqpath:
            for path in coqpath.split(';'):
                do_with_path(coqpath if coqpath != '' else '.')
        elif ':' in coqpath:
            for path in coqpath.split(':'):
                do_with_path(coqpath if coqpath != '' else '.') def add_logging_arguments(parser):
    parser.add_argument('--verbose', '-v', dest='verbose',
                        action='count',
                        help='display some extra information by default (does not impact --verbose-log-file)')
    parser.add_argument('--quiet', '-q', dest='quiet',
                        action='count',
                        help='the inverse of --verbose')
    parser.add_argument('--log-file', '-l', dest='log_files', nargs='+', type=argparse.FileType('w'),
                        default=[sys.stderr],
                        help='The files to log output to.  Use - for stdout.')
    parser.add_argument('--verbose-log-file', dest='verbose_log_files', nargs='+', type=TupleType(int, argparse.FileType('w')),
                        default=[],
                        help=(('The files to log output to at verbosity other than the default verbosity (%d if no -v/-q arguments are passed); ' +
                               'each argument should be a pair of a verbosity level and a file name. '
                               'Use - for stdout.') % DEFAULT_VERBOSITY)) def process_logging_arguments(args):
    if args.verbose is None: args.verbose = DEFAULT_VERBOSITY
    if args.quiet is None: args.quiet = 0
    args.verbose -= args.quiet
    args.log = make_logger([(args.verbose, f) for f in args.log_files]
                           + args.verbose_log_files)
    del args.quiet
    del args.verbose
    return args DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)]) LOG_ALWAYS=None def has_dir_binding(args, coqc_help, file_name=None):
    kwargs = dict()
    if file_name is not None: kwargs['topname'] = topname_of_filename(file_name)
    bindings = group_coq_args(args, coqc_help, **kwargs)
    return any(i[0] in ('-R', '-Q') for i in bindings) def deduplicate_trailing_dir_bindings(args, coqc_help, coq_accepts_top, file_name=None):
    kwargs = dict()
    if file_name is not None: kwargs['topname'] = topname_of_filename(file_name)
    bindings = group_coq_args(args, coqc_help, **kwargs)
    ret = []
    for binding in bindings:
        if coq_accepts_top or binding[0] != '-top':
            ret.extend(binding)
    return tuple(ret) def process_maybe_list(ls, log=DEFAULT_LOG):
    if ls is None: return tuple()
    if isinstance(ls, str): return tuple([ls])
    if isinstance(ls, tuple): return ls
    if isinstance(ls, list): return tuple(ls)
    log("Unknown type '%s' of list '%s'" % (str(type(ls)), repr(ls)))
    return tuple(ls) def clean_v_file(file_name):
    clean_extra_coq_files(file_name, extra_exts=('.v',)) def read_from_file(file_name):
    return util.normalize_newlines(read_bytes_from_file(file_name).decode('utf-8')) def write_to_file(file_name, contents, *args, **kwargs):
    return write_bytes_to_file(file_name, contents.replace('\n', os.linesep).encode('utf-8'), *args, **kwargs) def restore_file(file_name, backup_ext='.bak', backup_backup_ext='.unbak'):
    if not os.path.exists(file_name + backup_ext):
        raise IOError
    if os.path.exists(file_name):
        if backup_backup_ext:
            backup(file_name, backup_backup_ext)
        else:
            os.remove(file_name)
    os.rename(file_name + backup_ext, file_name) def yes_no_prompt(**kwargs):
    return prompt(({'value':True, 'display':'(y)es', 'values':('y', 'yes')},
                   {'value':False, 'display':'(n)o', 'values':('n', 'no')}),
                  yes_value=True,
                  **kwargs) PY3 = False
import tempfile, sys, os, re
import traceback
import custom_arguments
import util
import diagnose_error
from argparse_compat import argparse
from replace_imports import include_imports, normalize_requires, get_required_contents, recursively_get_requires_from_file, absolutize_and_mangle_libname
from import_util import get_file, get_recursive_require_names, run_recursively_get_imports
from strip_comments import strip_comments
from strip_newlines import strip_newlines
from split_file import split_coq_file_contents, split_leading_comments_and_whitespace
from split_definitions import split_statements_to_definitions, join_definitions
from admit_abstract import transform_abstract_to_admit
from import_util import lib_of_filename, clear_libimport_cache, IMPORT_ABSOLUTIZE_TUPLE, ALL_ABSOLUTIZE_TUPLE
from import_util import split_requires_of_statements, get_file_statements_insert_references
from memoize import memoize
from coq_version import get_coqc_version, get_coqtop_version, get_coqc_help, get_coq_accepts_top, get_coq_native_compiler_ondemand_fragment, group_coq_args, get_coqc_coqlib, get_coq_accepts_compile
from coq_running_support import get_ltac_support_snippet
from custom_arguments import add_libname_arguments, add_passing_libname_arguments, update_env_with_libnames, update_env_with_coqpath_folders, add_logging_arguments, process_logging_arguments, DEFAULT_LOG, LOG_ALWAYS
from binding_util import has_dir_binding, deduplicate_trailing_dir_bindings, process_maybe_list
from file_util import clean_v_file, read_from_file, write_to_file, restore_file
from util import yes_no_prompt, PY3


def try_normalize_requires(output_file_name, **kwargs):
    contents = read_from_file(output_file_name)
    old_contents = contents
    # we need to clear the libimport cache to get an accurate list of requires
    clear_libimport_cache(lib_of_filename(output_file_name, **kwargs))
    new_contents = normalize_requires(output_file_name, update_globs=True, **env)

    check_change_and_write_to_file(old_contents, new_contents, output_file_name,
                                   unchanged_message='No Requires to normalize.',
                                   success_message='Succeeded in normalizing Requires.',
                                   failure_description='normalize Requires',
                                   changed_descruption='Normalized Requires file',
                                   **kwargs)


def try_split_requires(output_file_name, **kwargs):
    contents = read_from_file(output_file_name)
    old_contents = contents
    annotated_contents = get_file_statements_insert_references(output_file_name, update_globs=True, types=('lib',), appends=('<>',), **kwargs)
    if annotated_contents is None:
        env['log']('\nNon-fatal error: Failed to get references for %s' % output_file_name, level=LOG_ALWAYS)
        return False

    annotated_contents = split_requires_of_statements(annotated_contents, **env)
    new_contents = ''.join(v[0].decode('utf-8') for v in annotated_contents)

    return check_change_and_write_to_file(old_contents, new_contents, output_file_name,
                                          unchanged_message='No Requires to split.',
                                          success_message='Succeeded in splitting Requires.',
                                          failure_description='split Requires',
                                          changed_descruption='Split Requires file',
                                          **kwargs)



def try_strip_newlines(output_file_name, max_consecutive_newlines, strip_trailing_space, **kwargs):
    contents = read_from_file(output_file_name)
    old_contents = contents
    if strip_trailing_space:
        contents = '\n'.join(line.rstrip() for line in contents.split('\n'))
    new_contents = strip_newlines(contents, max_consecutive_newlines)

    check_change_and_write_to_file(old_contents, new_contents, output_file_name,
                                   unchanged_message='No strippable newlines or spaces.',
                                   success_message='Succeeded in stripping newlines and spaces.',
                                   failure_description='strip newlines and spaces',
                                   changed_descruption='Stripped file',
                                   **kwargs)


def try_strip_extra_lines(output_file_name, line_num, **kwargs):
    contents = read_from_file(output_file_name)
    statements = split_coq_file_contents(contents)
    cur_line_num = 0
    new_statements = statements
    for statement_num, statement in enumerate(statements):
        cur_line_num += statement.count('\n') + 1 # +1 for the extra newline between each statement
        if cur_line_num >= line_num:
            new_statements = statements[:statement_num + 1]
            break

    if check_change_and_write_to_file('\n'.join(statements), '\n'.join(new_statements), output_file_name,
                                      unchanged_message='No lines to trim.',
                                      success_message=('Trimming successful.  We removed all lines after %d; the error was on line %d.' % (cur_line_num, line_num)),
                                      failure_description='trim file',
                                      changed_descruption='Trimmed file',
                                      **kwargs):
        kwargs['log']('Trimmed file:\n%s' % read_from_file(output_file_name), level=3)



EMPTY_SECTION_REG = re.compile(r'(\.\s+|^\s*)(?:Section|Module\s+Export|Module)\s+([^ \.]+)\.' +
                               r'(?:\s' +
                               r'|Local\s'
                               r'|Set\s+Universe\s+Polymorphism\s*\.\s' +
                               r'|Unset\s+Universe\s+Polymorphism\s*\.\s)+End\s+([^ \.]+)\.(\s+|$)', flags=re.MULTILINE)
def try_strip_empty_sections(output_file_name, **kwargs):
    contents = read_from_file(output_file_name)
    old_contents = contents
    new_contents = EMPTY_SECTION_REG.sub(r'\1', old_contents)
    while new_contents != old_contents:
        old_contents, new_contents = new_contents, EMPTY_SECTION_REG.sub(r'\1', new_contents)

    check_change_and_write_to_file(contents, new_contents, output_file_name,
                                   unchanged_message='No empty sections to remove.',
                                   success_message='Empty section removal successful.',
                                   failure_description='remove empty sections',
                                   changed_descruption='Trimmed file',
                                   **kwargs)


def add_admit_tactic(contents, **kwargs):
    before, after = get_ltac_support_snippet(**kwargs)
    tac_code = r"""%sModule Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
%sTactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
""" % (before, after)
    tac_code_re = r"""\s*Module Export AdmitTactic\.
?(?:Module Import LocalFalse\.
?(?:Inductive False : Prop := \.)?
?End LocalFalse\.)?
?(?:Axiom proof_admitted : False\.)?
?(?:%s)?(?:Tactic Notation "admit" := abstract case proof_admitted\.)?
?End AdmitTactic\.\n*""" % re.escape(after)
    header, contents = split_leading_comments_and_whitespace(contents)
    return '%s%s%s' % (header, tac_code, re.sub(tac_code_re, '\n', contents.replace(before, ''), flags=re.DOTALL|re.MULTILINE))


def default_on_fatal(message, log=DEFAULT_LOG, **env):
    if message is not None: log(message, level=0, force_stderr=True)
    sys.exit(1)

def minimize_file(output_file_name, die=default_on_fatal, **env):
    """The workhorse of bug minimization.  The only thing it doesn't handle is inlining [Require]s and other preprocesing"""

    contents = read_from_file(output_file_name)