[coq_lib] Enforce that boot libraries depend on no theories

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

src/dune_rules/coq_lib.ml

@@ -123,6 +123,7 @@ module Error = struct
       [ Pp.textf "Cannot have more than one boot theory in scope:"
       ; Pp.enumerate theories ~f:name
       ]
+
 end
 
 let top_closure =

src/dune_rules/coq_stanza.ml

@@ -83,6 +83,7 @@ module Extraction = struct
 end
 
 module Theory = struct
+
   type t =
     { loc : Loc.t
     ; name : Coq_lib_name.t
@@ -133,6 +134,9 @@ module Theory = struct
              1.0 version of the Coq language"
         ]
 
+  let boot_has_deps { Buildable.loc; _ } =
+    User_error.raise ~loc [ Pp.textf "(boot) libraries cannot have dependencies" ]
+
   let decode =
     fields
       (let+ loc, name = field "name" Coq_lib_name.decode
@@ -145,6 +149,8 @@ module Theory = struct
        and+ modules = Stanza_common.modules_field "modules"
        and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None ()
        and+ buildable = Buildable.decode in
+       (* boot libraries cannot depend on other theories *)
+       if boot && List.is_non_empty buildable.theories then boot_has_deps buildable;
        let package = select_deprecation ~package ~public in
        { loc
        ; name

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/a.v

@@ -0,0 +1 @@
+Inductive AnotherBegining := Of | The | Universe.

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune

@@ -0,0 +1,5 @@
+(coq.theory
+ (name A)
+ (package A)
+ (theories B)
+ (boot))

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.5)
+
+(using coq 0.2)

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/b.v

@@ -0,0 +1 @@
+Inductive Begining := Of | The | Universe.

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune

@@ -0,0 +1,5 @@
+(coq.theory
+ (name B)
+ (package B))
+
+

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.5)
+
+(using coq 0.2)

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/dune-workspace

@@ -0,0 +1 @@
+(lang dune 3.2)

test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t

@@ -0,0 +1,11 @@
+Testing composition with two boot libraries
+
+  $ dune build
+  File "A/dune", line 1, characters 0-57:
+  1 | (coq.theory
+  2 |  (name A)
+  3 |  (package A)
+  4 |  (theories B)
+  5 |  (boot))
+  Error: (boot) libraries cannot have dependencies
+  [1]