Run normalize_requires inside minimize_file

coq_version.py

@@ -5,7 +5,7 @@
 from memoize import memoize
 import util
 
-__all__ = ["get_coqc_version", "get_coqtop_version", "get_coqc_help", "get_coqc_coqlib", "get_coq_accepts_top", "get_coq_accepts_time", "get_coq_accepts_o", "get_coq_native_compiler_ondemand_fragment", "group_coq_args_split_recognized", "group_coq_args", "coq_makefile_supports_arg", "get_proof_term_works_with_time", "get_ltac_support_snippet"]
+__all__ = ["get_coqc_version", "get_coqtop_version", "get_coqc_help", "get_coqc_coqlib", "get_coq_accepts_top", "get_coq_accepts_time", "get_coq_accepts_o", "get_coq_accepts_compile", "get_coq_native_compiler_ondemand_fragment", "group_coq_args_split_recognized", "group_coq_args", "coq_makefile_supports_arg", "get_proof_term_works_with_time", "get_ltac_support_snippet"]
 
 @memoize
 def get_coqc_version_helper(coqc):
@@ -73,6 +73,9 @@ def get_coq_accepts_time(coqc_prog, **kwargs):
 def get_coq_accepts_w(coqc_prog, **kwargs):
     return get_coq_accepts_option(coqc_prog, '-w', **kwargs)
 
+def get_coq_accepts_compile(coqc_prog, **kwargs):
+    return get_coq_accepts_option(coqc_prog, '-compile', **kwargs)
+
 @memoize
 def get_coqc_native_compiler_ondemand_errors(coqc):
     temp_file = tempfile.NamedTemporaryFile(suffix='.v', dir='.', delete=True)

examples/Makefile

@@ -23,6 +23,7 @@ ONLY_IF_Q_LOGS = $(patsubst %,example_%_result.log,$(ONLY_IF_Q_TESTS))
 ONLY_IF_FROM_LOGS = $(patsubst %,example_%_result.log,$(ONLY_IF_FROM_TESTS))
 
 .DEFAULT_GOAL := test-suite
+.SECONDEXPANSION:
 
 # Order the builds for 8 so they don't run in parallel
 example_08-2_result.log: | example_08_result.log
@@ -135,7 +136,7 @@ print-support::
 	@printf "coqc is < 8.12:\t\t\tYes\n"
 endif
 
-$(DEFAULT_LOGS) $(CONDITIONAL_LOGS) : example_%_result.log : $(wildcard example_%/*.v run-example-%.sh) Makefile
+$(DEFAULT_LOGS) $(CONDITIONAL_LOGS) : example_%_result.log : $$(wildcard example_%/example_%.v) run-example-%.sh
 	$(VECHO) "TEST run-example-$*.sh..." >&2
 	$(Q)yes "y" 2>/dev/null | ./run-example-$*.sh >"example_$*_make.log" 2>&1; RV=$$?; (echo "$$RV" > "$@")
 	$(Q)RV="$$(cat "$@")"; if [ "$$RV" -eq 0 ]; then RESULT="$(GREEN)success!$(NC)"; else RESULT="$(RED)failure$(NC)"; fi; \

examples/prefix-grep.py

@@ -102,6 +102,6 @@ def check_grep(search_for):
         p.stdin.close()
         p.wait()
         print("Mismatch: good prefix search:\n%s" % search_for)
-        print("Mismatch: bad next characters at %d: %s" % (len(search_for), repr(sys.argv[2][len(search_for):][:10])))
-        print("Mismatch: expected next characters at %d: %s" % (len(stdout)-1, repr(sys.argv[1][len(stdout)-1:][:10])))
+        print("Mismatch: expected next characters at %d: %s" % (len(search_for), repr(sys.argv[2][len(search_for):][:10])))
+        print("Mismatch: actual next characters at %d: %s" % (len(stdout)-1, repr(sys.argv[1][len(stdout)-1:][:10])))
     #sys.exit(p.errorcode)

examples/run-example-00.sh

@@ -49,8 +49,7 @@ EXPECTED_ERROR=$(cat <<EOF
 getting example_[0-9]\+\.v (${ABS_PATH}/example_[0-9]\+\.v)
 getting example_[0-9]\+\.glob (${ABS_PATH}/example_[0-9]\+\.glob)
 
-First, I will attempt to factor out all of the \[Require\]s example_[0-9]\+\.v, and store the result in bug_[0-9]\+\.v\.\.\.
-getting example_[0-9]\+\.glob (${ABS_PATH}/example_[0-9]\+\.glob)
+First, I will attempt to absolutize relevant \[Require\]s in example_[0-9]\+\.v, and store the result in bug_[0-9]\+\.v\.\.\.
 
 Now, I will attempt to coq the file, and find the error\.\.\.
 
@@ -63,7 +62,7 @@ The timeout for coqc has been set to: 3
 This file produces the following output when Coq'ed:
 Set
      : Type
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(1\|2\), characters 0-15:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(0\|1\), characters 0-15:
 Error: The command has not failed\s\?!
 
 .\?Does this output display the correct error? \[(y)es/(n)o\]\s

examples/run-example-28.sh

@@ -42,7 +42,7 @@ set -x
 # Note that the -top argument only appears in Coq >= 8.4
 EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[45], characters 6-7:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 6-7:
 Error: The term "x" has type "Set" while it is expected to have type "nat"\.
 EOF
 )

examples/run-example-30.sh

@@ -37,7 +37,7 @@ EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
 Set
      : Type
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(1\|2\), characters 0-15:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 0-15:
 Error: The command has not failed\s\?!
 
 .\?Does this output display the correct error? \[(y)es/(n)o\]\s

examples/run-example-31.sh

@@ -35,7 +35,7 @@ set -x
 # Note that the -top argument only appears in Coq >= 8.4
 EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(3\|4\), characters 6-13:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(2\|3\), characters 6-13:
 Error:
 EOF
 )

examples/run-example-35.sh

@@ -42,7 +42,7 @@ set -x
 # Note that the -top argument only appears in Coq >= 8.4
 EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(3\|4\), characters 6-9:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 6-9:
 Error: The reference foo was not found in the current environment\.
 
 .\?Does this output display the correct error? \[(y)es/(n)o\]\s

examples/run-example-36.sh

@@ -35,7 +35,7 @@ set -x
 # Note that the -top argument only appears in Coq >= 8.4
 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 47-49:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(7\|8\), characters 47-49:
 Error:
 The term.*
 EOF

examples/run-example-37.sh

@@ -50,7 +50,7 @@ EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
 Set
      : Type
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(6\|7\), characters 0-15:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 0-15:
 Error: The command has not failed\s\?!
 
 .\?Does this output display the correct error? \[(y)es/(n)o\]\s

examples/run-example-38.sh

@@ -45,7 +45,7 @@ set -x
 # 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\(0\|1\), characters 10-14:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line \(9\|10\), characters 10-14:
 Error: The reference True was not found in the current environment\.
 EOF
 )

examples/run-example-39.sh

@@ -44,7 +44,7 @@ set -x
 # Note also that the line numbers tend to be one larger in old
 # versions of Coq (<= 8.6?)
 EXPECTED_ERROR=$(cat <<EOF
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(8\|9\), characters 6-9:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 6-9:
 Error:
 The term "bar" has type "False -> False" while it is expected to have type
  "True".

examples/run-example-40.sh

@@ -49,7 +49,7 @@ EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
 Set
      : Type
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(6\|7\), characters 0-15:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 0-15:
 Error: The command has not failed\s\?!
 EOF
 )

examples/run-example-41.sh

@@ -50,7 +50,7 @@ EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
 foo
      : Type
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(3\|4\), characters 0-15:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 0-15:
 Error: The command has not failed\s\?!
 EOF
 )

examples/run-example-42.sh

@@ -47,7 +47,7 @@ set -x
 # 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 2\(2\|3\), characters 6-25:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-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) \*
@@ -88,11 +88,21 @@ ${PYTHON} "$FIND_BUG_PY" "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" "${EXTRA_ARGS[@]}" |
 # 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 \*)
+(\* 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 B\.
+Definition foo : 1 = 2 -> forall P, ~~P -> P\.
+Proof\.
+  intros\.
+  try tauto\.
 
-Require Foo\.B\.
-Import Foo\.B\.
+  congruence\.
+Defined\.
+
+Require Import Foo\.A\.
+Require Import Foo\.C\.
+
+End B\.
 Import Foo\.C\.
 
 Definition bar := Eval unfold foo in foo\.

examples/run-example-43.sh

@@ -43,7 +43,7 @@ set -x
 # 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\(1\|2\), characters 2-61:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 2-61:
 Error: Tactic failure: Universe {TestSuite.issues.issue7.110} is unbound\.
 
 .\?Does this output display the correct error? \[(y)es/(n)o\]\s

examples/run-example-44.sh

@@ -46,7 +46,7 @@ set -x
 # Note also that the line numbers tend to be one larger in old
 # versions of Coq (<= 8.6?)
 EXPECTED_ERROR=$(cat <<EOF
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(3\|4\), characters 7-10:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 7-10:
 Error: The term "6" has type "nat" while it is expected to have type "Set".
 EOF
 )

examples/run-example-45.sh

@@ -49,7 +49,7 @@ EXPECTED_ERROR=$(cat <<EOF
 This file produces the following output when Coq'ed:
 b
      : A.SET
-File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1\(3\|4\), characters 0-21:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 0-21:
 Error: The command has not failed.*
 EOF
 )

examples/run-example-48.sh

@@ -47,7 +47,7 @@ set -x
 # 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 2\(0\|1\), characters 72-73:
+File "/tmp/tmp[A-Za-z0-9_]\+\.v", line 1[0-9], characters 72-73:
 Error:
 In environment
 f := fun _ : bar => eq_refl : forall _ : bar, eq Foo\.foo Set
@@ -92,8 +92,8 @@ EXPECTED=$(cat <<EOF
 (\* -\*- mode: coq; coq-prog-args: ("-emacs"\( "-w" "-deprecated-native-compiler-option"\)\? "-noinit" "-R" "\." "Top"\( "-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 [^\*]*\*)
+Require Coq\.Init\.Ltac\.
 
-Declare ML Module "ltac_plugin"\.
 Inductive False : Prop := \.
 Axiom proof_admitted : False\.
 Tactic Notation "admit" := abstract case proof_admitted\.
@@ -102,7 +102,6 @@ Global Set Universe Polymorphism\.
 Definition foo@{i} := Type@{i}\.
 
 End Foo\.
-Require Coq\.Init\.Ltac\.
 Import Coq\.Init\.Ltac\.
 Monomorphic Inductive eq {A} (x : A) : forall _ : A, Prop := eq_refl : eq x x\.
 Arguments eq_refl {A x} , \[A\] x\.