From 5e3244f3ca1d4382d259c43ca0f557001267fd9c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 8 Oct 2018 13:43:35 +0000 Subject: [test-suite] ensure file names are valid module names --- test-suite/bugs/closed/8553.v | 7 ------- test-suite/bugs/closed/8672.v | 5 ----- test-suite/bugs/closed/bug_8553.v | 7 +++++++ test-suite/bugs/closed/bug_8672.v | 5 +++++ 4 files changed, 12 insertions(+), 12 deletions(-) delete mode 100644 test-suite/bugs/closed/8553.v delete mode 100644 test-suite/bugs/closed/8672.v create mode 100644 test-suite/bugs/closed/bug_8553.v create mode 100644 test-suite/bugs/closed/bug_8672.v diff --git a/test-suite/bugs/closed/8553.v b/test-suite/bugs/closed/8553.v deleted file mode 100644 index 4a1afabe89..0000000000 --- a/test-suite/bugs/closed/8553.v +++ /dev/null @@ -1,7 +0,0 @@ -(* Using tactic "change" under binders *) - -Definition add2 n := n +2. -Goal (fun n => n) = (fun n => n+2). -change (?n + 2) with (add2 n). -match goal with |- _ = (fun n => add2 n) => idtac end. (* To test the presence of add2 *) -Abort. diff --git a/test-suite/bugs/closed/8672.v b/test-suite/bugs/closed/8672.v deleted file mode 100644 index 66cd6dfa8c..0000000000 --- a/test-suite/bugs/closed/8672.v +++ /dev/null @@ -1,5 +0,0 @@ -(* Was generating a dangling "pat" variable at some time *) - -Notation "'plet' x := e 'in' t" := - ((fun H => let x := id H in t) e) (at level 0, x pattern). -Definition bla := plet (pair x y) := pair 1 2 in x. diff --git a/test-suite/bugs/closed/bug_8553.v b/test-suite/bugs/closed/bug_8553.v new file mode 100644 index 0000000000..4a1afabe89 --- /dev/null +++ b/test-suite/bugs/closed/bug_8553.v @@ -0,0 +1,7 @@ +(* Using tactic "change" under binders *) + +Definition add2 n := n +2. +Goal (fun n => n) = (fun n => n+2). +change (?n + 2) with (add2 n). +match goal with |- _ = (fun n => add2 n) => idtac end. (* To test the presence of add2 *) +Abort. diff --git a/test-suite/bugs/closed/bug_8672.v b/test-suite/bugs/closed/bug_8672.v new file mode 100644 index 0000000000..66cd6dfa8c --- /dev/null +++ b/test-suite/bugs/closed/bug_8672.v @@ -0,0 +1,5 @@ +(* Was generating a dangling "pat" variable at some time *) + +Notation "'plet' x := e 'in' t" := + ((fun H => let x := id H in t) e) (at level 0, x pattern). +Definition bla := plet (pair x y) := pair 1 2 in x. -- cgit v1.2.3 From 77a8c7667c9a5186f6ed24bbab766f50de058129 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 4 Oct 2018 10:20:37 +0000 Subject: [test-suite] compile (rather than load) test cases --- test-suite/Makefile | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index e35393b5e8..759cd99048 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -43,7 +43,7 @@ coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte -coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source +coqtopload := $(coqtop) -async-proofs-cache force -load-vernac-source coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) @@ -213,7 +213,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...still active"; \ @@ -235,7 +235,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -309,7 +309,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ echo $(call log_intro,$<); \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -341,7 +341,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -482,7 +482,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_success); \ echo " $<...still wished"; \ -- cgit v1.2.3 From 54b4c6e3f916f3913920bbd7a778f477543f0afb Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 9 Oct 2018 12:47:47 +0000 Subject: [test-suite] use “-async-proofs-cache force” when compiling --- test-suite/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 759cd99048..08ac34d1d6 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -44,7 +44,7 @@ coqdoc := $(BIN)coqdoc coqtopbyte := $(BIN)coqtop.byte coqtopload := $(coqtop) -async-proofs-cache force -load-vernac-source -coqtopcompile := $(coqtop) -compile +coqtopcompile := $(coqtop) -async-proofs-cache force -compile coqdep := $(BIN)coqdep -coqlib $(LIB) VERBOSE?= -- cgit v1.2.3