# Path: diagnose_error.py
# def get_coq_output(coqc_prog, coqc_prog_args, contents, timeout_val, cwd=None, is_coqtop=False, pass_on_stdin=False, verbose_base=1, retry_with_debug_when=(lambda output: 'is not a compiled interface for this version of OCaml' in output), **kwargs):
#     """Returns the coqc output of running through the given
#     contents.  Pass timeout_val = None for no timeout."""
#     if timeout_val is not None and timeout_val < 0 and get_timeout(coqc_prog) is not None:
#         return get_coq_output(coqc_prog, coqc_prog_args, contents, get_timeout(coqc_prog), cwd=cwd, is_coqtop=is_coqtop, pass_on_stdin=pass_on_stdin, verbose_base=verbose_base, retry_with_debug_when=retry_with_debug_when, **kwargs)
# 
#     key, file_name, cmds, input_val, cleaner = prepare_cmds_for_coq_output(coqc_prog, coqc_prog_args, contents, cwd=cwd, timeout_val=timeout_val, is_coqtop=is_coqtop, pass_on_stdin=pass_on_stdin, verbose_base=verbose_base, **kwargs)
# 
#     if key in COQ_OUTPUT.keys():
#         cleaner()
#         return COQ_OUTPUT[key][1]
# 
#     start = time.time()
#     ((stdout, stderr), returncode) = memory_robust_timeout_Popen_communicate(kwargs['log'], cmds, stderr=subprocess.STDOUT, stdout=subprocess.PIPE, stdin=subprocess.PIPE, timeout=(timeout_val if timeout_val is not None and timeout_val > 0 else None), input=input_val, cwd=cwd)
#     finish = time.time()
#     runtime = finish - start
#     kwargs['log']('\nretcode: %d\nstdout:\n%s\n\nstderr:\n%s\nruntime:\n%f\n\n' % (returncode, util.s(stdout), util.s(stderr), runtime),
#                   level=verbose_base + 1)
#     if get_timeout(coqc_prog) is None and timeout_val is not None:
#         set_timeout(coqc_prog, 3 * max((1, int(math.ceil(finish - start)))), **kwargs)
#     cleaner()
#     COQ_OUTPUT[key] = (file_name, (clean_output(util.s(stdout)), tuple(cmds), returncode, runtime))
#     kwargs['log']('Storing result: COQ_OUTPUT[%s]:\n%s' % (repr(key), repr(COQ_OUTPUT[key])),
#                   level=verbose_base + 2)
#     if retry_with_debug_when(COQ_OUTPUT[key][1][0]):
#         debug_args = get_coq_debug_native_compiler_args(coqc_prog)
#         kwargs['log']('Retrying with %s...' % ' '.join(debug_args),
#                       level=verbose_base - 1)
#         return get_coq_output(coqc_prog, list(debug_args) + list(coqc_prog_args), contents, timeout_val, cwd=cwd, is_coqtop=is_coqtop, pass_on_stdin=pass_on_stdin, verbose_base=verbose_base, retry_with_debug_when=(lambda output: False), **kwargs)
#     return COQ_OUTPUT[key][1]
# 
# Path: coq_version.py
# 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()


from diagnose_error import get_coq_output
from coq_version import get_coq_native_compiler_ondemand_fragment
from __future__ import with_statement

# Like coq_version.py, except for things that use get_coq_output (or
# perhaps a bit more generally for things that need to run coqc on a
# file)

__all__ = ["get_proof_term_works_with_time", "get_ltac_support_snippet"]

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

LTAC_SUPPORT_SNIPPET = {}
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 = {}

# Path: diagnose_error.py
# def get_coq_output(coqc_prog, coqc_prog_args, contents, timeout_val, cwd=None, is_coqtop=False, pass_on_stdin=False, verbose_base=1, retry_with_debug_when=(lambda output: 'is not a compiled interface for this version of OCaml' in output), **kwargs):
#     """Returns the coqc output of running through the given
#     contents.  Pass timeout_val = None for no timeout."""
#     if timeout_val is not None and timeout_val < 0 and get_timeout(coqc_prog) is not None:
#         return get_coq_output(coqc_prog, coqc_prog_args, contents, get_timeout(coqc_prog), cwd=cwd, is_coqtop=is_coqtop, pass_on_stdin=pass_on_stdin, verbose_base=verbose_base, retry_with_debug_when=retry_with_debug_when, **kwargs)
# 
#     key, file_name, cmds, input_val, cleaner = prepare_cmds_for_coq_output(coqc_prog, coqc_prog_args, contents, cwd=cwd, timeout_val=timeout_val, is_coqtop=is_coqtop, pass_on_stdin=pass_on_stdin, verbose_base=verbose_base, **kwargs)
# 
#     if key in COQ_OUTPUT.keys():
#         cleaner()
#         return COQ_OUTPUT[key][1]
# 
#     start = time.time()
#     ((stdout, stderr), returncode) = memory_robust_timeout_Popen_communicate(kwargs['log'], cmds, stderr=subprocess.STDOUT, stdout=subprocess.PIPE, stdin=subprocess.PIPE, timeout=(timeout_val if timeout_val is not None and timeout_val > 0 else None), input=input_val, cwd=cwd)
#     finish = time.time()
#     runtime = finish - start
#     kwargs['log']('\nretcode: %d\nstdout:\n%s\n\nstderr:\n%s\nruntime:\n%f\n\n' % (returncode, util.s(stdout), util.s(stderr), runtime),
#                   level=verbose_base + 1)
#     if get_timeout(coqc_prog) is None and timeout_val is not None:
#         set_timeout(coqc_prog, 3 * max((1, int(math.ceil(finish - start)))), **kwargs)
#     cleaner()
#     COQ_OUTPUT[key] = (file_name, (clean_output(util.s(stdout)), tuple(cmds), returncode, runtime))
#     kwargs['log']('Storing result: COQ_OUTPUT[%s]:\n%s' % (repr(key), repr(COQ_OUTPUT[key])),
#                   level=verbose_base + 2)
#     if retry_with_debug_when(COQ_OUTPUT[key][1][0]):
#         debug_args = get_coq_debug_native_compiler_args(coqc_prog)
#         kwargs['log']('Retrying with %s...' % ' '.join(debug_args),
#                       level=verbose_base - 1)
#         return get_coq_output(coqc_prog, list(debug_args) + list(coqc_prog_args), contents, timeout_val, cwd=cwd, is_coqtop=is_coqtop, pass_on_stdin=pass_on_stdin, verbose_base=verbose_base, retry_with_debug_when=(lambda output: False), **kwargs)
#     return COQ_OUTPUT[key][1]
# 
# Path: coq_version.py
# 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()


# Path: coq_running_support.py
from diagnose_error import get_coq_output
from coq_version import get_coq_native_compiler_ondemand_fragment

from __future__ import with_statement

# Like coq_version.py, except for things that use get_coq_output (or
# perhaps a bit more generally for things that need to run coqc on a
# file)

__all__ = ["get_proof_term_works_with_time", "get_ltac_support_snippet"]

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

LTAC_SUPPORT_SNIPPET = {}
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))