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


From e739af593ae0a9ca20a839aa2a481628dd768ef6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 4 Oct 2018 09:14:32 +0000
Subject: [default.nix] some fixes

---
 default.nix | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/default.nix b/default.nix
index 1faaafae03..a5c4c1fbb9 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,6 +84,10 @@ 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 = ''
-- 
cgit v1.2.3


From 41dcd52864a569d2a0305ce97ad335238a0bc17d Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 4 Oct 2018 09:57:09 +0000
Subject: [default.nix] Add install dir to OCAMLPATH before running the
 test-suite

---
 default.nix         | 1 +
 test-suite/Makefile | 5 ++++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/default.nix b/default.nix
index a5c4c1fbb9..1cc74dc0d2 100644
--- a/default.nix
+++ b/default.nix
@@ -93,6 +93,7 @@ stdenv.mkDerivation rec {
   preInstallCheck = ''
     patchShebangs tools/
     patchShebangs test-suite/
+    export OCAMLPATH=$OCAMLFIND_DESTDIR:$OCAMLPATH
   '';
 
   installCheckTarget = [ "check" ];
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5e465ab47d..d088702b44 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -250,8 +250,11 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 # Unit tests
 #######################################################################
 
+# 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 := $(patsubst "%",%,$(COQLIBINSTALL))
+  export OCAMLPATH := $(shell echo $(COQLIBINSTALL))
 endif
 
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
-- 
cgit v1.2.3