diff options
| author | Enrico Tassi | 2018-10-10 12:59:11 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-10-10 12:59:11 +0200 |
| commit | b4fd032e0a05533bab701125c4abcbf392c799c7 (patch) | |
| tree | d8e7b8b786e60066c1c5279f401bbc780edd7d65 /test-suite | |
| parent | 6b7d0df8c077f40c53cc69a7192bdcdb0b483343 (diff) | |
| parent | 41dcd52864a569d2a0305ce97ad335238a0bc17d (diff) | |
Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit tests.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index ce448267fd..b4cc3dda11 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -250,11 +250,14 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v # Unit tests ####################################################################### -OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) -SYSMOD:=-package num,str,unix,dynlink,threads +# COQLIBINSTALL is quoted in config/make thus we must unquote it, +# otherwise the directory name will include the quotes, see +# see for example https://stackoverflow.com/questions/10424645/how-to-convert-a-quoted-string-to-a-normal-one-in-makefile +ifeq ($(LOCAL),true) + export OCAMLPATH := $(shell echo $(COQLIBINSTALL)) +endif -COQSRCDIRS:=$(addprefix -I $(LIB)/,$(CORESRCDIRS)) -COQCMXS:=$(addprefix $(LIB)/,$(LINKCMX)) +OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) # ML files from unit-test framework, not containing tests UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) @@ -278,10 +281,8 @@ unit-tests: $(UNIT_LOGFILES) # Build executable, run it to generate log file 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) $(COQCMXS) \ - $(UNIT_CMXS) $< -o $<.test; + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -package coq.toplevel,oUnit \ + -I unit-tests/src $(UNIT_CMXS) $< -o $<.test; $(HIDE)./$<.test ####################################################################### |