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 | |
| parent | 6b7d0df8c077f40c53cc69a7192bdcdb0b483343 (diff) | |
| parent | 41dcd52864a569d2a0305ce97ad335238a0bc17d (diff) | |
Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit tests.
| -rw-r--r-- | .gitlab-ci.yml | 1 | ||||
| -rw-r--r-- | default.nix | 7 | ||||
| -rw-r--r-- | test-suite/Makefile | 17 |
3 files changed, 17 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/default.nix b/default.nix index 1faaafae03..1cc74dc0d2 100644 --- a/default.nix +++ b/default.nix @@ -75,6 +75,8 @@ stdenv.mkDerivation rec { (path: _: !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; + preConfigure = "patchShebangs kernel/"; + prefixKey = "-prefix "; buildFlags = [ "world" "byte" ] ++ optional buildDoc "doc-html"; @@ -82,11 +84,16 @@ stdenv.mkDerivation rec { installTargets = [ "install" "install-byte" ] ++ optional buildDoc "install-doc-html"; + createFindlibDestdir = !shell; + + postInstall = "ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq"; + inherit doInstallCheck; preInstallCheck = '' patchShebangs tools/ patchShebangs test-suite/ + export OCAMLPATH=$OCAMLFIND_DESTDIR:$OCAMLPATH ''; installCheckTarget = [ "check" ]; 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 ####################################################################### |