[coq] Re-add boot library to list of dependencies in Coq_lib.DB

Should fix a bug introduced in ocaml#5866 , the handling of boot Coq lib really needs to be done at the top level as coqdep's `source_rule` etc... need to be aware of it. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego · Sep 27, 2022 · 96a3789 · 96a3789
1 parent 27f1c04
commit 96a3789
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 3 deletions.
diff --git a/src/dune_rules/coq_lib.ml b/src/dune_rules/coq_lib.ml
@@ -50,6 +50,8 @@ include struct
     ; boot : t option Resolve.t
     ; id : Id.t
     ; implicit : bool (* Only useful for the stdlib *)
+    ; use_stdlib : bool
+          (* whether this theory uses the stdlib, eventually set to false for all libs *)
     ; src_root : Path.Build.t
     ; obj_root : Path.Build.t
     ; theories : (Loc.t * t) list Resolve.t
@@ -183,6 +185,7 @@ module DB = struct
         let open Memo.O in
         let* boot = if s.boot then Resolve.Memo.return None else boot coq_db in
         let allow_private_deps = Option.is_none s.package in
+        let use_stdlib = true in
         let+ libraries =
           Resolve.Memo.List.map s.buildable.plugins ~f:(fun (loc, lib) ->
               let open Resolve.Memo.O in
@@ -237,19 +240,29 @@ module DB = struct
                   | Some _ -> Resolve.Memo.return ()
                   | None -> Error.private_deps_not_allowed ~loc theory_name
               in
-
               (loc, theory))
         in
+        let theories =
+          Resolve.O.(
+            let* boot = boot in
+            match boot with
+            | Some boot when use_stdlib ->
+              let+ theories = theories in
+              (* TODO: if lib is boot, don't add boot dep *)
+              (* maybe use the loc for boot? *)
+              (Loc.none, boot) :: theories
+            | Some _ | None -> theories)
+        in
         let map_error x =
           let human_readable_description () = Id.pp id in
           Resolve.push_stack_frame ~human_readable_description x
         in
         let theories = map_error theories in
         let libraries = map_error libraries in
-
         { loc = s.buildable.loc
         ; boot
         ; id
+        ; use_stdlib
         ; implicit = s.boot
         ; obj_root = dir
         ; src_root = dir

diff --git a/src/dune_rules/coq_rules.ml b/src/dune_rules/coq_rules.ml
@@ -88,7 +88,7 @@ module Bootstrap = struct
     let dir = Coq_lib.src_root lib in
     S
       (if coqdoc then [ A "--coqlib"; Path (Path.build dir) ]
-      else [ A "-boot"; Util.theory_coqc_flag lib ])
+      else [ A "-boot" ])
 
   let flags ~coqdoc t : _ Command.Args.t =
     match t with