Separate unit tests into vernac and tactics

smtcoq · Apr 12, 2019 · 93bd713 · 93bd713
1 parent bcf5d89
commit 93bd713
Show file tree

Hide file tree

Showing 9 changed files with 587 additions and 545 deletions.
diff --git a/src/versions/native/Make b/src/versions/native/Make
@@ -37,10 +37,9 @@
 -I versions/native
 
 
--custom "cd ../unit-tests; make" "" "test"
--custom "cd ../unit-tests; make zchaff" "" "ztest"
--custom "cd ../unit-tests; make verit" "" "vtest"
--custom "cd ../unit-tests; make lfsc" "" "lfsctest"
+-custom "cd ../unit-tests; make vernac" "" "test"
+-custom "cd ../unit-tests; make zchaffv" "" "ztest"
+-custom "cd ../unit-tests; make veritv" "" "vtest"
 
 -custom "$(CAMLLEX) $<" "%.mll" "%.ml"
 -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"

diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
@@ -339,17 +339,14 @@ ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/sm
 %.ml: %.mll
 	$(CAMLLEX) $<
 
-lfsctest: 
-	cd ../unit-tests; make lfsc
-
 vtest: 
-	cd ../unit-tests; make verit
+	cd ../unit-tests; make veritv
 
 ztest: 
-	cd ../unit-tests; make zchaff
+	cd ../unit-tests; make zchaffv
 
 test: 
-	cd ../unit-tests; make
+	cd ../unit-tests; make vernac
 
 ####################
 #                  #
@@ -417,7 +414,6 @@ clean:
 	- rm -rf $(CMXS)
 	- rm -rf $(CMXA)
 	- rm -rf ml
-	- rm -rf lfsctest
 	- rm -rf vtest
 	- rm -rf ztest
 	- rm -rf test

diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local
@@ -17,7 +17,7 @@ lfsctest :
 	cd ../unit-tests; make lfsc
 
 clean::
-	cd ../unit-tests; make clean; rm *vo *glob
+	cd ../unit-tests; make clean
 
 
 CAMLLEX = $(CAMLBIN)ocamllex

diff --git a/unit-tests/Makefile b/unit-tests/Makefile
@@ -11,9 +11,19 @@ COQC?=$(COQBIN)coqc
 
 
 all: zchaff verit lfsc
-zchaff: $(ZCHAFFLOG) Tests_zchaff.vo
-verit: $(VERITLOG) Tests_verit.vo
-lfsc: Tests_lfsc.vo
+vernac: zchaffv veritv
+tactics: zchafft veritt lfsc
+
+zchaff: zchaffv zchafft
+zchaffv: $(ZCHAFFLOG) Tests_zchaff_vernac.vo
+zchafft: Tests_zchaff_tactics.vo
+
+verit: veritv veritt
+veritv: $(VERITLOG) Tests_verit_vernac.vo
+veritt: Tests_verit_tactics.vo
+
+lfsc: Tests_lfsc_tactics.vo
+
 logs: $(OBJ)
 
 
@@ -30,4 +40,4 @@ logs: $(OBJ)
 
 
 clean:
-	rm -rf *~ $(ZCHAFFLOG) $(VERITLOG)
+	rm -rf *~ $(ZCHAFFLOG) $(VERITLOG) *.vo *.glob
diff --git a/unit-tests/Tests_lfsc.v → unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc.v → unit-tests/Tests_lfsc_tactics.v