Merge PR #958: coq_makefile: build/use .cma for packed plugins too

12 files changed, 49 insertions, 0 deletions

diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 1feff7479..dc5a500db 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
 ./test
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.glob
 ./test/test.v
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 1feff7479..dc5a500db 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
 ./test
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.glob
 ./test/test.v
diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local
new file mode 100644
index 000000000..0f4a7d995
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/Makefile.local
@@ -0,0 +1 @@
+CAMLPKGS   += -package foo
diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META
new file mode 100644
index 000000000..ff5f1c7c9
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/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/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
new file mode 100644
index 000000000..31cf11665
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/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/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml
new file mode 100644
index 000000000..81306fb89
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/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/run.sh b/test-suite/coq-makefile/findlib-package/run.sh
new file mode 100755
index 000000000..a0d8a7fea
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/run.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+. ../template/init.sh
+
+echo "let () = Foolib.foo ();;" >> src/test_aux.ml
+export OCAMLPATH=$OCAMLPATH:$PWD/findlib
+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/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 51669f28f..03df9cf05 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 51669f28f..03df9cf05 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 3bec11cb7..89bafe9ad 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -18,6 +18,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo