JasonGross · JasonGross · Oct 9, 2021 · Oct 9, 2021
diff --git a/examples/Makefile b/examples/Makefile
@@ -6,7 +6,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 42 43 44 45
-CONDITIONAL_TESTS = 06 08-3 10 13 18 20 26 27
+CONDITIONAL_TESTS = 06 08-3 10 13 18 20 26 27 46
 
 ONLY_IF_COQTOP_COMPILE_TESTS = 08-3
 ONLY_IF_Q_TESTS = 10 26
@@ -53,10 +53,10 @@ GREEN=\033[0;32m
 BOLD=$(shell tput bold)
 NORMAL=$(shell tput sgr0)
 
-COQC_VERSION=$(subst version ,,$(shell coqc --version 2>&1 | grep -o 'version [^ ]*'))
-COQC_SUPPORTS_Q=$(shell coqc --help 2>&1 | grep -c -- -Q)
-COQTOP_SUPPORTS_COMPILE=$(shell coqtop --help 2>&1 | tr '\n' '~' | sed s'/Deprecated options.*//g' | tr '~' '\n' | grep -c -- '\s-compile\s')
-COQC_SUPPORTS_FROM=$(shell echo "From Coq.Init Require Import Notations." | coqtop 2>&1 | grep -c 'Error')
+COQC_VERSION:=$(subst version ,,$(shell coqc --version 2>&1 | grep -o 'version [^ ]*'))
+COQC_SUPPORTS_Q:=$(shell coqc --help 2>&1 | grep -c -- -Q)
+COQTOP_SUPPORTS_COMPILE:=$(shell coqtop --help 2>&1 | tr '\n' '~' | sed s'/Deprecated options.*//g' | tr '~' '\n' | grep -c -- '\s-compile\s')
+COQC_SUPPORTS_FROM:=$(shell echo "From Coq.Init Require Import Notations." | coqtop 2>&1 | grep -c 'Error')
 
 .PHONY: check
 check::
@@ -117,6 +117,15 @@ print-support::
 	@printf "coqc is 8.3 or 8.4:\t\t\tYes\n"
 endif
 
+ifeq (,$(strip $(filter 8.3% 8.4% 8.5% 8.6% 8.7% 8.8% 8.9% 8.10% 8.11% 8.12% 8.13% 8.14%,$(COQC_VERSION))))
+test-suite: example_46_result.log
+print-support::
+	@printf "coqc is < 8.15:\t\t\tNo\n"
+else
+print-support::
+	@printf "coqc is < 8.15:\t\t\tYes\n"
+endif
+
 $(DEFAULT_LOGS) $(CONDITIONAL_LOGS) : example_%_result.log : $(wildcard example_%/*.v run-example-%.sh) Makefile
 	$(VECHO) "TEST run-example-$*.sh..." >&2
 	$(Q)yes "y" 2>/dev/null | ./run-example-$*.sh >"example_$*_make.log" 2>&1; RV=$$?; (echo "$$RV" > "$@")

diff --git a/examples/example_46/Foo.v b/examples/example_46/Foo.v
@@ -0,0 +1 @@
+Axiom A : Set.
diff --git a/examples/example_46/example_46.v b/examples/example_46/example_46.v
@@ -0,0 +1,15 @@
+Require Foo.Foo.
+
+Module Export Top_DOT_Foo_DOT_Foo_DOT_Baz.
+  Module Export Foo.
+    Module Export Foo.
+      Module Baz.
+        Axiom B : Set.
+      End Baz.
+    End Foo.
+  End Foo.
+End Top_DOT_Foo_DOT_Foo_DOT_Baz.
+
+Import Foo.Foo.
+
+Fail Check A -> Foo.Foo.Baz.B.
diff --git a/examples/run-example-12.sh b/examples/run-example-12.sh
@@ -49,6 +49,7 @@ cannot be applied to the term
  "Set" : "Type"
 .\?'\.
 The corresponding regular expression is 'File "\[^"\]+", line (\[0-9\]+), characters \[0-9-\]+:\\\\n(Error:\\\\s+Illegal\\\\s+application\\\\s+\\\\(Non\\\\-functional\\\\s+construction\\\\):\\\\s+The\\\\s+expression\\\\s+"Set"\\\\s+of\\\\s+type\\\\s+"Type"\\\\scannot\\\\s+be\\\\s+applied\\\\s+to\\\\s+the\\\\s+term\\\\s+"Set"\\\\s+:\\\\s+"Type")'\.
+
 \?Is this correct? \[(y)es/(n)o\] Traceback (most recent call last):
   File "\.\./\.\./find-bug\.py", line [0-9]\+, in <module>
     env\['error_reg_string'\] = get_error_reg_string(output_file_name, \*\*env)

diff --git a/examples/run-example-46.sh b/examples/run-example-46.sh
@@ -0,0 +1,122 @@
+#!/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="46"
+EXAMPLE_DIRECTORY="example_$N"
+EXAMPLE_INPUT="example_$N.v"
+EXAMPLE_OUTPUT="bug_$N.v"
+EXTRA_ARGS=("--arg=-w" "--arg=-masking-absolute-name" "-R" "." "Foo" "$@")
+##########################################################
+
+# 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:
+A -> Baz.B
+     : Set
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 23, characters 0-30:
+Error: The command has not failed\s\?!
+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" "-masking-absolute-name"\( "-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, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*)
+(\* coqc version [^\*]*\*)
+
+Module Export Foo_DOT_Foo_WRAPPED\.
+Module Export Foo\.
+Axiom A : Set\.
+
+End Foo\.
+
+End Foo_DOT_Foo_WRAPPED\.
+Module Export Foo\.
+    Module Export Foo\.
+      Module Export Baz\.
+        Axiom B : Set\.
+
+Fail Check A -> Foo\.Foo\.Baz\.B\.
+
+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
diff --git a/find-bug.py b/find-bug.py
@@ -3,7 +3,7 @@
 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
+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
 from strip_comments import strip_comments
 from strip_newlines import strip_newlines
@@ -198,7 +198,7 @@ def get_error_reg_string_of_output(output, **kwargs):
     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'." % (error_string, error_reg_string.replace('\\\n', '\\n').replace('\n', '\\n')), force_stdout=True)
+        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)
         result = ''
         while result not in ('y', 'n', 'yes', 'no'):
             result = ask('Is this correct? [(y)es/(n)o] ', **kwargs).lower().strip()
@@ -1223,7 +1223,7 @@ def prepend_coqbin(prog):
         env['log']('\nError: OUT_FILE must end in .v (value: %s)' % output_file_name, force_stdout=True)
         sys.exit(1)
     if os.path.exists(output_file_name):
-        env['log']('\nWarning: OUT_FILE (%s) already exists.  Would you like to overwrite?' % output_file_name, force_stdout=True)
+        env['log']('\nWarning: OUT_FILE (%s) already exists.  Would you like to overwrite?\n' % output_file_name, force_stdout=True)
         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')):
@@ -1340,7 +1340,8 @@ def prepend_coqbin(prog):
             # 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, libnames=tuple(env['libnames']), non_recursive_libnames=tuple(env['non_recursive_libnames'])))
-            cur_output = add_admit_tactic(normalize_requires(output_file_name, **env), **env).strip() + '\n'
+            cur_output_gen = (lambda mod_remap: add_admit_tactic(normalize_requires(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
@@ -1363,8 +1364,15 @@ def prepend_coqbin(prog):
                         # we prefer wrapping modules via Include,
                         # because this is a bit more robust against
                         # future module inlining (see example test 45)
-                        test_output = ('\n' + cur_output).replace(rep, '\n' + get_required_contents(req_module, first_wrap_then_include=True, **env).strip() + '\n').strip() + '\n'
-                        test_output_alt = ('\n' + cur_output).replace(rep, '\n' + get_required_contents(req_module, **env).strip() + '\n').strip() + '\n'
+                        def get_test_output(absolutize_mods=False, first_wrap_then_include=True):
+                            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)})
+                            return ('\n' + test_output).replace(rep, '\n' + get_required_contents(req_module, first_wrap_then_include=first_wrap_then_include, **env).strip() + '\n').strip() + '\n'
+                        test_output = get_test_output(absolutize_mods=False, first_wrap_then_include=True)
+                        test_output_alts = [
+                            (' without Include', get_test_output(absolutize_mods=False, first_wrap_then_include=False)),
+                            (' via Include, absolutizing mod references', get_test_output(absolutize_mods=True, first_wrap_then_include=True)),
+                            (' without Include, absolutizing mod references', get_test_output(absolutize_mods=True, first_wrap_then_include=False))
+                        ]
                     except IOError as e:
                         if env['verbose'] >= 1: 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
@@ -1378,13 +1386,17 @@ def prepend_coqbin(prog):
                             timeout_retry_count=SENSITIVE_TIMEOUT_RETRY_COUNT, # is this the right retry count?
                             display_source_to_error=False,
                             **env):
-                        if not check_change_and_write_to_file(
+                        # 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 succeeded.' % req_module),
-                                failure_description=('inline %s' % req_module), changed_description='File',
+                                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?
                                 display_source_to_error=True,
-                                **env):
+                                **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
@@ -1408,7 +1420,8 @@ def prepend_coqbin(prog):
                         break
 
                 clear_libimport_cache(lib_of_filename(output_file_name, libnames=tuple(env['libnames']), non_recursive_libnames=tuple(env['non_recursive_libnames'])))
-                cur_output = add_admit_tactic(normalize_requires(output_file_name, update_globs=True, **env), **env).strip() + '\n'
+                cur_output_gen = (lambda mod_remap: add_admit_tactic(normalize_requires(output_file_name, update_globs=True, mod_remap=mod_remap, **env), **env).strip() + '\n')
+                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)