Display the source of the error-producing file

At least when the issue is that inlining a module failed.

Also add a test case involving the example of #41

diagnose_error.py

@@ -7,11 +7,13 @@
 from custom_arguments import DEFAULT_LOG
 import util
 
-__all__ = ["has_error", "get_error_line_number", "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"]
 
 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)'
+DEFAULT_PRE_ERROR_REG_STRING_WITH_BYTES = 'File "[^"]+", line ([0-9]+), characters ([0-9]+)-([0-9]+):\n(?!Warning)'
 DEFAULT_ERROR_REG_STRING = DEFAULT_PRE_ERROR_REG_STRING + '((?:.|\n)+)'
+DEFAULT_ERROR_REG_STRING_WITH_BYTES = DEFAULT_PRE_ERROR_REG_STRING_WITH_BYTES + '((?:.|\n)+)'
 DEFAULT_ERROR_REG_STRING_GENERIC = DEFAULT_PRE_PRE_ERROR_REG_STRING + '(%s)'
 
 def clean_output(output):
@@ -48,6 +50,16 @@ def get_error_line_number(output, reg_string=DEFAULT_ERROR_REG_STRING, pre_reg_s
     errors = get_error_match(output, reg_string=reg_string, pre_reg_string=pre_reg_string)
     return int(errors.groups()[0])
 
+@memoize
+def get_error_byte_locations(output, reg_string=DEFAULT_ERROR_REG_STRING_WITH_BYTES, pre_reg_string=DEFAULT_PRE_ERROR_REG_STRING_WITH_BYTES):
+    """Returns the byte locations that the error matching reg_string
+    occured on.
+
+    Precondition: has_error(output, reg_string)
+    """
+    errors = get_error_match(output, reg_string=reg_string, pre_reg_string=pre_reg_string)
+    return (int(errors.groups()[1]), int(errors.groups()[2]))
+
 @memoize
 def get_error_string(output, reg_string=DEFAULT_ERROR_REG_STRING, pre_reg_string=DEFAULT_PRE_ERROR_REG_STRING):
     """Returns the error string of the error matching reg_string.

examples/Makefile

@@ -5,7 +5,7 @@ CAT_ALL_LOGS=0
 
 ####
 
-DEFAULT_TESTS = 00 01 02 03 04 05 07 08 08-2 09 11 12 14 15 16 17 19 21 22 23 24 25 28 29 30 31 32 33 34 35 36 37 38 39 40 41
+DEFAULT_TESTS = 00 01 02 03 04 05 07 08 08-2 09 11 12 14 15 16 17 19 21 22 23 24 25 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
 CONDITIONAL_TESTS = 06 08-3 10 13 18 20 26 27
 
 ONLY_IF_COQTOP_COMPILE_TESTS = 08-3

examples/example_42/A.v

@@ -0,0 +1 @@
+Axiom a : Set.

examples/example_42/B.v

@@ -0,0 +1,9 @@
+Definition foo : 1 = 2 -> forall P, ~~P -> P.
+Proof.
+  intros.
+  try tauto. (* no-op, unless Classical_Prop has been Required *)
+  congruence.
+Defined.
+
+Require Import Foo.A.
+Require Import Foo.C.

examples/example_42/C.v

@@ -0,0 +1,4 @@
+Require Import Coq.Logic.Classical_Prop.
+
+Lemma npp : forall P, ~~P -> P.
+Proof. tauto. Qed.

examples/example_42/example_42.v

@@ -0,0 +1,5 @@
+Require Import Foo.B Foo.C.
+
+Definition bar := Eval unfold foo in foo.
+
+Check (bar, npp, Foo.A.a) : Set.

examples/run-example-42.sh

@@ -0,0 +1,117 @@
+#!/bin/bash
+###################################################################
+## This is a template file for new examples.  It explains how to ##
+## check for various things.                                     ##
+##                                                               ##
+## An example script should exit with code 0 if the test passes, ##
+## and with some other code if the test fails.                   ##
+###################################################################
+
+##########################################################
+# Various options that must be updated for each example
+N="42"
+EXAMPLE_DIRECTORY="example_$N"
+EXAMPLE_INPUT="example_$N.v"
+EXAMPLE_OUTPUT="bug_$N.v"
+EXTRA_ARGS=(-R . Foo --no-admit-transparent --no-admit-opaque "$@")
+##########################################################
+
+# Get the directory name of this script, and `cd` to that directory
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+cd "$DIR/$EXAMPLE_DIRECTORY"
+FIND_BUG_PY="$(cd "$DIR/.." && pwd)/find-bug.py"
+
+# Initialize common settings like the version of python
+. "$DIR/init-settings.sh"
+
+ABS_PATH="$(${PYTHON} -c 'import os.path; print(os.path.abspath("."))')"
+
+# Set up bash to be verbose about displaying the commands run
+PS4='$ '
+set -x
+
+# Disable parallel make in subcalls to the bug minimizer because it screws with things
+. "$DIR/disable-parallel-make.sh"
+
+######################################################################
+# Create the output file (to normalize the number of "yes"es needed),
+# and run the script only up to the request for the regular
+# expression; then test that the output is as expected.
+#
+# If you don't need to test the output of the initial requests, feel
+# free to remove this section.
+#
+# Note that the -top argument only appears in Coq >= 8.4
+#
+# Note also that the line numbers tend to be one larger in old
+# versions of Coq (<= 8.6?)
+EXPECTED_ERROR=$(cat <<EOF
+This file produces the following output when Coq'ed:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(8\|9\), characters 6-25:
+Error:
+The term "(bar, npp, A\.a)" has type
+ "((1 = 2 -> forall P : Prop, ~ ~ P -> P) \* (forall P : Prop, ~ ~ P -> P) \*
+   Set)%type" while it is expected to have type "Set"\.
+EOF
+)
+# pre-build the files to normalize the output for the run we're testing
+rm -f *.vo *.glob
+echo "y" | ${PYTHON} "$FIND_BUG_PY" "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" "${EXTRA_ARGS[@]}" 2>/dev/null >/dev/null
+# kludge: create the .glob file so we don't run the makefile
+touch "${EXAMPLE_OUTPUT%%.v}.glob"
+ACTUAL_PRE="$((echo "y"; echo "y") | ${PYTHON} "$FIND_BUG_PY" "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" "${EXTRA_ARGS[@]}" -l - 2>&1)"
+ACTUAL_PRE_ONE_LINE="$(echo "$ACTUAL_PRE" | tr '\n' '\1')"
+TEST_FOR="$(echo "$EXPECTED_ERROR" | tr '\n' '\1')"
+if [ "$(echo "$ACTUAL_PRE_ONE_LINE" | grep -c "$TEST_FOR")" -lt 1 ]
+then
+    echo "Expected a string matching:"
+    echo "$EXPECTED_ERROR"
+    echo
+    echo
+    echo
+    echo "Actual:"
+    echo "$ACTUAL_PRE"
+    ${PYTHON} "$DIR/prefix-grep.py" "$ACTUAL_PRE_ONE_LINE" "$TEST_FOR"
+    exit 1
+fi
+#########################################################################################################
+
+
+#####################################################################
+# Run the bug minimizer on this example; error if it fails to run
+# correctly.  Make sure you update the arguments, etc.
+${PYTHON} "$FIND_BUG_PY" "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" "${EXTRA_ARGS[@]}" || exit $?
+
+######################################################################
+# Put some segment that you expect to see in the file here.  Or count
+# the number of lines.  Or make some other test.  Or remove this block
+# entirely if you don't care about the minimized file.
+EXPECTED=$(cat <<EOF
+(\* -\*- mode: coq; coq-prog-args: ("-emacs"\( "-w" "-deprecated-native-compiler-option"\)\? "-R" "\." "Foo"\( "-top" "example_[0-9]\+"\)\?\( "-native-compiler" "ondemand"\)\?) -\*- \*)
+(\* File reduced by coq-bug-finder from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
+(\* coqc version [^\*]*\*)
+
+Require Foo\.B\.
+Import Foo\.B\.
+Import Foo\.C\.
+
+Definition bar := Eval unfold foo in foo\.
+
+Check (bar, npp, Foo\.A\.a) : Set\.
+
+EOF
+)
+
+EXPECTED_ONE_LINE="$(echo "$EXPECTED" | grep -v '^$' | tr '\n' '\1')"
+ACTUAL="$(cat "$EXAMPLE_OUTPUT" | grep -v '^$' | tr '\n' '\1')"
+LINES="$(echo "$ACTUAL" | grep -c "$EXPECTED_ONE_LINE")"
+if [ "$LINES" -ne 1 ]
+then
+    echo "Expected a string matching:"
+    echo "$EXPECTED"
+    echo "Got:"
+    cat "$EXAMPLE_OUTPUT" | grep -v '^$'
+    ${PYTHON} "$DIR/prefix-grep.py" "$ACTUAL" "$EXPECTED_ONE_LINE"
+    exit 1
+fi
+exit 0

find-bug.py

@@ -384,7 +384,7 @@ 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,
+                                   verbose_base=1, display_source_to_error=False,
                                    **kwargs):
     if kwargs['verbose'] >= 2 + verbose_base:
         kwargs['log']('Running coq on the file\n"""\n%s\n"""' % new_contents)
@@ -414,6 +414,14 @@ def check_change_and_write_to_file(old_contents, new_contents, output_file_name,
                                                   timeout_retry_count=timeout_retry_count-1, ignore_coq_output_cache=True,
                                                   verbose_base=verbose_base,
                                                   **kwargs)
+        elif kwargs['verbose'] >= verbose_base and 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:')
+            kwargs['log']('%s\n%s\n' % (new_contents_to_error,
+                                        new_contents_rest.encode('utf-8')[:new_end].decode('utf-8')))
         return False
     else:
         kwargs['log']('ERROR: Unrecognized change result %s on\nclassify_contents_change(\n  %s\n ,%s\n)\n%s'
@@ -1364,6 +1372,7 @@ def prepend_coqbin(prog):
                             unchanged_message='Invalid empty file!', success_message=('Inlining %s succeeded.' % req_module),
                             failure_description=('inline %s' % req_module), changed_description='File',
                             timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT, # is this the right retry count?
+                            display_source_to_error=True,
                             **env):
                         extra_blacklist = [r for r in get_recursive_require_names(req_module, **env) if r not in libname_blacklist]
                         if extra_blacklist and env['verbose'] >= 1: