diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2017-10-03 10:56:55 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2017-10-03 10:56:55 +0200 |
| commit | 1cedf0df745cc5ed6bf5031b59f84fc37c8ce9f0 (patch) | |
| tree | 1bc1d7da809dc8f1b06c82a029bd1c8ba9b0c00c /src/versions | |
| parent | 0d5b50fad7bf72dd0fe332eab05c68bd932220b0 (diff) | |
| download | smtcoq-1cedf0df745cc5ed6bf5031b59f84fc37c8ce9f0.tar.gz smtcoq-1cedf0df745cc5ed6bf5031b59f84fc37c8ce9f0.zip | |
Tests for Coq-8.6
Diffstat (limited to 'src/versions')
| -rw-r--r-- | src/versions/standard/Make | 8 | ||||
| -rw-r--r-- | src/versions/standard/Makefile | 29 |
2 files changed, 31 insertions, 6 deletions
diff --git a/src/versions/standard/Make b/src/versions/standard/Make index 7c4497e..2445f87 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -10,6 +10,8 @@ ## To generate the Makefile: ## ## coq_makefile -f Make -o Makefile ## ## Suppress the "Makefile" target ## +## Suppress the "test", "ztest", "vtest" and "./" dependencies from ## +## the all target ## ## Change the "all" target into: ## ## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ## @@ -37,9 +39,9 @@ -I $(COQBIN)../plugins/micromega -# -extra "test" "" "cd ../unit-tests; make" "" -# -extra "ztest" "" "cd ../unit-tests; make zchaff" -# -extra "vtest" "" "cd ../unit-tests; make verit" +-extra "test" "" "cd ../unit-tests; make" "" +-extra "ztest" "" "cd ../unit-tests; make zchaff" +-extra "vtest" "" "cd ../unit-tests; make verit" -extra "%.ml" "%.mll" "$(CAMLLEX) $<" -extra "%.ml %.mli" "%.mly" "$(CAMLYACC) $<" diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index 9fda4ea..1a6eb97 100644 --- a/src/versions/standard/Makefile +++ b/src/versions/standard/Makefile @@ -314,7 +314,7 @@ endif # # ####################################### -all: $(VOFILES) $(CMOFILES) $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) +all: $(VOFILES) $(CMOFILES) $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) mlihtml: $(MLIFILES:.mli=.cmi) mkdir $@ || rm -rf $@/* @@ -359,7 +359,7 @@ beautify: $(VFILES:=.beautified) @echo 'Do not do "make clean" until you are sure that everything went well!' @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo smtcoq_plugin.mlpack.d +.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo ./ smtcoq_plugin.mlpack.d ################### # # @@ -367,6 +367,15 @@ beautify: $(VFILES:=.beautified) # # ################### +test: + cd ../unit-tests; make + +ztest: + cd ../unit-tests; make zchaff + +vtest: + cd ../unit-tests; make verit + %.ml: %.mll $(CAMLLEX) $< @@ -375,6 +384,15 @@ beautify: $(VFILES:=.beautified) smtcoq_plugin.mlpack.d: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml +################### +# # +# Subdirectories. # +# # +################### + +./: + +cd "./" && $(MAKE) all + ##################################### # # # Ad-hoc implicit rules for mlpack. # @@ -419,6 +437,7 @@ install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink) install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ done + +cd ./ && $(MAKE) DSTROOT="$(DSTROOT)" INSTALLDEFAULTROOT="$(INSTALLDEFAULTROOT)/./" install install-doc: install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/html @@ -499,12 +518,17 @@ clean:: rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - rm -rf html mlihtml uninstall_me.sh + - rm -rf test + - rm -rf ztest + - rm -rf vtest + +cd ./ && $(MAKE) clean cleanall:: clean rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) archclean:: rm -f *.cmx *.o + +cd ./ && $(MAKE) archclean printenv: @"$(COQBIN)coqtop" -config @@ -515,7 +539,6 @@ printenv: @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' - ################### # # # Implicit rules. # |