Merge PR #11357: coq_makefile: don't use CAMLPKGS when building cmxa of mllib

Reviewed-by: gares

9 files changed, 56 insertions, 1 deletions

diff --git a/doc/changelog/08-tools/11357-master.rst b/doc/changelog/08-tools/11357-master.rst
new file mode 100644
index 0000000000..599db5b1da
--- /dev/null
+++ b/doc/changelog/08-tools/11357-master.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable
+  together with an unpacked (``mllib``) plugin. (`#11357
+  <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert).
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local
new file mode 100644
index 0000000000..0f4a7d9954
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local
@@ -0,0 +1 @@
+CAMLPKGS   += -package foo
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject
new file mode 100644
index 0000000000..cbdb43f842
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mllib
+src/test.mlg
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META
new file mode 100644
index 0000000000..ff5f1c7c96
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META
@@ -0,0 +1,4 @@
+archive(byte)="foo.cma"
+archive(native)="foo.cmxa"
+linkopts="-linkall"
+requires="str"
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile
new file mode 100644
index 0000000000..1615bfd067
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile
@@ -0,0 +1,14 @@
+-include ../../Makefile.conf
+
+CO="$(COQMF_OCAMLFIND)" opt
+CB="$(COQMF_OCAMLFIND)" ocamlc
+
+all:
+	$(CO) -c foolib.ml
+	$(CO) -a foolib.cmx -o foo.cmxa
+	$(CB) -c foolib.ml
+	$(CB) -a foolib.cmo -o foo.cma
+	$(CB) -c foo.mli # empty .mli file, to be understood
+
+clean:
+	rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml
new file mode 100644
index 0000000000..81306fb89b
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml
@@ -0,0 +1,2 @@
+let foo () =
+  assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3)
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh
new file mode 100755
index 0000000000..e53a7ed0f7
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+. ../template/init.sh
+mv src/test_plugin.mlpack src/test_plugin.mllib
+
+echo "let () = Foolib.foo ();;" >> src/test_aux.ml
+export OCAMLPATH=$OCAMLPATH:$PWD/findlib
+if which cygpath 2>/dev/null; then
+  # the only way I found to pass OCAMLPATH on win is to have it contain
+  # only one entry
+  OCAMLPATH=$(cygpath -w "$PWD"/findlib)
+  export OCAMLPATH
+fi
+make -C findlib/foo clean
+coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
+cat Makefile.local
+make -C findlib/foo
+make
+make byte
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 7c53ecfe18..7cd5962d86 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -632,7 +632,7 @@ $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
 
 $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
 	$(SHOW)'CAMLOPT -a -o $@'
-	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
 
 
 $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa