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 | |
| 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.
| -rw-r--r-- | .gitlab-ci.yml | 1 | ||||
| -rw-r--r-- | test-suite/Makefile | 14 |
2 files changed, 7 insertions, 8 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 948e4f0a37..6169c7e7e4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -130,6 +130,7 @@ after_script: # careful with the ending / - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ + - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH" - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all artifacts: name: "$CI_JOB_NAME.logs" 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 ####################################################################### |