Skip to content

Commit

Permalink
Passing coqc timeout should not be considered success
Browse files Browse the repository at this point in the history
Oops.  Should deal with coq/coq#14746 (comment)
  • Loading branch information
JasonGross committed Oct 27, 2021
1 parent 4b98560 commit ed441c2
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 3 deletions.
11 changes: 9 additions & 2 deletions diagnose_error.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
from custom_arguments import DEFAULT_LOG
import util

__all__ = ["has_error", "get_error_line_number", "get_error_byte_locations", "make_reg_string", "get_coq_output", "get_coq_output_iterable", "get_error_string", "get_timeout", "reset_timeout", "reset_coq_output_cache"]
__all__ = ["has_error", "get_error_line_number", "get_error_byte_locations", "make_reg_string", "get_coq_output", "get_coq_output_iterable", "get_error_string", "get_timeout", "reset_timeout", "reset_coq_output_cache", "is_timeout"]

DEFAULT_PRE_PRE_ERROR_REG_STRING = 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n'
DEFAULT_PRE_ERROR_REG_STRING = 'File "[^"]+", line ([0-9]+), characters [0-9-]+:\n(?!Warning)'
Expand Down Expand Up @@ -54,6 +54,13 @@ def has_error(output, reg_string=DEFAULT_ERROR_REG_STRING, pre_reg_string=DEFAUL
else:
return False

TIMEOUT_POSTFIX = '\nTimeout!'

@memoize
def is_timeout(output):
"""Returns True if the output was killed with a timeout, False otherwise"""
return output.endswith(TIMEOUT_POSTFIX)

@memoize
def get_error_line_number(output, reg_string=DEFAULT_ERROR_REG_STRING, pre_reg_string=DEFAULT_PRE_ERROR_REG_STRING):
"""Returns the line number that the error matching reg_string
Expand Down Expand Up @@ -156,7 +163,7 @@ def target():

p.terminate()
thread.join()
return (tuple(map((lambda s: (s if s else '') + '\nTimeout!'), ret['value'])), ret['returncode'])
return (tuple(map((lambda s: (s if s else '') + TIMEOUT_POSTFIX), ret['value'])), ret['returncode'])


def memory_robust_timeout_Popen_communicate(log, *args, **kwargs):
Expand Down
2 changes: 1 addition & 1 deletion find-bug.py
Original file line number Diff line number Diff line change
Expand Up @@ -372,7 +372,7 @@ def get_padded_contents(): return prepend_header(new_contents, **kwargs)
if diagnose_error.has_error(output, kwargs['error_reg_string']):
if kwargs['passing_coqc']:
passing_output, cmds, passing_retcode, passing_runtime = diagnose_error.get_coq_output(kwargs['passing_coqc'], kwargs['passing_coqc_args'], new_contents, kwargs['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):
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
Expand Down

0 comments on commit ed441c2

Please sign in to comment.