From 763b635a4cf54efc1cf7793c1d841a3abbcd16ac Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 11 Jun 2022 13:10:42 +0200
Subject: [PATCH] [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    | 1 +
 src/dune_rules/coq_stanza.ml | 6 ++++++
 2 files changed, 7 insertions(+)

diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml
index 6154496e2634..fb0c803ddd02 100644
--- a/src/dune_rules/coq_lib.ml
+++ b/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 =
diff --git a/src/dune_rules/coq_stanza.ml b/src/dune_rules/coq_stanza.ml
index 93de0b1beda3..7993a0f8b063 100644
--- a/src/dune_rules/coq_stanza.ml
+++ b/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 () =
+    User_error.raise [ 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 ();
        let package = select_deprecation ~package ~public in
        { loc
        ; name