[coq_lib] Enforce that boot libraries depend on no theories

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ocaml · Jun 11, 2022 · 5e243ec · 5e243ec
1 parent f2f42dd
commit 5e243ec
Show file tree

Hide file tree

Showing 11 changed files with 42 additions and 0 deletions.
diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
@@ -133,6 +133,16 @@ module Theory = struct
              1.0 version of the Coq language"
         ]
 
+  let boot_has_deps loc =
+    User_error.raise ~loc
+      [ Pp.textf "(boot) libraries cannot have dependencies" ]
+
+  let check_boot_has_no_deps boot { Buildable.theories; _ } =
+    if boot then
+      match theories with
+      | [] -> ()
+      | t :: _ -> boot_has_deps (fst t)
+
   let decode =
     fields
       (let+ loc, name = field "name" Coq_lib_name.decode
@@ -145,6 +155,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 *)
+       check_boot_has_no_deps boot buildable;
        let package = select_deprecation ~package ~public in
        { loc
        ; name

diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/A.opam b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/A.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/a.v b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/a.v
@@ -0,0 +1 @@
+Inductive AnotherBegining := Of | The | Universe.
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune b/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))
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/A/dune-project b/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)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/B.opam b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/B.opam
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/b.v b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/b.v
@@ -0,0 +1 @@
+Inductive Begining := Of | The | Universe.
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name B)
+ (package B))
+
+
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/B/dune-project 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)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/dune-workspace b/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/dune-workspace
@@ -0,0 +1 @@
+(lang dune 3.2)
diff --git a/test/blackbox-tests/test-cases/coq/compose-boot-nodeps.t/run.t b/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]