diff options
| author | Enrico Tassi | 2018-10-10 12:57:38 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-10-10 12:57:38 +0200 |
| commit | 6b7d0df8c077f40c53cc69a7192bdcdb0b483343 (patch) | |
| tree | 014e23abc0577393eec56a73e762c42a7b3309db | |
| parent | 71280c8f38824e28bb0464ed15d951b542e33b48 (diff) | |
| parent | 54b4c6e3f916f3913920bbd7a778f477543f0afb (diff) | |
Merge PR #8679: [test suite] Compile test cases, instead of only loading them
| -rw-r--r-- | test-suite/Makefile | 14 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_8553.v (renamed from test-suite/bugs/closed/8553.v) | 0 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_8672.v (renamed from test-suite/bugs/closed/8672.v) | 0 |
3 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index a1c6586d8a..ce448267fd 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -43,8 +43,8 @@ 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 -coqtopcompile := $(coqtop) -compile +coqtopload := $(coqtop) -async-proofs-cache force -load-vernac-source +coqtopcompile := $(coqtop) -async-proofs-cache force -compile coqdep := $(BIN)coqdep -coqlib $(LIB) VERBOSE?= @@ -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"; \ diff --git a/test-suite/bugs/closed/8553.v b/test-suite/bugs/closed/bug_8553.v index 4a1afabe89..4a1afabe89 100644 --- a/test-suite/bugs/closed/8553.v +++ b/test-suite/bugs/closed/bug_8553.v diff --git a/test-suite/bugs/closed/8672.v b/test-suite/bugs/closed/bug_8672.v index 66cd6dfa8c..66cd6dfa8c 100644 --- a/test-suite/bugs/closed/8672.v +++ b/test-suite/bugs/closed/bug_8672.v |