diff --git a/src/coq_rules.ml b/src/coq_rules.ml index 6ffa58bc2ea..e2623f13f00 100644 --- a/src/coq_rules.ml +++ b/src/coq_rules.ml @@ -125,7 +125,8 @@ let setup_ml_deps ~lib_db libs = (* Pair of include flags and paths to mlpack *) let ml_iflags, mlpack = - let libs = libs_of_coq_deps ~lib_db libs in + let libs = libs_of_coq_deps ~lib_db libs + |> Lib.closure ~linking:false |> Result.ok_exn in Util.include_flags libs, List.concat_map ~f:ml_pack_files libs in diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/simple.ml b/test/blackbox-tests/test-cases/coq/ml_lib/src/simple.ml deleted file mode 100644 index 7d693024653..00000000000 --- a/test/blackbox-tests/test-cases/coq/ml_lib/src/simple.ml +++ /dev/null @@ -1 +0,0 @@ -let _ = 3 diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/dune b/test/blackbox-tests/test-cases/coq/ml_lib/src_a/dune similarity index 63% rename from test/blackbox-tests/test-cases/coq/ml_lib/src/dune rename to test/blackbox-tests/test-cases/coq/ml_lib/src_a/dune index d4f874c31be..7e053c7bba0 100644 --- a/test/blackbox-tests/test-cases/coq/ml_lib/src/dune +++ b/test/blackbox-tests/test-cases/coq/ml_lib/src_a/dune @@ -1,6 +1,6 @@ (library - (public_name ml_lib.ml_plugin) - (name ml_plugin) + (public_name ml_lib.ml_plugin_a) + (name ml_plugin_a) (flags :standard -rectypes) (libraries coq.plugins.ltac)) diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mlg b/test/blackbox-tests/test-cases/coq/ml_lib/src_a/gram.mlg similarity index 100% rename from test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mlg rename to test/blackbox-tests/test-cases/coq/ml_lib/src_a/gram.mlg diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mli b/test/blackbox-tests/test-cases/coq/ml_lib/src_a/gram.mli similarity index 100% rename from test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mli rename to test/blackbox-tests/test-cases/coq/ml_lib/src_a/gram.mli diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/ml_plugin.mlpack b/test/blackbox-tests/test-cases/coq/ml_lib/src_a/ml_plugin_a.mlpack similarity index 100% rename from test/blackbox-tests/test-cases/coq/ml_lib/src/ml_plugin.mlpack rename to test/blackbox-tests/test-cases/coq/ml_lib/src_a/ml_plugin_a.mlpack diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src_a/simple.ml b/test/blackbox-tests/test-cases/coq/ml_lib/src_a/simple.ml new file mode 100644 index 00000000000..555166169c9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/ml_lib/src_a/simple.ml @@ -0,0 +1,2 @@ +let a = 3 +let _ = a diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src_b/dune b/test/blackbox-tests/test-cases/coq/ml_lib/src_b/dune new file mode 100644 index 00000000000..e40e980f8d4 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/ml_lib/src_b/dune @@ -0,0 +1,5 @@ +(library + (public_name ml_lib.ml_plugin_b) + (name ml_plugin_b) + (flags :standard -rectypes) + (libraries ml_plugin_a)) diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src_b/ml_plugin_b.mlpack b/test/blackbox-tests/test-cases/coq/ml_lib/src_b/ml_plugin_b.mlpack new file mode 100644 index 00000000000..e69de29bb2d diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src_b/simple_b.ml b/test/blackbox-tests/test-cases/coq/ml_lib/src_b/simple_b.ml new file mode 100644 index 00000000000..04ea5df11e8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/ml_lib/src_b/simple_b.ml @@ -0,0 +1 @@ +let _ = Ml_plugin_a.Simple.a diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/theories/a.v b/test/blackbox-tests/test-cases/coq/ml_lib/theories/a.v index e784b669d76..340c0d8abb5 100644 --- a/test/blackbox-tests/test-cases/coq/ml_lib/theories/a.v +++ b/test/blackbox-tests/test-cases/coq/ml_lib/theories/a.v @@ -1,2 +1,3 @@ -Declare ML Module "ml_plugin". +Declare ML Module "ml_plugin_a". +Declare ML Module "ml_plugin_b". diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune b/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune index 736a5e9f4a3..72259ae558b 100644 --- a/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune +++ b/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune @@ -2,5 +2,5 @@ (name Plugin) (public_name ml_lib.Plugin) (synopsis "Test Plugin") - (libraries coq.plugins.ltac ml_lib.ml_plugin) + (libraries ml_lib.ml_plugin_b) (modules :standard)) diff --git a/test/blackbox-tests/test-cases/coq/run.t b/test/blackbox-tests/test-cases/coq/run.t index 15df108ad21..39f877a7f19 100644 --- a/test/blackbox-tests/test-cases/coq/run.t +++ b/test/blackbox-tests/test-cases/coq/run.t @@ -18,21 +18,29 @@ $ dune build --root ml_lib --display short --debug-dependency-path @all Entering directory 'ml_lib' - coqpp src/gram.ml - ocamldep src/.ml_plugin.objs/gram.ml.d - ocamlc src/.ml_plugin.objs/byte/ml_plugin.{cmi,cmo,cmt} - ocamlopt src/.ml_plugin.objs/native/ml_plugin.{cmx,o} - ocamldep src/.ml_plugin.objs/gram.mli.d - ocamlc src/.ml_plugin.objs/byte/ml_plugin__Gram.{cmi,cmti} - ocamlc src/.ml_plugin.objs/byte/ml_plugin__Gram.{cmo,cmt} - ocamldep src/.ml_plugin.objs/simple.ml.d - ocamlc src/.ml_plugin.objs/byte/ml_plugin__Simple.{cmi,cmo,cmt} - ocamlc src/ml_plugin.cma + coqpp src_a/gram.ml + ocamldep src_a/.ml_plugin_a.objs/gram.ml.d + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a.{cmi,cmo,cmt} + ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a.{cmx,o} + ocamldep src_a/.ml_plugin_a.objs/gram.mli.d + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a__Gram.{cmi,cmti} + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a__Gram.{cmo,cmt} + ocamldep src_a/.ml_plugin_a.objs/simple.ml.d + ocamlc src_a/.ml_plugin_a.objs/byte/ml_plugin_a__Simple.{cmi,cmo,cmt} + ocamlc src_a/ml_plugin_a.cma + ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b.{cmi,cmo,cmt} + ocamlopt src_b/.ml_plugin_b.objs/native/ml_plugin_b.{cmx,o} + ocamldep src_b/.ml_plugin_b.objs/simple_b.ml.d + ocamlc src_b/.ml_plugin_b.objs/byte/ml_plugin_b__Simple_b.{cmi,cmo,cmt} + ocamlc src_b/ml_plugin_b.cma coqdep theories/a.v.d - ocamlopt src/.ml_plugin.objs/native/ml_plugin__Gram.{cmx,o} - ocamlopt src/.ml_plugin.objs/native/ml_plugin__Simple.{cmx,o} - ocamlopt src/ml_plugin.{a,cmxa} - ocamlopt src/ml_plugin.cmxs + ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a__Gram.{cmx,o} + ocamlopt src_a/.ml_plugin_a.objs/native/ml_plugin_a__Simple.{cmx,o} + ocamlopt src_a/ml_plugin_a.{a,cmxa} + ocamlopt src_a/ml_plugin_a.cmxs + ocamlopt src_b/.ml_plugin_b.objs/native/ml_plugin_b__Simple_b.{cmx,o} + ocamlopt src_b/ml_plugin_b.{a,cmxa} + ocamlopt src_b/ml_plugin_b.cmxs coqc theories/a.vo $ dune build --root base --display short --debug-dependency-path @default