[coq] Don't allow public theories to depend on private ones.

For now we follow very simple rules, public theories cannot depend on
any way on private ones.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

src/dune/coq_lib.ml

@@ -46,6 +46,15 @@ module Error = struct
     let name = Coq_lib_name.to_string name in
     make ~loc [ Pp.textf "Theory %s not found" name ]
 
+  let private_deps_not_allowed ~loc private_dep =
+    let name = Coq_lib_name.to_string (name private_dep) in
+    make ~loc
+      [ Pp.textf
+          "Theory %S is private, it cannot be a dependency of a public theory. \
+           You need to associate %S to a package."
+          name name
+      ]
+
   let duplicate_boot_lib ~loc boot_theory =
     let name = Coq_lib_name.to_string (snd boot_theory.Dune_file.Coq.name) in
     make ~loc [ Pp.textf "Cannot have more than one boot library: %s)" name ]
@@ -97,9 +106,13 @@ module DB = struct
     in
     { boot; libs }
 
-  let resolve db (loc, name) =
+  let resolve ?(allow_private_deps = true) db (loc, name) =
     match Coq_lib_name.Map.find db.libs name with
-    | Some s -> Ok s
+    | Some s ->
+      if (not allow_private_deps) && Option.is_none s.package then
+        Error.private_deps_not_allowed ~loc s
+      else
+        Ok s
     | None -> Error.theory_not_found ~loc name
 
   let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name))
@@ -125,10 +138,15 @@ module DB = struct
       | Some (loc, stdlib) -> (loc, snd stdlib.name) :: t.theories
     in
     let open Result.O in
-    let* theories = Result.List.map ~f:(resolve db) theories in
+    let allow_private_deps = Option.is_none t.package in
+    let* theories = Result.List.map ~f:(resolve ~allow_private_deps db) theories in
     let key t = Coq_lib_name.to_string (snd t.name) in
-    let deps t = Result.List.map ~f:(resolve db) t.theories in
+    let deps t =
+      Result.List.map ~f:(resolve ~allow_private_deps db) t.theories
+    in
     Result.bind (Coq_lib_closure.top_closure theories ~key ~deps) ~f:(function
       | Ok libs -> Ok libs
       | Error cycle -> Error.cycle_found ~loc:(location t) cycle)
+
+  let resolve db l = resolve db l
 end

test/blackbox-tests/test-cases/coq/public_dep_on_private/dune

@@ -0,0 +1,3 @@
+(rule
+ (alias default)
+ (action (echo "%{read:public.install}")))

test/blackbox-tests/test-cases/coq/public_dep_on_private/dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.4)
+
+(using coq 0.1)

test/blackbox-tests/test-cases/coq/public_dep_on_private/private/a.v

@@ -0,0 +1 @@
+Definition foo := 3.

test/blackbox-tests/test-cases/coq/public_dep_on_private/private/dune

@@ -0,0 +1,2 @@
+(coq.theory
+ (name private))

test/blackbox-tests/test-cases/coq/public_dep_on_private/public/b.v

@@ -0,0 +1,3 @@
+From private Require a.
+
+Definition bar := a.foo.

test/blackbox-tests/test-cases/coq/public_dep_on_private/public/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name public)
+ (package public)
+ (theories private))

test/blackbox-tests/test-cases/coq/run.t

@@ -117,6 +117,21 @@
 # Test only works on Coq 8.12 due to boot constraints
 # $ dune build --root compose_boot/ --display short --debug-dependency-path
 
+  $ dune build --root public_dep_on_private/ --display short --debug-dependency-path
+  Entering directory 'public_dep_on_private'
+  File "public/dune", line 4, characters 11-18:
+  4 |  (theories private))
+                 ^^^^^^^
+  Error: Theory "private" is private, it cannot be a dependency of a public
+  theory. You need to associate "private" to a package.
+  -> required by public/b.v.d
+  -> required by public/b.vo
+  -> required by install lib/coq/user-contrib/public/b.vo
+  -> required by public.install
+  -> required by alias default
+  -> required by alias default
+  [1]
+
   $ dune build --root compose_cycle/ --display short --debug-dependency-path
   Entering directory 'compose_cycle'
   File "a/dune", line 2, characters 7-8: