diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-16 20:36:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-16 20:36:34 +0200 |
| commit | d0243311634a8d6fa77fb2d0bb36eab96186a605 (patch) | |
| tree | 78708423b22b7b5025c4fae1d35a725de6bba830 /test-suite/Makefile | |
| parent | 107e42b0776a0979e522e82654435d9f2bea7a80 (diff) | |
Modify make system to include Makefile.common in the test suite
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 21 |
1 files changed, 8 insertions, 13 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index a6e6283bf..ce21ff41c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -26,6 +26,7 @@ ########################################################################### include ../config/Makefile +include ../Makefile.common ####################################################################### # Variables @@ -258,31 +259,25 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) SYSMOD:=-package num,str,unix,dynlink,threads -COQSRCDIRS=-I $(LIB)/clib -I $(LIB)/lib -I $(LIB)/kernel -I $(LIB)/kernel/byterun \ --I $(LIB)/library -I $(LIB)/engine -I $(LIB)/pretyping -I $(LIB)/interp \ --I $(LIB)/proofs -I $(LIB)/parsing -I $(LIB)/printing -I $(LIB)/tactics -I $(LIB)/vernac \ --I $(LIB)/stm -I $(LIB)/toplevel +COQSRCDIRS:=$(addprefix -I $(LIB)/,$(CORESRCDIRS)) +COQCMXS:=$(addprefix $(LIB)/,$(LINKCMX)) # ML files from unit-test framework, not containing tests -UNIT_SRCFILES=$(shell find ./unit-tests/src -name *.ml) +UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) UNIT_CMXS=utest.cmx -# this is same link order as CORECMA in Makefile.common in Coq root dir -COQCMXAS=clib.cmxa lib.cmxa kernel.cmxa library.cmxa engine.cmxa pretyping.cmxa \ - interp.cmxa proofs.cmxa parsing.cmxa printing.cmxa tactics.cmxa vernac.cmxa stm.cmxa toplevel.cmxa - -unit-tests/src/utest.cmx : unit-tests/src/utest.ml unit-tests/src/utest.cmi +unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi $(SHOW) 'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $< -unit-tests/src/utest.cmi : unit-tests/src/utest.mli +unit-tests/src/utest.cmi: unit-tests/src/utest.mli $(SHOW) 'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) -package oUnit $< -$(UNIT_LOGFILES) : unit-tests/src/utest.cmx +$(UNIT_LOGFILES): unit-tests/src/utest.cmx unit-tests: $(UNIT_LOGFILES) @@ -291,7 +286,7 @@ unit-tests/%.ml.log: unit-tests/%.ml $(SHOW) 'TEST $<' $(HIDE)$(OCAMLOPT) -linkall -linkpkg -cclib -lcoqrun \ $(SYSMOD) -package camlp5.gramlib,oUnit \ - -I unit-tests/src $(COQSRCDIRS) $(COQCMXAS) \ + -I unit-tests/src $(COQSRCDIRS) $(COQCMXS) \ $(UNIT_CMXS) $< -o $<.test; $(HIDE)./$<.test |