add coqwc tests

11 files changed, 68 insertions, 1 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index ae426f0da..61e75fa5d 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -92,7 +92,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   coqdoc
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log
@@ -156,6 +156,7 @@ summary:
 	  $(call summary_dir, "IDE tests", ide); \
 	  $(call summary_dir, "VI tests", vio); \
 	  $(call summary_dir, "Coqchk tests", coqchk); \
+	  $(call summary_dir, "Coqwc tests", coqwc); \
 	  $(call summary_dir, "Coq makefile", coq-makefile); \
 	  $(call summary_dir, "Coqdoc tests", coqdoc); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
@@ -498,6 +499,26 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	  fi; \
 	} > "$@"
 
+# coqwc : test output
+
+coqwc : $(patsubst %.v,%.v.log,$(wildcard coqwc/*.v))
+
+coqwc/%.v.log : coqwc/%.v
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  tmpoutput=`mktemp /tmp/coqwc.XXXXXX`; \
+	  $(BIN)coqwc $< 2>&1 > $$tmpoutput; \
+	  diff -u --strip-trailing-cr coqwc/$*.out $$tmpoutput 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error! (unexpected output)"; \
+	  fi; \
+	  rm $$tmpoutput; \
+	} > "$@"
+
 # coq_makefile
 
 coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
diff --git a/test-suite/coqwc/BZ5637.out b/test-suite/coqwc/BZ5637.out
new file mode 100644
index 000000000..f0b5e4f7e
--- /dev/null
+++ b/test-suite/coqwc/BZ5637.out
@@ -0,0 +1,2 @@
+     spec    proof comments
+        5        0        0 coqwc/BZ5637.v
diff --git a/test-suite/coqwc/BZ5637.v b/test-suite/coqwc/BZ5637.v
new file mode 100644
index 000000000..6428b10ff
--- /dev/null
+++ b/test-suite/coqwc/BZ5637.v
@@ -0,0 +1,5 @@
+Local Obligation Tactic := idtac.
+Definition a := 1.
+Definition b := 1.
+Definition c := 1.
+Definition d := 1.
diff --git a/test-suite/coqwc/BZ5756.out b/test-suite/coqwc/BZ5756.out
new file mode 100644
index 000000000..039d1e500
--- /dev/null
+++ b/test-suite/coqwc/BZ5756.out
@@ -0,0 +1,2 @@
+     spec    proof comments
+        3        0        2 coqwc/BZ5756.v
diff --git a/test-suite/coqwc/BZ5756.v b/test-suite/coqwc/BZ5756.v
new file mode 100644
index 000000000..ccb12076a
--- /dev/null
+++ b/test-suite/coqwc/BZ5756.v
@@ -0,0 +1,3 @@
+Definition myNextValue := 0. (* OK *)
+Definition x := myNextValue. (* not OK *)
+Definition y := 0.
diff --git a/test-suite/coqwc/false.out b/test-suite/coqwc/false.out
new file mode 100644
index 000000000..14c5713f6
--- /dev/null
+++ b/test-suite/coqwc/false.out
@@ -0,0 +1,2 @@
+     spec    proof comments
+        3        3        1 coqwc/false.v
diff --git a/test-suite/coqwc/false.v b/test-suite/coqwc/false.v
new file mode 100644
index 000000000..640f9ea7f
--- /dev/null
+++ b/test-suite/coqwc/false.v
@@ -0,0 +1,8 @@
+Axiom x : nat.
+
+Definition foo (x : nat) := x + 1.
+
+Lemma bar : False.
+ idtac.
+ idtac. (* truth is overrated *)
+Admitted.
diff --git a/test-suite/coqwc/next-obligation.out b/test-suite/coqwc/next-obligation.out
new file mode 100644
index 000000000..7a0fd777c
--- /dev/null
+++ b/test-suite/coqwc/next-obligation.out
@@ -0,0 +1,2 @@
+     spec    proof comments
+        1        7        0 coqwc/next-obligation.v
diff --git a/test-suite/coqwc/next-obligation.v b/test-suite/coqwc/next-obligation.v
new file mode 100644
index 000000000..786df9891
--- /dev/null
+++ b/test-suite/coqwc/next-obligation.v
@@ -0,0 +1,10 @@
+(* make sure all proof lines are counted *)
+
+Goal True. 
+  Next Obligation.
+  idtac.
+  Next Obligation.
+  idtac.
+  Next Obligation.
+  idtac.
+Qed.  
diff --git a/test-suite/coqwc/theorem.out b/test-suite/coqwc/theorem.out
new file mode 100644
index 000000000..d01507bf7
--- /dev/null
+++ b/test-suite/coqwc/theorem.out
@@ -0,0 +1,2 @@
+     spec    proof comments
+        1        9        2 coqwc/theorem.v
diff --git a/test-suite/coqwc/theorem.v b/test-suite/coqwc/theorem.v
new file mode 100644
index 000000000..901c9074f
--- /dev/null
+++ b/test-suite/coqwc/theorem.v
@@ -0,0 +1,10 @@
+Theorem foo : True.
+Proof.
+  idtac. (* comment *)
+  idtac.
+  idtac.
+  idtac. (* comment *)
+  idtac.
+  idtac.
+  auto.
+Qed.