https://github.com/JasonGross/coq-tools
Tip revision: a47ed37e05cc2f848d43cb70a627db5c518ba0c0 authored by Jason Gross on 12 July 2022, 18:21:59 UTC
Remove path sensitivity in traceback output, test 12
Remove path sensitivity in traceback output, test 12
Tip revision: a47ed37
find-bug.py
#!/usr/bin/env python3
import tempfile, sys, os, re
import traceback
import custom_arguments
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
import split_definitions
from split_definitions import split_statements_to_definitions, join_definitions, get_preferred_passing, get_fallback_passing
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
import util
if PY3: raw_input = util.raw_input
import diagnose_error
# {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 os.name != 'nt' else os.path.join(SCRIPT_DIRECTORY, 'coqtop.bat')
parser = custom_arguments.ArgumentParser(description='Attempt to create a small file which reproduces a bug found in a large development.')
parser.add_argument('bug_file', metavar='BUGGY_FILE', type=argparse.FileType('r'),
help='a .v file which displays the bug')
parser.add_argument('output_file', metavar='OUT_FILE', type=str,
help='a .v file which will hold intermediate results, as well as the final reduced file')
parser.add_argument('temp_file', metavar='TEMP_FILE', nargs='?', type=str, default='',
help='a .v file which will be used to build up intermediate files while they are being tested')
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-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('--strip-newlines', dest='max_consecutive_newlines',
metavar='N', nargs='?', type=int, default=2,
help=("Passing `--strip-newlines N` will cause the " +
"program to, for all M > N, replace any " +
"instances of M consecutive newlines with N " +
"consecutive newlines. The result will be a " +
"file with no more than N consecutive newlines. " +
"Passing a negative number will disable this option. " +
"(Default: 2)"))
parser.add_argument('--no-admit-opaque', dest='admit_opaque',
action='store_const', const=False, default=True,
help=("Don't try to replace opaque things ([Qed] and [abstract])" +
"with [admit]s."))
parser.add_argument('--no-admit-transparent', dest='admit_transparent',
action='store_const', const=False, default=True,
help=("Don't try to replace transparent things with [admit]s."))
parser.add_argument('--no-admit-obligations', dest='admit_obligations',
action='store_const', const=False, default=True,
help=("Don't try to replace obligations with [Admit Obligations]."))
parser.add_argument('--no-admit', dest='admit_any',
action='store_const', const=False, default=True,
help=("Don't try to replace things with [admit]s."))
parser.add_argument('--no-aggressive', dest='aggressive',
action='store_const', const=False, default=True,
help=("Be less aggressive; don't try to remove _all_ definitions/lines."))
parser.add_argument('--no-remove-typeclasses', dest='save_typeclasses',
action='store_const', const=True, default=False,
help=("Don't remove Hints, Instances, or Canonical Structures; " +
"this should mostly preserve typeclass logs, and can be useful " +
"for debugging slow typeclass bugs."))
parser.add_argument('--ignore-coq-prog-args', dest='use_coq_prog_args',
action='store_const', const=False, default=True,
help=("Don't add extra arguments from a coq-prog-args file header."))
parser.add_argument('--dynamic-header', dest='dynamic_header', nargs='?', type=str,
default='(* File reduced by coq-bug-minimizer from %(old_header)s, then from %(original_line_count)d lines to %(final_line_count)d lines *)',
help=("A line to be placed at the top of the " +
"output file, followed by a newline. The " +
"variables original_line_count and " +
"final_line_count will be available for " +
"substitution. The variable old_header will" +
"have the previous contents of this comment. " +
"The default is " +
"`(* File reduced by coq-bug-minimizer from %%(old_header)s, then from %%(original_line_count)d lines to %%(final_line_count)d lines *)'"))
parser.add_argument('--header', dest='header', nargs='?', type=str,
default='(* coqc version %(coqc_version)s\n coqtop version %(coqtop_version)s%(module_inline_failure_string)s\n Expected coqc runtime on this file: %(recent_runtime).3f sec *)',
help=("A line to be placed at the top of the " +
"output file, below the dynamic header, " +
"followed by a newline. The variables " +
"coqtop_version and coqc_version will be " +
"available for substitution. The default is " +
"`(* coqc version %%(coqc_version)s\\n coqtop version %%(coqtop_version)s%%(module_inline_failure_string)s\\n Expected coqc runtime on this file: %%(recent_runtime).3f sec *)'"))
parser.add_argument('--no-strip-trailing-space', dest='strip_trailing_space',
action='store_const', const=False, default=True,
help=("Don't strip trailing spaces. By default, " +
"trailing spaces on each line are removed."))
parser.add_argument('--strict-whitespace', dest='strict_whitespace',
action='store_const', const=True, default=False,
help=("Strictly enforce whitespace matching in error " +
"messages. By default, locations where there " +
"are newlines followed by spaces are interchangable " +
"with any amount of spacing."))
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('--inline-coqlib', dest='inline_coqlib',
metavar='COQLIB', nargs='?', type=str,
help=("Attempt to inline requires from Coq's standard library,\n" +
"passing `-coqlib COQLIB' to coqc"))
parser.add_argument('--inline-user-contrib', dest='inline_user_contrib',
action='store_const', const=True, default=False,
help=("Attempt to inline requires from the user-contrib folder"))
parser.add_argument('--timeout', dest='timeout', metavar='SECONDS', type=int, default=-1,
help=("Use a timeout; make sure Coq is " +
"killed after running for this many seconds. " +
"If 0, there is no timeout. If negative, then " +
"twice the initial run of the script is used.\n\n" +
"Default: -1"))
parser.add_argument('--no-timeout', dest='timeout', action='store_const', const=0,
help=("Do not use a timeout"))
parser.add_argument('--passing-timeout', dest='passing_timeout', metavar='SECONDS', type=int, default=-1,
help=("Like --timeout, but only for the passing Coq"))
parser.add_argument('--nonpassing-timeout', dest='nonpassing_timeout', metavar='SECONDS', type=int, default=-1,
help=("Like --timeout, but only for the non-passing Coq"))
parser.add_argument('--no-minimize-before-inlining', dest='minimize_before_inlining',
action='store_const', const=False, default=True,
help=("Don't run the full minimization script before inlining [Requires], " +
"and between the inlining of every individual [Require].\n\n" +
"Note that this option will not work well in conjunction with " +
"--passing-coqc.\n"
"Passing this option results in a much more robust " +
"run; it removes the requirement that the compiled dependencies " +
"of the file being debugged remain in place for the duration of the run."))
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-is-coqtop', dest='coqc_is_coqtop', default=False, action='store_const', const=True,
help="Strip the .v and pass -load-vernac-source to the coqc programs; this allows you to pass `--coqc coqtop'")
parser.add_argument('--coqc-args', metavar='ARG', dest='coqc_args', type=str, action='append',
help=('Arguments to pass to coqc; e.g., " -indices-matter" (leading and trailing spaces are stripped)\n' +
'NOTE: If you want to pass an argument to both coqc and coqtop, use --arg="-indices-matter", not --coqc-args="-indices-matter"'))
parser.add_argument('--coqtop-args', metavar='ARG', dest='coqtop_args', type=str, action='append',
help=('Arguments to pass to coqtop; e.g., " -indices-matter" (leading and trailing spaces are stripped)\n' +
'NOTE: If you want to pass an argument to both coqc and coqtop, use --arg="-indices-matter", not --coqc-args="-indices-matter"'))
parser.add_argument('--coq_makefile', metavar='COQ_MAKEFILE', dest='coq_makefile', type=str, default='coq_makefile',
help='The path to the coq_makefile program.')
parser.add_argument('--passing-coqc', metavar='COQC', dest='passing_coqc', type=str, default='',
help='The path to the coqc program that should compile the file successfully.')
parser.add_argument('--passing-coqtop', metavar='COQTOP', dest='passing_coqtop', type=str, default='',
help=('The path to the coqtop program that should compile the file successfully.'))
parser.add_argument('--parse-with', choices=[split_definitions.PREFER_PASSING, split_definitions.PASSING, split_definitions.PREFER_NONPASSING, split_definitions.NONPASSING], dest='parse_with', type=str, default=split_definitions.PREFER_PASSING,
help=('Parse and split the document using coqc/coqtop vs passing-coqc/passing-coqtop (default: %s).' % split_definitions.PREFER_NONPASSING))
parser.add_argument('--base-dir', metavar='DIR', dest='base_dir', type=str, default='',
help='The path to the base directory from which coqc should be run')
parser.add_argument('--passing-base-dir', metavar='DIR', dest='passing_base_dir', type=str, default='',
help='The path to the base directory from which the passing coqc should be run')
parser.add_argument('--passing-coqc-args', metavar='ARG', dest='passing_coqc_args', type=str, action='append',
help='Arguments to pass to coqc so that it compiles the file successfully; e.g., " -indices-matter" (leading and trailing spaces are stripped)')
parser.add_argument('--nonpassing-coqc-args', metavar='ARG', dest='nonpassing_coqc_args', type=str, action='append',
help='Arguments to pass to coqc so that it compiles the file successfully; e.g., " -indices-matter" (leading and trailing spaces are stripped)')
parser.add_argument('--passing-coqtop-args', metavar='ARG', dest='passing_coqtop_args', type=str, action='append',
help=('Arguments to pass to coqtop so that it compiles the file successfully; e.g., " -indices-matter" (leading and trailing spaces are stripped)\n' +
'NOTE: If you want to pass an argument to both coqc and coqtop, use --nonpassing-arg="-indices-matter", not --coqc-args="-indices-matter"'))
parser.add_argument('--nonpassing-coqtop-args', metavar='ARG', dest='nonpassing_coqtop_args', type=str, action='append',
help=('Arguments to pass to coqtop so that it compiles the file successfully; e.g., " -indices-matter" (leading and trailing spaces are stripped)\n' +
'NOTE: If you want to pass an argument to both coqc and coqtop, use --nonpassing-arg="-indices-matter", not --coqc-args="-indices-matter"'))
parser.add_argument('--passing-coqc-is-coqtop', dest='passing_coqc_is_coqtop', default=False, action='store_const', const=True,
help="Strip the .v and pass -load-vernac-source to the coqc programs; this allows you to pass `--passing-coqc coqtop'")
parser.add_argument('--error-log', metavar='ERROR_LOG', dest='error_log', type=argparse.FileType('r'), default=None,
help='If given, ensure that the computed error message occurs in this log.')
parser.add_argument('-y', '--yes', '--assume-yes', dest='yes', action='store_true',
help='Automatic yes to prompts. Assume "yes" as answer to all prompts and run non-interactively.')
parser.add_argument('--no-color', dest='color_on', action='store_const', const=False, default=True,
help=("Don't color any log messages."))
add_libname_arguments(parser)
add_passing_libname_arguments(parser)
add_logging_arguments(parser)
SENSITIVE_TIMEOUT_RETRY_COUNT=3
@memoize
def re_compile(pattern, *args):
return re.compile(pattern, *args)
# memoize the compilation
def re_search(pattern, string, flags=0):
return re_compile(pattern, flags).search(string)
def ask(query, **kwargs):
if kwargs['yes']:
print(query)
return 'y'
else:
return raw_input(query)
def get_error_reg_string_of_output(output, **kwargs):
error_reg_string = ''
if diagnose_error.has_error(output):
error_string = diagnose_error.get_error_string(output)
error_reg_string = diagnose_error.make_reg_string(output, strict_whitespace=kwargs['strict_whitespace'])
kwargs['log']("\nI think the error is '%s'.\nThe corresponding regular expression is '%s'.\n" % (error_string, error_reg_string.replace('\\\n', '\\n').replace('\n', '\\n')), force_stdout=True, level=LOG_ALWAYS)
result = ''
while result not in ('y', 'n', 'yes', 'no'):
result = ask('Is this correct? [(y)es/(n)o] ', **kwargs).lower().strip()
if result in ('no', 'n'):
error_reg_string = ''
else:
kwargs['log']('\nThe current state of the file does not have a recognizable error.', level=LOG_ALWAYS)
if error_reg_string == '':
success = False
while not success:
error_reg_string = raw_input('\nPlease enter a regular expression which matches on the output. Leave blank to re-coq the file.\n')
try:
re.compile(error_reg_string)
except Exception as e:
kwargs['log']('\nThat regular expression does not compile: %s' % e, force_stdout=True, level=LOG_ALWAYS)
success = False
else:
success = True
while (error_reg_string != ''
and (not re.search(error_reg_string, output)
or len(re.search(error_reg_string, output).groups()) != 2)):
if not re.search(error_reg_string, output):
kwargs['log']('\nThe given regular expression does not match the output.', force_stdout=True, level=LOG_ALWAYS)
elif len(re.search(error_reg_string, output).groups()) != 2:
kwargs['log']('\nThe given regular expression does not have two groups.', force_stdout=True, level=LOG_ALWAYS)
kwargs['log']('It must first have one integer group which matches on the line number,', force_stdout=True, level=LOG_ALWAYS)
kwargs['log']('and second a group which matches on the error string.', force_stdout=True, level=LOG_ALWAYS)
error_reg_string = raw_input('Please enter a valid regular expression which matches on the output. Leave blank to re-coq the file (%s).\n'
% output_file_name)
return error_reg_string
def get_error_reg_string(output_file_name, **kwargs):
error_reg_string = ''
while error_reg_string == '':
kwargs['log']('\nCoqing the file (%s)...' % output_file_name)
contents = read_from_file(output_file_name)
diagnose_error.reset_timeout()
kwargs['log']('\nContents:\n\n%s\n\n' % contents, level=3)
output, cmds, retcode, runtime = diagnose_error.get_coq_output(kwargs['coqc'], kwargs['coqc_args'], contents, kwargs['timeout'], is_coqtop=kwargs['coqc_is_coqtop'], verbose_base=1, **kwargs)
result = ''
kwargs['log']("\nThis file produces the following output when Coq'ed:\n%s" % output, force_stdout=True, level=LOG_ALWAYS)
while result not in ('y', 'n', 'yes', 'no'):
result = ask('Does this output display the correct error? [(y)es/(n)o] ', **kwargs).lower().strip()
if result in ('n', 'no'):
raw_input('Please modify the file (%s) so that it errors correctly, and then press ENTER to continue, or ^C to break.' % output_file_name)
continue
error_reg_string = get_error_reg_string_of_output(output, **kwargs)
if error_reg_string == '':
continue
return error_reg_string
def escape_coq_prog_args(coq_prog_args):
return ' '.join('"' + arg.replace('\\', '\\\\').replace('"', r'\"') + '"'
for arg in coq_prog_args)
def unescape_coq_prog_args(coq_prog_args):
ret = []
cur = None
in_string = False
idx = 0
while idx < len(coq_prog_args):
cur_char = coq_prog_args[idx]
idx += 1
if not in_string:
if cur_char == '"':
in_string = True
cur = ''
elif cur_char not in ' \t':
DEFAULT_LOG("Warning: Invalid unquoted character '%s' at index %d in coq-prog-args '%s'" % (cur_char, idx - 1, coq_prog_args), level=LOG_ALWAYS)
return tuple(ret)
else:
if cur_char == '"':
in_string = False
ret.append(cur)
cur = None
elif cur_char == '\\':
if idx < len(coq_prog_args):
# take the next character
cur += coq_prog_args[idx]
idx += 1
else:
DEFAULT_LOG("Warning: Invalid backslash at end of coq-prog-args '%s'" % coq_prog_args, level=LOG_ALWAYS)
else:
cur += cur_char
return tuple(ret)
COQ_PROG_ARGS_REG = re.compile(r'coq-prog-args\s*:\s*\(([^\)]+)\)')
def get_coq_prog_args(contents):
return tuple(arg
for args in COQ_PROG_ARGS_REG.findall(contents)
for arg in unescape_coq_prog_args(args)
if arg not in ("-emacs", "-emacs-U"))
COQ_PROG_ARGS_REP = re.compile(r'[ \t]*\(\*+\s+-\*-\s+.*?\s-\*-\s+\*+\)\s*')
def strip_coq_prog_args(contents):
return COQ_PROG_ARGS_REP.sub('', contents)
def get_old_header(contents, header=''):
contents = strip_coq_prog_args(contents)
if header[:2] == '(*' and header[-2:] == '*)' and '*)' not in header[2:-2]:
pre_header = header[:header.index('%')]
if pre_header in contents and contents.index('*)') > contents.index(pre_header):
return contents[contents.index(pre_header)+len(pre_header):contents.index('*)')].strip()
return 'original input'
def prepend_header(contents, dynamic_header='', header='', header_dict={}, **kwargs):
"""Fills in the variables in the header for output files"""
contents = strip_coq_prog_args(contents)
if dynamic_header[:2] == '(*' and dynamic_header[-2:] == '*)' and '*)' not in dynamic_header[2:-2]:
pre_header = dynamic_header[:dynamic_header.index('%')]
if contents[:len(pre_header)] == pre_header:
# strip the old header
contents = contents[contents.index('*)')+2:]
if contents[0] == '\n': contents = contents[1:]
if header[:2] == '(*' and header[-2:] == '*)' and '*)' not in header[2:-2]:
pre_header = header[:header.index('%')]
if contents[:len(pre_header)] == pre_header:
# strip the old header
contents = contents[contents.index('*)')+2:]
if contents[0] == '\n': contents = contents[1:]
final_line_count = len(contents.split('\n'))
header_dict = dict(header_dict) # clone the dict
header_dict['final_line_count'] = final_line_count
header_dict['inline_failure_libnames'] = ', '.join(kwargs['inline_failure_libnames'])
header_dict['module_inline_failure_string'] = ('\n Modules that could not be inlined: %s' % header_dict['inline_failure_libnames'] if header_dict['inline_failure_libnames'] else '')
if 'old_header' not in header_dict.keys():
header_dict['old_header'] = 'original input'
use_header = (dynamic_header + '\n' + header) % header_dict
coq_prog_args = ('(* -*- mode: coq; coq-prog-args: ("-emacs" %s) -*- *)\n' % escape_coq_prog_args(kwargs['coqc_args'])
if len(kwargs['coqc_args']) > 0
else '')
## de-duplicate things in a list
## XXX This is a hack to deal with things like "from x lines to y lines, from x lines to y lines"
#if use_header[-3:] == ' *)':
# use_header = ','.join(OrderedSet(use_header[:-3].split(','))) + ' *)'
return '%s%s\n%s' % (coq_prog_args, use_header, contents)
INSTANCE_REG = re.compile(r"(?<![\w'])Instance\s")
CANONICAL_STRUCTURE_REG = re.compile(r"(?<![\w'])Canonical\s+Structure\s")
TC_HINT_REG = re.compile("(?<![\w'])Hint\s")
def get_header_dict(contents, old_header=None, original_line_count=0, **env):
coqc_version = get_coqc_version(env['coqc'], **env)
coqtop_version = get_coqtop_version(env['coqtop'], **env)
if old_header is None: old_header = get_old_header(contents, env['dynamic_header'])
return {'original_line_count':original_line_count,
'old_header':old_header,
'coqc_version':coqc_version,
'coqtop_version':coqtop_version,
'recent_runtime':0}
CONTENTS_UNCHANGED, CHANGE_SUCCESS, CHANGE_FAILURE = 'contents_unchanged', 'change_success', 'change_failure'
def classify_contents_change(old_contents, new_contents, ignore_coq_output_cache=False, reset_timeout=False, **kwargs):
# returns (RESULT_TYPE, PADDED_CONTENTS, OUTPUT_LIST, option BAD_INDEX, DESCRIPTION_OF_FAILURE_MODE, RUNTIME, EXTRA_VERBOSE_DESCRIPTION_OF_FAILURE_MODE_TUPLE_LIST)
kwargs['header_dict'] = kwargs.get('header_dict', get_header_dict(new_contents, original_line_count=len(old_contents.split('\n')), **env))
# this is a function, so that once we update the header dict with the runtime, we get the right header
def get_padded_contents(): return prepend_header(new_contents, **kwargs)
if new_contents == old_contents:
return (CONTENTS_UNCHANGED, get_padded_contents(), tuple(), None, 'No change. ', None, [])
if reset_timeout: diagnose_error.reset_timeout()
if ignore_coq_output_cache: diagnose_error.reset_coq_output_cache(kwargs['coqc'], kwargs['coqc_args'], new_contents, kwargs['timeout'], cwd=kwargs['base_dir'], is_coqtop=kwargs['coqc_is_coqtop'], verbose_base=2, **kwargs)
output, cmds, retcode, runtime = diagnose_error.get_coq_output(kwargs['coqc'], kwargs['coqc_args'], new_contents, kwargs['timeout'], cwd=kwargs['base_dir'], is_coqtop=kwargs['coqc_is_coqtop'], verbose_base=2, **kwargs)
if diagnose_error.has_error(output, kwargs['error_reg_string']):
if kwargs['passing_coqc']:
if ignore_coq_output_cache: diagnose_error.reset_coq_output_cache(kwargs['passing_coqc'], kwargs['passing_coqc_args'], new_contents, kwargs['passing_timeout'], cwd=kwargs['passing_base_dir'], is_coqtop=kwargs['passing_coqc_is_coqtop'], verbose_base=2, **kwargs)
passing_output, cmds, passing_retcode, passing_runtime = diagnose_error.get_coq_output(kwargs['passing_coqc'], kwargs['passing_coqc_args'], new_contents, kwargs['passing_timeout'], cwd=kwargs['passing_base_dir'], is_coqtop=kwargs['passing_coqc_is_coqtop'], verbose_base=2, **kwargs)
if not (diagnose_error.has_error(passing_output) or diagnose_error.is_timeout(passing_output)):
# we return passing_runtime, under the presumption
# that in Coq's test-suite, the file should pass, and
# so this is a better indicator of how long it'll take
kwargs['header_dict']['recent_runtime'] = passing_runtime
return (CHANGE_SUCCESS, get_padded_contents(), (output, passing_output), None, 'Change successful. ', passing_runtime, [])
else:
return (CHANGE_FAILURE, get_padded_contents(), (output, passing_output), 1, 'The alternate coqc (%s) was supposed to pass, but instead emitted an error. ' % kwargs['passing_coqc'], runtime, [])
else:
kwargs['header_dict']['recent_runtime'] = runtime
return (CHANGE_SUCCESS, get_padded_contents(), (output,), None, 'Change successful. ', runtime, [])
else:
extra_desc = ''
extra_desc_list = [(2, 'The error was:\n%s\n' % output)]
return (CHANGE_FAILURE, get_padded_contents(), (output,), 0, extra_desc, runtime, extra_desc_list)
def check_change_and_write_to_file(old_contents, new_contents, output_file_name,
unchanged_message='No change.', success_message='Change successful.',
failure_description='make a change', changed_description='Changed file',
timeout_retry_count=1, ignore_coq_output_cache=False,
verbose_base=1, display_source_to_error=False,
write_to_temp_file=False,
**kwargs):
kwargs['log']('Running coq on the file\n"""\n%s\n"""' % new_contents, level=2 + verbose_base)
change_result, contents, outputs, output_i, error_desc, runtime, error_desc_verbose_list = classify_contents_change(old_contents, new_contents, ignore_coq_output_cache=ignore_coq_output_cache, **kwargs)
if change_result == CONTENTS_UNCHANGED:
kwargs['log']('\n%s' % unchanged_message, level=verbose_base)
return False
elif change_result == CHANGE_SUCCESS:
kwargs['log'](util.color('\n%s' % success_message, util.colors.OKGREEN, kwargs['color_on']), level=verbose_base)
write_to_file(output_file_name, contents)
return True
elif change_result == CHANGE_FAILURE:
kwargs['log']('\nNon-fatal error: Failed to %s and preserve the error. %s' % (failure_description, error_desc), level=verbose_base)
for lvl, msg in error_desc_verbose_list: kwargs['log'](msg, level=lvl)
if write_to_temp_file and not kwargs['remove_temp_file']: kwargs['log']('Writing %s to %s.' % (changed_description.lower(), kwargs['temp_file_name']), level=verbose_base)
kwargs['log']('The new error was:', level=verbose_base)
kwargs['log'](outputs[output_i], level=verbose_base)
kwargs['log']('All Outputs:\n%s' % '\n'.join(outputs), level=verbose_base+2)
if write_to_temp_file and not kwargs['remove_temp_file']:
write_to_file(kwargs['temp_file_name'], contents)
else:
kwargs['log'](util.color('%s not saved.' % changed_description, util.colors.WARNING, kwargs['color_on']), level=verbose_base)
if timeout_retry_count > 1 and diagnose_error.is_timeout(outputs[output_i]):
kwargs['log']('\nRetrying another %d time%s...' % (timeout_retry_count - 1, 's' if timeout_retry_count > 2 else ''), level=verbose_base)
return check_change_and_write_to_file(old_contents, new_contents, output_file_name,
unchanged_message=unchanged_message, success_message=success_message,
failure_description=failure_description, changed_description=changed_description,
timeout_retry_count=timeout_retry_count-1, ignore_coq_output_cache=True,
verbose_base=verbose_base,
write_to_temp_file=write_to_temp_file,
**kwargs)
elif display_source_to_error and diagnose_error.has_error(outputs[output_i]):
new_line = diagnose_error.get_error_line_number(outputs[output_i])
new_start, new_end = diagnose_error.get_error_byte_locations(outputs[output_i])
new_contents_lines = new_contents.split('\n')
new_contents_to_error, new_contents_rest = '\n'.join(new_contents_lines[:new_line-1]), '\n'.join(new_contents_lines[new_line-1:])
kwargs['log']('The file generating the error was:', level=verbose_base)
kwargs['log']('%s\n%s\n' % (new_contents_to_error,
new_contents_rest.encode('utf-8')[:new_end].decode('utf-8')), level=verbose_base)
return False
else:
kwargs['log']('ERROR: Unrecognized change result %s on\nclassify_contents_change(\n %s\n ,%s\n)\n%s'
% (change_result, repr(old_contents), repr(new_contents),
repr((change_result, contents, outputs, output_i, error_desc, runtime, error_desc_verbose_list))),
level=LOG_ALWAYS)
return None
def try_transform_each(definitions, output_file_name, transformer, skip_n=1, **kwargs):
"""Tries to apply transformer to each definition in definitions,
additionally passing in the list of subsequent definitions. If
the returned value of the 'statement' key is not equal to the old
value, or if the return value is a false-y value (indicating that
we should remove the line) then we see if the error is still
present. If it is, we keep the change; otherwise, we discard it.
The order in which definitions are passed in is guaranteed to be
reverse-order.
Returns updated definitions."""
kwargs['log']('try_transform_each', level=3)
original_definitions = [dict(i) for i in definitions]
# TODO(jgross): Use coqtop and [BackTo] to do incremental checking
success = False
i = len(definitions) - 1 - skip_n
while i >= 0:
old_definition = definitions[i]
new_definition = transformer(old_definition, definitions[i + 1:])
if not new_definition:
if kwargs['save_typeclasses'] and \
(INSTANCE_REG.search(old_definition['statement']) or
CANONICAL_STRUCTURE_REG.search(old_definition['statement']) or
TC_HINT_REG.search(old_definition['statement'])):
kwargs['log']('Ignoring Instance/Canonical Structure/Hint: %s' % old_definition['statement'], level=3)
i -= 1
continue
new_definitions = []
elif isinstance(new_definition, dict):
if not new_definition['statement'].strip(): new_definitions = []
else: new_definitions = [new_definition]
else: new_definitions = list(new_definition)
if len(new_definitions) != 1 or \
re.sub(r'\s+', ' ', old_definition['statement']).strip() != re.sub(r'\s+', ' ', new_definitions[0]['statement']).strip():
if len(new_definitions) == 0:
kwargs['log']('Attempting to remove %s' % repr(old_definition['statement']),
level=2)
try_definitions = definitions[:i] + definitions[i + 1:]
else:
kwargs['log']('Attempting to transform %s\ninto\n%s' % (old_definition['statement'], ''.join(defn['statement'] for defn in new_definitions)),
level=2)
if len(new_definitions) > 1: kwargs['log']('Splitting definition: %s' % repr(new_definitions), level=2)
try_definitions = definitions[:i] + new_definitions + definitions[i + 1:]
if check_change_and_write_to_file('', join_definitions(try_definitions), output_file_name, verbose_base=2, **kwargs):
success = True
definitions = try_definitions
# make a copy for saving
save_definitions = [dict(defn) for defn in try_definitions]
else:
kwargs['log']('No change to %s' % old_definition['statement'], level=3)
i -= 1
if success:
kwargs['log'](kwargs['noun_description'] + ' successful')
if join_definitions(save_definitions) != join_definitions(definitions):
kwargs['log']('Probably fatal error: definitions != save_definitions', level=LOG_ALWAYS)
else:
contents = prepend_header(join_definitions(definitions), **kwargs)
write_to_file(output_file_name, contents)
return definitions
else:
kwargs['log'](kwargs['noun_description'] + ' unsuccessful.')
return original_definitions
def try_transform_reversed(definitions, output_file_name, transformer, skip_n=1, **kwargs):
"""Replaces each definition in definitions, with transformer
applied to that definition and the subsequent (transformed)
definitions. If transformer returns a false-y value, the
definition is removed. After transforming the entire list, we see
if the error is still present. If it is, we keep the change;
otherwise, we discard it. The order in which definitions are
passed in is guaranteed to be reverse-order.
Returns updated definitions."""
kwargs['log']('try_transform_reversed', level=3)
definitions = list(definitions) # clone the list of definitions
original_definitions = list(definitions)
kwargs['log'](len(definitions), level=3)
kwargs['log'](definitions, level=3)
for i in reversed(list(range(len(definitions) - skip_n))):
new_definition = transformer(definitions[i], definitions[i + 1:])
if new_definition:
if definitions[i] != new_definition:
kwargs['log']('Transforming %s into %s' % (definitions[i]['statement'], new_definition['statement']),
level=2)
else:
kwargs['log']('No change to %s' % new_definition['statement'], level=3)
definitions[i] = new_definition
else:
if kwargs['save_typeclasses'] and \
(INSTANCE_REG.search(definitions[i]['statement']) or
CANONICAL_STRUCTURE_REG.search(definitions[i]['statement']) or
TC_HINT_REG.search(definitions[i]['statement'])):
kwargs['log']('Ignoring Instance/Canonical Structure/Hint: %s' % definitions[i]['statement'], level=3)
pass
else:
kwargs['log']('Removing %s' % definitions[i]['statement'], level=2)
definitions = definitions[:i] + definitions[i + 1:]
if check_change_and_write_to_file('', join_definitions(definitions), output_file_name,
success_message=kwargs['noun_description']+' successful.', failure_description=kwargs['verb_description'],
changed_description='Intermediate code', **kwargs):
return definitions
return original_definitions
def try_transform_reversed_or_else_each(definitions, *args, **kwargs):
"""Invokes try_transform_reversed. If there are no changes, then try_transform_each is tried."""
old_definitions = join_definitions(definitions) # for comparison,
# to see if things have changed first, try to do everything at
# once; python cycles are assumed to be cheap in comparison to coq
# cycles
definitions = try_transform_reversed(definitions, *args, **kwargs)
new_definitions = join_definitions(definitions)
if new_definitions == old_definitions:
# we failed to do everything at once, try the simple thing and
# try to admit each individually
kwargs['log']('Failed to do everything at once; trying one at a time.')
definitions = try_transform_each(definitions, *args, **kwargs)
new_definitions = join_definitions(definitions)
if new_definitions == old_definitions:
kwargs['log']('No successful changes.')
else:
kwargs['log']('Success!')
return definitions
def try_remove_if_not_matches_transformer(definition_found_in, **kwargs):
def transformer(cur_definition, rest_definitions):
if any(definition_found_in(cur_definition, future_definition)
for future_definition in rest_definitions):
kwargs['log']('Definition found; found:\n%s\nin\n%s'
% (cur_definition,
[future_definition['statement']
for future_definition in rest_definitions
if definition_found_in(cur_definition, future_definition)][0]),
level=3)
return cur_definition
else:
return None
return transformer
# don't count things like [Section ...], [End ...]
EXCLUSION_REG = re.compile(r"^\s*Section\s+[^\.]+\.\s*$" +
r"|^\s*Module\s+[^\.]+\.\s*$" +
r"|^\s*End\s+[^\.]+\.\s*$" +
r"|^\s*Require\s+[^\.]+\.\s*$" +
r"|^\s*Import\s+[^\.]+\.\s*$" +
r"|^\s*Export\s+[^\.]+\.\s*$")
def try_remove_if_name_not_found_in_transformer(get_names, **kwargs):
def definition_found_in(cur_definition, future_definition):
names = get_names(cur_definition)
if len(names) == 0:
return True
elif EXCLUSION_REG.search(future_definition['statement']):
return False # we don't care if the name is found in a
# statement like [Section ...] or [End ...]
return any(re_search(r"(?<![\w'])%s(?![\w'])" % re.escape(name), future_definition['statement'])
for name in names)
return try_remove_if_not_matches_transformer(definition_found_in, **kwargs)
def try_remove_if_name_not_found_in_section_transformer(get_names, **kwargs):
SECTION_BEGIN_REG = re.compile(r'^\s*(?:Section|Module)\s+[^\.]+\.\s*$')
SECTION_END_REG = re.compile(r'^\s*End\s+[^\.]+\.\s*$')
def transformer(cur_definition, rest_definitions):
names = get_names(cur_definition)
if len(names) == 0:
return cur_definition
section_level = 0
for future_definition in rest_definitions:
if section_level < 0:
break
if SECTION_BEGIN_REG.match(future_definition['statement']):
section_level += 1
elif SECTION_END_REG.match(future_definition['statement']):
section_level -= 1
elif any(re_search(r"(?<![\w'])%s(?![\w'])" % re.escape(name), future_definition['statement'])
for name in names):
return cur_definition
# we didn't find the name, so we can safely remove it
return None
return transformer
def try_remove_non_instance_definitions(definitions, output_file_name, **kwargs):
def get_names(definition):
if INSTANCE_REG.search(definition['statements'][0]):
return tuple()
elif CANONICAL_STRUCTURE_REG.search(definition['statements'][0]):
return tuple()
else:
return definition.get('terms_defined', tuple())
return try_transform_reversed(definitions, output_file_name,
try_remove_if_name_not_found_in_transformer(get_names, **kwargs),
noun_description='Non-instance definition removal',
verb_description='remove non-instance definitions',
**kwargs)
def try_remove_definitions(definitions, output_file_name, **kwargs):
return try_transform_reversed(definitions, output_file_name,
try_remove_if_name_not_found_in_transformer(lambda definition: definition.get('terms_defined', tuple()), **kwargs),
noun_description='Definition removal',
verb_description='remove definitions',
**kwargs)
def try_remove_each_definition(definitions, output_file_name, **kwargs):
return try_transform_each(definitions, output_file_name,
try_remove_if_name_not_found_in_transformer(lambda definition: definition.get('terms_defined', tuple()), **kwargs),
noun_description='Definition removal',
verb_description='remove definitions',
**kwargs)
def try_remove_each_and_every_line(definitions, output_file_name, **kwargs):
return try_transform_each(definitions, output_file_name,
(lambda cur_definition, rest_definitions: False),
noun_description='Line removal',
verb_description='remove lines',
**kwargs)
ABORT_REG = re.compile(r'\sAbort\s*\.\s*$')
def try_remove_aborted(definitions, output_file_name, **kwargs):
return try_transform_reversed(definitions, output_file_name,
(lambda definition, rest:
None if ABORT_REG.search(definition['statement']) else definition),
noun_description='Aborted removal',
verb_description='remove Aborts',
**kwargs)
LTAC_REG = re.compile(r'^\s*(?:Local\s+|Global\s+)?Ltac\s+([^\s]+)', flags=re.MULTILINE)
def try_remove_ltac(definitions, output_file_name, **kwargs):
return try_transform_reversed(definitions, output_file_name,
try_remove_if_name_not_found_in_transformer(lambda definition: LTAC_REG.findall(definition['statement'].replace(':', '\
: ')),
**kwargs),
noun_description='Ltac removal',
verb_description='remove Ltac',
**kwargs)
DEFINITION_ISH = r'Variables|Variable|Hypotheses|Hypothesis|Parameters|Parameter|Axioms|Axiom|Conjectures|Conjecture'
HINT_REG = re.compile(r'^\s*' +
r'(?:Local\s+|Global\s+|Polymorphic\s+|Monomorphic\s+)*' +
r'(?:' +
r'Definition|Fixpoint|Record|Inductive' +
r'|Coinductive|CoFixpoint' +
r'|Set\s+Universe\s+Polymorphism' +
r'|Unet\s+Universe\s+Polymorphism' +
r'|' + DEFINITION_ISH +
r')\.?(?:\s+|$)')
def try_remove_hints(definitions, output_file_name, **kwargs):
return try_transform_each(definitions, output_file_name,
(lambda definition, rest:
(None
if len(definition['statements']) == 1 and \
not HINT_REG.match(definition['statement'])
else definition)),
noun_description='Hint removal',
verb_description='remove hints',
**kwargs)
VARIABLE_REG = re.compile(r'^\s*' +
r'(?:Local\s+|Global\s+|Polymorphic\s+|Monomorphic\s+)*' +
r'(?:' + DEFINITION_ISH + r')\s+' +
r'([^\.:]+)',
flags=re.MULTILINE)
def try_remove_variables(definitions, output_file_name, **kwargs):
def get_names(definition):
terms = VARIABLE_REG.findall(definition['statement'])
return [i for i in sorted(set(j
for term in terms
for j in term.split(' ')))]
return try_transform_reversed(definitions, output_file_name,
try_remove_if_name_not_found_in_section_transformer(get_names, **kwargs),
noun_description='Variable removal',
verb_description='remove variables',
**kwargs)
CONTEXT_REG = re.compile(r'^\s*' +
r'(?:Local\s+|Global\s+|Polymorphic\s+|Monomorphic\s+)*' +
r'Context\s*`\s*[\({]\s*([^:\s]+)\s*:',
flags=re.MULTILINE)
def try_remove_contexts(definitions, output_file_name, **kwargs):
return try_transform_reversed(definitions, output_file_name,
try_remove_if_name_not_found_in_section_transformer(lambda definition: CONTEXT_REG.findall(definition['statement'].replace(':', ' : ')), **kwargs),
noun_description='Context removal',
verb_description='remove Contexts',
**kwargs)
def try_admit_abstracts(definitions, output_file_name, **kwargs):
def do_call(method, definitions, agressive):
return method(definitions, output_file_name,
(lambda definition, rest_definitions:
transform_abstract_to_admit(definition, rest_definitions, agressive=agressive, log=kwargs['log'])),
noun_description='Admitting [abstract ...]',
verb_description='[abstract ...] admits',
**kwargs)
old_definitions = join_definitions(definitions)
# for comparison, to see if things have changed first, try to do
# everything at once; python cycles are assumed to be cheap in
# comparison to coq cycles
definitions = do_call(try_transform_reversed, definitions, True)
new_definitions = join_definitions(definitions)
if new_definitions != old_definitions:
kwargs['log']('Success with [abstract ...] admits on try_transform_reversed, agressive: True, definitions:\n%s'
% new_definitions,
level=3)
return definitions
# try the other options, each less agressive than the last
definitions = do_call(try_transform_reversed, definitions, False)
new_definitions = join_definitions(definitions)
if new_definitions != old_definitions:
kwargs['log']('Success with [abstract ...] admits on try_transform_reversed, agressive: False, definitions:\n%s'
% new_definitions,
level=3)
return definitions
definitions = do_call(try_transform_each, definitions, True)
new_definitions = join_definitions(definitions)
if new_definitions != old_definitions:
kwargs['log']('Success with [abstract ...] admits on try_transform_each, agressive: True, definitions:\n%s'
% new_definitions,
level=3)
return definitions
definitions = do_call(try_transform_each, definitions, False)
new_definitions = join_definitions(definitions)
if new_definitions != old_definitions:
kwargs['log']('Success with [abstract ...] admits on try_transform_each, agressive: False, definitions:\n%s'
% new_definitions, level=3)
else:
kwargs['log']('Failure with [abstract ...] admits.', level=3)
return definitions
def make_try_admit_matching_definitions(matcher, use_admitted=False, **kwargs):
def transformer(cur_definition, rest_definitions):
if len(cur_definition['statements']) > 2 and matcher(cur_definition):
statements = (cur_definition['statements'][0], 'Admitted.') if use_admitted else (cur_definition['statements'][0], 'admit.', 'Defined.')
return {'statements':statements,
'statement':'\n'.join(statements),
'terms_defined':cur_definition['terms_defined']}
else:
return cur_definition
def try_admit_matching_definitions(definitions, output_file_name, **kwargs2):
return try_transform_reversed_or_else_each(definitions, output_file_name, transformer, **dict(list(kwargs.items()) + list(kwargs2.items())))
return try_admit_matching_definitions
def make_try_admit_qeds(**kwargs):
QED_REG = re.compile(r"(?<![\w'])Qed\s*\.\s*$", flags=re.MULTILINE)
return make_try_admit_matching_definitions((lambda definition: QED_REG.search(definition['statement'])),
noun_description='Admitting Qeds',
verb_description='admit Qeds',
**kwargs)
def make_try_admit_lemmas(**kwargs):
LEMMA_REG = re.compile(r'^\s*' +
r'(?:Local\s+|Global\s+|Polymorphic\s+|Monomorphic\s+)*' +
r'(?:Lemma|Remark|Fact|Corollary|Proposition)\s*', flags=re.MULTILINE)
return make_try_admit_matching_definitions((lambda definition: LEMMA_REG.search(definition['statement'])),
noun_description='Admitting lemmas',
verb_description='admit lemmas',
**kwargs)
def make_try_admit_definitions(**kwargs):
return make_try_admit_matching_definitions((lambda definition: True),
noun_description='Admitting definitions',
verb_description='admit definitions',
**kwargs)
def try_split_imports(definitions, output_file_name, **kwargs):
def transformer(cur_definition, rest_definitions):
if (len(cur_definition['statements']) > 1
or any(ch in cur_definition['statement'] for ch in '*()')
or cur_definition['statement'].strip()[-1] != '.'
or cur_definition['statement'].strip().replace('\n', ' ').split(' ')[0] not in ('Import', 'Export')):
return cur_definition
else:
terms = [i for i in cur_definition['statement'].strip().replace('\n', ' ')[:-1].split(' ') if i != '']
import_or_export, terms = terms[0], terms[1:]
pat = import_or_export + ' %s.'
rtn_part = dict(cur_definition)
rtn = []
for term in terms:
rtn_part['statement'] = pat % term
rtn_part['statements'] = (pat % term,)
rtn.append(dict(rtn_part))
return tuple(rtn)
return try_transform_each(definitions, output_file_name,
transformer,
noun_description='Import/Export splitting',
verb_description='split Imports/Exports',
**kwargs)
def try_admit_matching_obligations(definitions, output_file_name, matcher, **kwargs):
OBLIGATION_REG = re.compile(r"^\s*(Next\s+Obligation|Obligation\s+[0-9]+)\b", flags=re.DOTALL)
def transformer(cur_definition, rest_definitions):
if len(cur_definition['statements']) > 1 and OBLIGATION_REG.match(cur_definition['statements'][0]) and matcher(cur_definition):
statements = ('Admit Obligations.',)
return {'statements':statements,
'statement':'\n'.join(statements),
'terms_defined':cur_definition['terms_defined']}
else:
return cur_definition
return try_transform_reversed_or_else_each(definitions, output_file_name, transformer, **kwargs)
def try_admit_qed_obligations(definitions, output_file_name, **kwargs):
QED_REG = re.compile(r"(?<![\w'])(Qed|Admitted)\s*\.\s*$", flags=re.MULTILINE)
return try_admit_matching_obligations(definitions, output_file_name,
(lambda definition: QED_REG.search(definition['statement'])),
noun_description='Admitting Qed Obligations',
verb_description='admit Qed Obligations',
**kwargs)
def try_admit_obligations(definitions, output_file_name, **kwargs):
return try_admit_matching_obligations(definitions, output_file_name,
(lambda definition: True),
noun_description='Admitting Obligations',
verb_description='admit Obligations',
**kwargs)
def try_split_oneline_definitions(definitions, output_file_name, **kwargs):
def update_paren(in_string, paren_count, new_string):
for ch in new_string:
if in_string:
if ch == '"': in_string = False
else:
if ch == '"':
in_string = True
elif ch == '(':
paren_count += 1
elif ch == ')':
paren_count -= 1
return (in_string, paren_count)
def transformer(cur_definition, rest_definitions):
if (len(cur_definition['statements']) > 1
or cur_definition['statement'].strip()[-1] != '.'
or ':=' not in cur_definition['statement']
or len(cur_definition['terms_defined']) != 1):
return cur_definition
else:
terms = cur_definition['statement'].strip()[:-1].split(':=')
pre_statement = terms[0]
in_string, paren_count = update_paren(False, 0, pre_statement)
for i, term in list(enumerate(terms))[1:]:
if not in_string and paren_count == 0:
rtn_part = dict(cur_definition)
rtn_part['statements'] = (pre_statement.rstrip() + '.',
'exact (%s).' % ':='.join(terms[i:]).strip(),
'Defined.')
rtn_part['statement'] = ' '.join(rtn_part['statements'])
return rtn_part
else:
in_string, paren_count = update_paren(in_string, paren_count, term)
pre_statement = ':=' + term
return cur_definition
return try_transform_each(definitions, output_file_name,
transformer,
noun_description='One-line definition splitting',
verb_description='split one-line definitions',
**kwargs)
MODULE_REG = re.compile(r'^(\s*Module)(\s+[^\s\.]+\s*\.\s*)$')
def try_export_modules(definitions, output_file_name, **kwargs):
def transformer(cur_definition, rest_definitions):
if (len(cur_definition['statements']) > 1 or
not MODULE_REG.match(cur_definition['statement'])):
return cur_definition
else:
new_statement = MODULE_REG.sub(r'\1 Export\2', cur_definition['statement'])
rtn = dict(cur_definition)
rtn['statement'] = new_statement
rtn['statements'] = (new_statement, )
return rtn
return try_transform_each(definitions, output_file_name,
transformer,
noun_description='Module exportation',
verb_description='export modules',
**kwargs)
def try_strip_comments(output_file_name, **kwargs):
contents = read_from_file(output_file_name)
old_contents = contents
new_contents = strip_comments(contents)
check_change_and_write_to_file(old_contents, new_contents, output_file_name,
unchanged_message='No strippable comments.',
success_message='Succeeded in stripping comments.',
failure_description='strip comments',
changed_descruption='Stripped comments file',
**kwargs)
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)
coqc_help = get_coqc_help(get_preferred_passing('coqc', **env), **env)
env['header_dict'] = get_header_dict(contents, **env)
if not check_change_and_write_to_file('', contents, output_file_name,
unchanged_message='Invalid empty file!', success_message='Sanity check passed.',
failure_description='validate all coq runs', changed_description='File',
timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT,
write_to_temp_file=True,
**env):
if os.path.exists(output_file_name):
env['log']('\nMoving %s to %s...' % (output_file_name, env['temp_file_name']))
write_to_file(env['temp_file_name'], read_from_file(output_file_name))
os.remove(output_file_name)
return die('Fatal error: Sanity check failed.', **env)
if env['max_consecutive_newlines'] >= 0 or env['strip_trailing_space']:
env['log']('\nNow, I will attempt to strip repeated newlines and trailing spaces from this file...')
try_strip_newlines(output_file_name, **env)
contents = read_from_file(output_file_name)
original_line_count = len(contents.split('\n'))
env['header_dict']['original_line_count'] = original_line_count
env['log']('\nNow, I will attempt to strip the comments from this file...')
try_strip_comments(output_file_name, **env)
env['log']('\nNow, I will attempt to factor out all of the [Require]s...')
try_normalize_requires(output_file_name, **env)
env['log']('\nNow, I will attempt to split up [Require] statements...')
try_split_requires(output_file_name, **env)
contents = read_from_file(output_file_name)
env['log']('\nIn order to efficiently manipulate the file, I have to break it into statements. I will attempt to do this by matching on periods.')
strings = re.findall(r'"[^"\n\r]+"', contents)
bad_strings = [i for i in strings if re.search(r'(?<=[^\.]\.\.\.)\s|(?<=[^\.]\.)\s', i)]
if bad_strings:
env['log']('If you have periods in strings, and these periods are essential to generating the error, then this process will fail. Consider replacing the string with some hack to get around having a period and then a space, like ["a. b"%string] with [("a." ++ " b")%string].')
env['log']('You have the following strings with periods in them:\n%s' % '\n'.join(bad_strings))
statements = split_coq_file_contents(contents)
if not check_change_and_write_to_file('', '\n'.join(statements), output_file_name,
unchanged_message='Invalid empty file!',
success_message='Splitting successful.',
failure_description='split file to statements',
changed_description='Split',
timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT,
**env):
env['log']('I will not be able to proceed.')
env['log']('re.search(' + repr(env['error_reg_string']) + ', <output above>)', level=2)
return die(None, **env)
env['log']('\nI will now attempt to remove any lines after the line which generates the error.')
output, cmds, retcode, runtime = diagnose_error.get_coq_output(env['coqc'], env['coqc_args'], '\n'.join(statements), env['timeout'], is_coqtop=env['coqc_is_coqtop'], verbose_base=2, **env)
line_num = diagnose_error.get_error_line_number(output, env['error_reg_string'])
try_strip_extra_lines(output_file_name, line_num, **env)
env['log']('\nIn order to efficiently manipulate the file, I have to break it into definitions. I will now attempt to do this.')
contents = read_from_file(output_file_name)
statements = split_coq_file_contents(contents)
env['log']('I am using the following file: %s' % '\n'.join(statements), level=3)
definitions = split_statements_to_definitions(statements, **env)
if not check_change_and_write_to_file('', join_definitions(definitions), output_file_name,
unchanged_message='Invalid empty file!',
success_message='Splitting to definitions successful.',
failure_description='split file to definitions',
changed_description='Split',
timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT,
**env):
env['log']('I will not be able to proceed.')
env['log']('re.search(' + repr(env['error_reg_string']) + ', <output above>)', level=2)
return die(None, **env)
recursive_tasks = (('remove goals ending in [Abort.]', try_remove_aborted),
('remove unused Ltacs', try_remove_ltac),
('remove unused definitions', try_remove_definitions),
('remove unused non-instance, non-canonical structure definitions', try_remove_non_instance_definitions),
('remove unused variables', try_remove_variables),
('remove unused contexts', try_remove_contexts))
tasks = recursive_tasks
if env['admit_opaque']:
if env['admit_obligations']:
tasks += (('replace Qed Obligation with Admit Obligations', try_admit_qed_obligations),)
tasks += ((('replace Qeds with Admitteds', make_try_admit_qeds(use_admitted=True)),
('replace Qeds with admit. Defined.', make_try_admit_qeds(use_admitted=False))) +
# we've probably just removed a lot, so try to remove definitions again
recursive_tasks +
(('admit [abstract ...]s', try_admit_abstracts),) +
# we've probably just removed a lot, so try to remove definitions again
recursive_tasks)
if not env['aggressive']:
tasks += (('remove unused definitions, one at a time', try_remove_each_definition),)
if env['admit_transparent']:
if env['admit_obligations']:
tasks += (('replace Obligation with Admit Obligations', try_admit_obligations),)
tasks += (('admit lemmas with Admitted', make_try_admit_lemmas(use_admitted=True)),
('admit definitions with Admitted', make_try_admit_definitions(use_admitted=True)),
('admit lemmas with admit. Defined', make_try_admit_lemmas(use_admitted=False)),
('admit definitions with admit. Defined', make_try_admit_definitions(use_admitted=False)))
if not env['aggressive'] and not env['save_typeclasses']:
tasks += (('remove hints', try_remove_hints),)
tasks += (('export modules', try_export_modules),
('split imports and exports', try_split_imports),
('split := definitions', try_split_oneline_definitions))
if env['aggressive']:
tasks += ((('remove all lines, one at a time', try_remove_each_and_every_line),) +
# we've probably just removed a lot, so try to remove definitions again
recursive_tasks)
old_definitions = ''
while old_definitions != join_definitions(definitions):
old_definitions = join_definitions(definitions)
env['log']('Definitions:', level=2)
env['log'](definitions, level=2)
for description, task in tasks:
env['log']('\nI will now attempt to %s' % description)
definitions = task(definitions, output_file_name, **env)
env['log']('\nI will now attempt to remove empty sections')
try_strip_empty_sections(output_file_name, **env)
if env['max_consecutive_newlines'] >= 0 or env['strip_trailing_space']:
env['log']('\nNow, I will attempt to strip repeated newlines and trailing spaces from this file...')
try_strip_newlines(output_file_name, **env)
return True
def maybe_add_coqlib_import(contents, **env):
if env['inline_coqlib']:
contents = 'Require Coq.Init.Prelude.\nImport Coq.Init.Prelude.\n' + contents
return contents
if __name__ == '__main__':
try:
args = process_logging_arguments(parser.parse_args())
except argparse.ArgumentError as exc:
if exc.message == 'expected one argument':
exc.reraise('\nNote that argparse does not accept arguments with leading dashes.\nTry --foo=bar or --foo " -bar", if this was your intent.\nSee Python issue 9334.')
else:
exc.reraise()
def prepend_coqbin(prog):
if args.coqbin != '':
return os.path.join(args.coqbin, prog)
else:
return prog
bug_file_name = args.bug_file.name
output_file_name = args.output_file
env = {
'fast_merge_imports': args.fast_merge_imports,
'log': args.log,
'coqc': prepend_coqbin(args.coqc),
'coqtop': prepend_coqbin(args.coqtop),
'as_modules': args.wrap_modules,
'max_consecutive_newlines': args.max_consecutive_newlines,
'header': args.header,
'dynamic_header': args.dynamic_header,
'strip_trailing_space': args.strip_trailing_space,
'timeout': (args.nonpassing_timeout if args.nonpassing_timeout != -1 else args.timeout),
'passing_timeout': (args.passing_timeout if args.passing_timeout != -1 else args.timeout),
'absolutize': args.absolutize,
'minimize_before_inlining': args.minimize_before_inlining,
'save_typeclasses': args.save_typeclasses,
'admit_opaque': args.admit_opaque and args.admit_any,
'admit_obligations': args.admit_obligations and args.admit_any,
'aggressive': args.aggressive,
'admit_transparent': args.admit_transparent and args.admit_any,
'coqc_args': tuple(i.strip()
for i in (list(process_maybe_list(args.nonpassing_coqc_args, log=args.log))
+ list(process_maybe_list(args.nonpassing_coq_args, log=args.log))
+ list(process_maybe_list(args.coq_args, log=args.log)))),
'coqtop_args': tuple(i.strip()
for i in (list(process_maybe_list(args.nonpassing_coqtop_args, log=args.log))
+ list(process_maybe_list(args.coqtop_args, log=args.log))
+ list(process_maybe_list(args.nonpassing_coq_args, log=args.log))
+ list(process_maybe_list(args.coq_args, log=args.log)))),
'coq_makefile': prepend_coqbin(args.coq_makefile),
'passing_coqc_args': tuple(i.strip()
for i in (list(process_maybe_list(args.passing_coqc_args, log=args.log))
+ list(process_maybe_list(args.passing_coq_args, log=args.log))
+ list(process_maybe_list(args.coq_args, log=args.log)))),
'passing_coqtop_args': tuple(i.strip()
for i in (list(process_maybe_list(args.passing_coqtop_args, log=args.log))
+ list(process_maybe_list(args.coqtop_args, log=args.log))
+ list(process_maybe_list(args.passing_coq_args, log=args.log))
+ list(process_maybe_list(args.coq_args, log=args.log)))),
'passing_coqc' : (prepend_coqbin(args.passing_coqc)
if args.passing_coqc != ''
else (prepend_coqbin(args.coqc)
if args.passing_coqc_args is not None
else None)),
'passing_coqtop' : (prepend_coqbin(args.passing_coqtop)
if args.passing_coqtop != ''
else (prepend_coqbin(args.coqtop)
if args.passing_coqtop_args is not None
else None)),
'passing_base_dir': (os.path.abspath(args.passing_base_dir)
if args.passing_base_dir != ''
else None),
'base_dir': (os.path.abspath(args.base_dir)
if args.base_dir != ''
else None),
'walk_tree': args.walk_tree,
'strict_whitespace': args.strict_whitespace,
'temp_file_name': args.temp_file,
'coqc_is_coqtop': args.coqc_is_coqtop,
'passing_coqc_is_coqtop': args.passing_coqc_is_coqtop,
'inline_coqlib': args.inline_coqlib,
'yes': args.yes,
'color_on' : args.color_on,
'inline_failure_libnames': [],
'parse_with': args.parse_with,
}
if bug_file_name[-2:] != '.v':
env['log']('\nError: BUGGY_FILE must end in .v (value: %s)' % bug_file_name, force_stdout=True, level=LOG_ALWAYS)
sys.exit(1)
if output_file_name[-2:] != '.v':
env['log']('\nError: OUT_FILE must end in .v (value: %s)' % output_file_name, force_stdout=True, level=LOG_ALWAYS)
sys.exit(1)
if os.path.exists(output_file_name):
env['log']('\nWarning: OUT_FILE (%s) already exists. Would you like to overwrite?\n' % output_file_name, force_stdout=True, level=LOG_ALWAYS)
if not yes_no_prompt(yes=env['yes']):
sys.exit(1)
for k, arg in (('base_dir', '--base-dir'), ('passing_base_dir', '--passing-base-dir')):
if env[k] is not None and not os.path.isdir(env[k]):
env['log']('\nError: Argument to %s (%s) must exist and be a directory.' % (arg, env[k]), force_stdout=True, level=LOG_ALWAYS)
sys.exit(1)
env['remove_temp_file'] = False
if env['temp_file_name'] == '':
temp_file = tempfile.NamedTemporaryFile(suffix='.v', dir='.', delete=False)
env['temp_file_name'] = temp_file.name
temp_file.close()
env['remove_temp_file'] = True
def make_make_coqc(coqc_prog, **kwargs):
if get_coq_accepts_compile(coqc_prog): return os.path.join(SCRIPT_DIRECTORY, 'coqtop-as-coqc.sh') + ' ' + coqc_prog
if 'coqtop' in coqc_prog: return coqc_prog.replace('coqtop', 'coqc')
return 'coqc'
if env['coqc_is_coqtop']:
if env['coqc'] == 'coqc': env['coqc'] = env['coqtop']
env['make_coqc'] = make_make_coqc(env['coqc'], **env)
if env['passing_coqc_is_coqtop']:
if env['passing_coqc'] == 'coqc':
if env['passing_coqtop'] is not None: env['passing_coqc'] = env['passing_coqtop']
else: env['passing_coqc'] = env['coqtop']
env['passing_make_coqc'] = make_make_coqc(env['passing_coqc'], **env)
coqc_help = get_coqc_help(get_preferred_passing('coqc', **env), **env)
coqc_version = get_coqc_version(env['coqc'], **env)
update_env_with_libnames(env, args, include_passing=env['passing_coqc'],
use_default =not has_dir_binding(env[ 'coqc_args'], coqc_help=coqc_help, file_name=bug_file_name),
use_passing_default=not has_dir_binding(env['passing_coqc_args'], coqc_help=coqc_help, file_name=bug_file_name))
if args.inline_user_contrib:
for passing_prefix in ('', 'passing_'):
if env[passing_prefix + 'coqc']:
update_env_with_coqpath_folders(passing_prefix, env, os.path.join(get_coqc_coqlib(env[passing_prefix + 'coqc'], **env), 'user-contrib'))
env['log']('{', level=2)
for k, v in sorted(list(env.items())):
env['log'](' %s: %s' % (repr(k), repr(v)), level=2)
env['log']('}', level=2)
for passing_prefix in ('', 'passing_'):
if env[passing_prefix + 'coqc']:
args_key = passing_prefix + 'coqc_args'
if '-native-compiler' not in env[args_key]:
env[args_key] = tuple(list(env[args_key]) + list(get_coq_native_compiler_ondemand_fragment(env[passing_prefix + 'coqc'], **env)))
try:
if env['temp_file_name'][-2:] != '.v':
env['log']('\nError: TEMP_FILE must end in .v (value: %s)' % env['temp_file_name'], force_stdout=True, level=LOG_ALWAYS)
sys.exit(1)
env['log']('\nCoq version: %s\n' % coqc_version)
extra_args = get_coq_prog_args(get_file(bug_file_name, **env)) if args.use_coq_prog_args else []
for args_name, coq_prog, passing_prefix in (('coqc_args', env['coqc'], ''), ('coqtop_args', env['coqtop'], ''), ('passing_coqc_args', env['passing_coqc'] if env['passing_coqc'] else env['coqc'], 'passing_'), ('passing_coqtop_args', env['passing_coqtop'] if env['passing_coqtop'] else env['coqtop'], 'passing_')):
env[args_name] = tuple(list(env[args_name]) + list(extra_args))
for dirname, libname in env.get(passing_prefix + 'libnames', []):
env[args_name] = tuple(list(env[args_name]) + ['-R', dirname, libname])
for dirname, libname in env.get(passing_prefix + 'non_recursive_libnames', []):
env[args_name] = tuple(list(env[args_name]) + ['-Q', dirname, libname])
for dirname in env.get(passing_prefix + 'ocaml_dirnames', []):
env[args_name] = tuple(list(env[args_name]) + ['-I', dirname])
env[args_name] = deduplicate_trailing_dir_bindings(env[args_name], coqc_help=coqc_help, file_name=bug_file_name, coq_accepts_top=get_coq_accepts_top(coq_prog))
for arg in group_coq_args(extra_args, coqc_help):
for passing_prefix in ('passing_', ''):
if arg[0] == '-R': env.get(passing_prefix + 'libnames', []).append((arg[1], arg[2]))
if arg[0] == '-Q': env.get(passing_prefix + 'non_recursive_libnames', []).append((arg[1], arg[2]))
if arg[0] == '-I': env.get(passing_prefix + 'ocaml_dirnames', []).append(arg[1])
if env['minimize_before_inlining']:
env['log']('\nFirst, I will attempt to absolutize relevant [Require]s in %s, and store the result in %s...' % (bug_file_name, output_file_name))
inlined_contents = get_file(bug_file_name, update_globs=True, **env)
args.bug_file.close()
inlined_contents = maybe_add_coqlib_import(inlined_contents, **env)
inlined_contents = add_admit_tactic(inlined_contents, **env)
write_to_file(output_file_name, inlined_contents)
else:
if env['inline_coqlib']:
env['log']('\nError: --inline-coqlib is incompatible with --no-minimize-before-inlining;\nthe Coq standard library is not suited for inlining all-at-once.', force_stdout=True, level=LOG_ALWAYS)
sys.exit(1)
env['log']('\nFirst, I will attempt to inline all of the inputs in %s, and store the result in %s...' % (bug_file_name, output_file_name))
inlined_contents = include_imports(bug_file_name, **env)
args.bug_file.close()
if inlined_contents:
inlined_contents = add_admit_tactic(inlined_contents, **env)
env['log']('Stripping trailing ends')
while re.search(r'End [^ \.]*\.\s*$', inlined_contents):
inlined_contents = re.sub(r'End [^ \.]*\.\s*$', '', inlined_contents)
write_to_file(output_file_name, inlined_contents)
else:
env['log']('Failed to inline inputs.')
sys.exit(1)
if env['inline_coqlib']:
for key in ('coqc_args', 'coqtop_args', 'passing_coqc_args', 'passing_coqtop_args'):
env[key] = tuple(list(env[key]) + ['-nois', '-coqlib', env['inline_coqlib']])
env['libnames'] = tuple(list(env['libnames']) + [(os.path.join(env['inline_coqlib'], 'theories'), 'Coq')])
env['log']('\nNow, I will attempt to coq the file, and find the error...')
env['error_reg_string'] = get_error_reg_string(output_file_name, **env)
if args.error_log:
env['log']('\nNow, I will attempt to find the error message in the log...')
error_log = args.error_log.read()
args.error_log.close()
if not diagnose_error.has_error(error_log, env['error_reg_string']):
env['log']('\nMoving %s to %s...' % (output_file_name, env['temp_file_name']))
write_to_file(env['temp_file_name'], read_from_file(output_file_name))
os.remove(output_file_name)
default_on_fatal('The computed error message was not present in the given error log.', **env)
# initial run before we (potentially) do fancy things with the requires
minimize_file(output_file_name, **env)
if env['minimize_before_inlining']: # if we've not already inlined everything
# so long as we keep changing, we will pull all the
# requires to the top, then try to replace them in reverse
# order. As soon as we succeed, we reset the list
last_output = get_file(output_file_name, **env)
clear_libimport_cache(lib_of_filename(output_file_name, **env))
cur_output_gen = (lambda mod_remap: add_admit_tactic(get_file(output_file_name, mod_remap=mod_remap, **env), **env).strip() + '\n')
cur_output = cur_output_gen(dict())
# keep a list of libraries we've already tried to inline, and don't try them again
libname_blacklist = []
first_run = True
while cur_output != last_output or first_run:
first_run = False
last_output = cur_output
requires = recursively_get_requires_from_file(output_file_name, update_globs=True, **env)
for req_module in reversed(requires):
if req_module in libname_blacklist:
continue
else:
libname_blacklist.append(req_module)
rep = '\nRequire %s.\n' % req_module
if rep not in '\n' + cur_output:
env['log']('\nWarning: I cannot find Require %s.' % req_module)
env['log']('in contents:\n' + cur_output, level=3)
continue
try:
# we prefer wrapping modules via Include,
# because this is a bit more robust against
# future module inlining (see example test 45)
def get_test_output(absolutize_mods=False, first_wrap_then_include=True, without_require=True, insert_at_top=False):
test_output = cur_output if not absolutize_mods else cur_output_gen({req_module: absolutize_and_mangle_libname(req_module, first_wrap_then_include=first_wrap_then_include)})
replacement = '\n' + get_required_contents(req_module, first_wrap_then_include=first_wrap_then_include, without_require=without_require, **env).strip() + '\n'
if without_require:
all_imports = run_recursively_get_imports(req_module, **env) # like get_recursive_require_names, but with better sorting properties, I think, and also automatically strips off the self module
replacement = '\n' + ''.join('Require %s.\n' % i for i in all_imports) + replacement
if insert_at_top:
header, test_output = split_leading_comments_and_whitespace(test_output)
return add_admit_tactic((
header +
replacement + '\n' +
('\n' + test_output).replace(rep, '\n')).strip() + '\n',
**env)
else:
return ('\n' + test_output).replace(rep, replacement, 1).replace(rep, '\n').strip() + '\n'
test_output_alts = [
(((' without Include' if not first_wrap_then_include else ' via Include')
+ (', absolutizing mod references' if absolutize_mods else '')
+ (', stripping Requires' if without_require else ', with Requires')),
get_test_output(absolutize_mods=absolutize_mods, first_wrap_then_include=first_wrap_then_include, without_require=without_require, insert_at_top=insert_at_top))
for absolutize_mods in (False, True)
for first_wrap_then_include in (True, False)
for without_require, insert_at_top in ((True, False),
(False, True),
(False, False))
]
(test_output_descr, test_output), test_output_alts = test_output_alts[0], test_output_alts[1:]
except IOError as e:
env['log']('\nWarning: Cannot inline %s (%s)\nRecursively Searched: %s\nNonrecursively Searched: %s' % (req_module, str(e), str(tuple(env['libnames'])), str(tuple(env['non_recursive_libnames']))))
continue
if not check_change_and_write_to_file(
cur_output, test_output, output_file_name,
unchanged_message='Invalid empty file!', success_message=('Inlining %s%s succeeded.' % (req_module, test_output_descr)),
failure_description=('inline %s%s' % (req_module, test_output_descr)), changed_description='File',
reset_timeout=True,
timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT, # is this the right retry count?
display_source_to_error=False,
**env):
# any lazily evaluates the iterator, so we'll
# only run the check up to the point of the
# first success
if not any(check_change_and_write_to_file(
cur_output, test_output_alt, output_file_name,
unchanged_message='Invalid empty file!', success_message=('Inlining %s%s succeeded.' % (req_module, descr)),
failure_description=('inline %s%s' % (req_module, descr)), changed_description='File',
timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT, # is this the right retry count?
# reset the timeout on each different
# way of inlining, so that an earlier
# one failing doesn't hobble the
# ability of a later one to succeed
reset_timeout=True,
display_source_to_error=True,
**env)
for descr, test_output_alt in test_output_alts):
# let's also display the error and source
# for the original failure to inline,
# without the Include, so we can see
# what's going wrong in both cases
check_change_and_write_to_file(
cur_output, test_output, output_file_name,
unchanged_message='Invalid empty file!', success_message=('Inlining %s%s succeeded.' % (req_module, test_output_descr)),
failure_description=('inline %s%s' % (req_module, test_output_descr)), changed_description='File',
timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT, # is this the right retry count?
reset_timeout=True,
display_source_to_error=True,
write_to_temp_file=True,
**env)
extra_blacklist = [r for r in get_recursive_require_names(req_module, **env) if r not in libname_blacklist]
if extra_blacklist:
env['log']('\nWarning: Preemptively skipping recursive dependency module%s: %s\n'
% (('' if len(extra_blacklist) == 1 else 's'), ', '.join(extra_blacklist)))
libname_blacklist.extend(extra_blacklist)
env['inline_failure_libnames'].append(req_module)
continue
if minimize_file(output_file_name, die=(lambda *args, **kargs: False), **env):
break
clear_libimport_cache(lib_of_filename(output_file_name, libnames=tuple(env['libnames']), non_recursive_libnames=tuple(env['non_recursive_libnames'])))
cur_output = cur_output_gen(dict())
# and we make one final run, or, in case there are no requires, one run
minimize_file(output_file_name, **env)
except EOFError:
env['log'](traceback.format_exc(), level=LOG_ALWAYS)
raise
except Exception:
if hasattr(traceback, 'TracebackException'):
etype, value, tb = sys.exc_info()
env['log'](''.join(traceback.TracebackException(type(value), value, tb, capture_locals=True).format()), level=LOG_ALWAYS)
else:
env['log'](traceback.format_exc(), level=LOG_ALWAYS)
raise
finally:
if env['remove_temp_file']:
clean_v_file(env['temp_file_name'])
