diff options
| author | Emilio Jesus Gallego Arias | 2018-09-30 18:49:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-09 14:00:11 +0200 |
| commit | 368d854566ee076618be625d0223657d31f8e13d (patch) | |
| tree | 79734c4d8fe5a0966db2a0b7d317c608fa319b1b /test-suite | |
| parent | 59de2827b63b5bc475452bef385a2149a10a631c (diff) | |
[test-suite] Use ocamlfind to locate Coq libraries in unit tests.
This is slightly more robust and allows to run the test suite with
Dune which may place OCaml objects differently.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index e35393b5e8..5e465ab47d 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -250,11 +250,11 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v # Unit tests ####################################################################### -OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) -SYSMOD:=-package num,str,unix,dynlink,threads +ifeq ($(LOCAL),true) + export OCAMLPATH := $(patsubst "%",%,$(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 +278,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 ####################################################################### |