From 368d854566ee076618be625d0223657d31f8e13d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 30 Sep 2018 18:49:34 +0200 Subject: [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. --- .gitlab-ci.yml | 1 + 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 ####################################################################### -- cgit v1.2.3