# Path: split_file.py
# def postprocess_split_proof_term(statements, do_warn=True, **kwargs):
#     def do_warn_method(statement_num, statement, proof_term):
#         kwargs['log']("""Warning: Your version of Coq suffers from bug #5349 (https://coq.inria.fr/bugs/show_bug.cgi?id=5349)
# and does not support [Proof (term).] with -time.  Falling back to
# replacing [Proof (term).] with [Proof. exact (term). Qed.], which may fail.""")
#     if do_warn and 'log' in kwargs.keys():
#         do_warn = do_warn_method
#     else:
#         do_warn = None
#     return list(postprocess_split_proof_term_iter(statements, do_warn))
# 
# Path: coq_version.py
# def get_coq_accepts_time(coqc_prog, **kwargs):
#     return get_coq_accepts_option(coqc_prog, '-time', **kwargs)
# 
# Path: coq_running_support.py
# def get_proof_term_works_with_time(coqc_prog, **kwargs):
#     contents = r"""Lemma foo : forall _ : Type, Type.
# Proof (fun x => x)."""
#     output, cmds, retcode, runtime = get_coq_output(coqc_prog, ('-time', '-q'), contents, 1, verbose_base=3, **kwargs)
#     return 'Error: Attempt to save an incomplete proof' not in output
# 
# Path: custom_arguments.py
# DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)])
# 
# LOG_ALWAYS=None


import re, time
import split_definitions_old
import util
from subprocess import Popen, PIPE, STDOUT
from split_file import postprocess_split_proof_term
from coq_version import get_coq_accepts_time
from coq_running_support import get_proof_term_works_with_time
from custom_arguments import DEFAULT_LOG, LOG_ALWAYS
        for i in range(max((len(old_definitions), len(new_definitions)))):
            if i < len(old_definitions) and i < len(new_definitions):
                if old_definitions[i] == new_definitions[i]:
                    shared.append(old_definitions[i])
                else:
                    removed.append(old_definitions[i])
                    added.append(new_definitions[i])
            elif i < len(old_definitions):
                removed.append(old_definitions[i])
            elif i < len(new_definitions):
                added.append(new_definitions[i])
        return (tuple(removed), tuple(shared), tuple(added))
    else:
        return (tuple(i for i in old_definitions if i not in new_definitions),
                tuple(i for i in old_definitions if i in new_definitions),
                tuple(i for i in new_definitions if i not in old_definitions))

def strip_newlines(string):
    if not string: return string
    if string[0] == '\n': return string[1:]
    if string[-1] == '\n': return string[:-1]
    return string

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

# Path: split_file.py
# def postprocess_split_proof_term(statements, do_warn=True, **kwargs):
#     def do_warn_method(statement_num, statement, proof_term):
#         kwargs['log']("""Warning: Your version of Coq suffers from bug #5349 (https://coq.inria.fr/bugs/show_bug.cgi?id=5349)
# and does not support [Proof (term).] with -time.  Falling back to
# replacing [Proof (term).] with [Proof. exact (term). Qed.], which may fail.""")
#     if do_warn and 'log' in kwargs.keys():
#         do_warn = do_warn_method
#     else:
#         do_warn = None
#     return list(postprocess_split_proof_term_iter(statements, do_warn))
# 
# Path: coq_version.py
# def get_coq_accepts_time(coqc_prog, **kwargs):
#     return get_coq_accepts_option(coqc_prog, '-time', **kwargs)
# 
# Path: coq_running_support.py
# def get_proof_term_works_with_time(coqc_prog, **kwargs):
#     contents = r"""Lemma foo : forall _ : Type, Type.
# Proof (fun x => x)."""
#     output, cmds, retcode, runtime = get_coq_output(coqc_prog, ('-time', '-q'), contents, 1, verbose_base=3, **kwargs)
#     return 'Error: Attempt to save an incomplete proof' not in output
# 
# Path: custom_arguments.py
# DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)])
# 
# LOG_ALWAYS=None


# Path: split_definitions.py
import re, time
import split_definitions_old
import util
from subprocess import Popen, PIPE, STDOUT
from split_file import postprocess_split_proof_term
from coq_version import get_coq_accepts_time
from coq_running_support import get_proof_term_works_with_time
from custom_arguments import DEFAULT_LOG, LOG_ALWAYS

        for i in range(max((len(old_definitions), len(new_definitions)))):
            if i < len(old_definitions) and i < len(new_definitions):
                if old_definitions[i] == new_definitions[i]:
                    shared.append(old_definitions[i])
                else:
                    removed.append(old_definitions[i])
                    added.append(new_definitions[i])
            elif i < len(old_definitions):
                removed.append(old_definitions[i])
            elif i < len(new_definitions):
                added.append(new_definitions[i])
        return (tuple(removed), tuple(shared), tuple(added))
    else:
        return (tuple(i for i in old_definitions if i not in new_definitions),
                tuple(i for i in old_definitions if i in new_definitions),
                tuple(i for i in new_definitions if i not in old_definitions))

def strip_newlines(string):
    if not string: return string
    if string[0] == '\n': return string[1:]
    if string[-1] == '\n': return string[:-1]
    return string

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):