Merge pull request #2088 from ejgallego/coq+full_deps

[coq] Pass closure of ML libs to Coq tools.
ocaml · Apr 26, 2019 · ea9080d · ea9080d
2 parents 817f6ed + af0a868
commit ea9080d
Show file tree

Hide file tree

Showing 13 changed files with 37 additions and 20 deletions.
diff --git 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
diff --git a/...kbox-tests/test-cases/coq/ml_lib/src/dune → ...ox-tests/test-cases/coq/ml_lib/src_a/dune b/...kbox-tests/test-cases/coq/ml_lib/src/dune → ...ox-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/...-tests/test-cases/coq/ml_lib/src/gram.mlg → ...ests/test-cases/coq/ml_lib/src_a/gram.mlg b/...-tests/test-cases/coq/ml_lib/src/gram.mlg → ...ests/test-cases/coq/ml_lib/src_a/gram.mlg
diff --git a/...-tests/test-cases/coq/ml_lib/src/gram.mli → ...ests/test-cases/coq/ml_lib/src_a/gram.mli b/...-tests/test-cases/coq/ml_lib/src/gram.mli → ...ests/test-cases/coq/ml_lib/src_a/gram.mli
diff --git a/...est-cases/coq/ml_lib/src/ml_plugin.mlpack → ...cases/coq/ml_lib/src_a/ml_plugin_a.mlpack b/...est-cases/coq/ml_lib/src/ml_plugin.mlpack → ...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
@@ -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
@@ -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
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
@@ -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
@@ -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
@@ -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
@@ -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