[scope] [coq] Make Coq_lib.DB creation lazy

This will be important once we have installed_theories in ocaml#7047

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

CHANGES.md

@@ -3,6 +3,7 @@ Unreleased
 
 - Fix preludes not being recorded as dependencies in the `(mdx)` stanza (#7109,
   fixes #7077, @emillon).
+- Make coq_db creation in scope lazy (@ejgallego, #)
 
 3.7.0 (2023-02-17)
 ------------------

src/dune_rules/scope.ml

@@ -4,7 +4,7 @@ open Memo.O
 type t =
   { project : Dune_project.t
   ; db : Lib.DB.t
-  ; coq_db : Coq_lib.DB.t
+  ; coq_db : Coq_lib.DB.t Lazy.t
   ; root : Path.Build.t
   }
 
@@ -14,7 +14,7 @@ let project t = t.project
 
 let libs t = t.db
 
-let coq_libs t = t.coq_db
+let coq_libs t = Lazy.force t.coq_db
 
 module DB = struct
   type scope = t
@@ -161,6 +161,9 @@ module DB = struct
         else None)
     |> Coq_lib.DB.create_from_coqlib_stanzas ~find_db ~parent:None
 
+  let public_theories ~find_db coq_stanzas =
+    lazy (public_theories ~find_db coq_stanzas)
+
   (* Create a database from the public libraries defined in the stanzas *)
   let public_libs t ~installed_libs ~lib_config stanzas =
     let public_libs =
@@ -265,14 +268,16 @@ module DB = struct
                 let entry =
                   match stanza.package with
                   | None -> Coq_lib.DB.Theory dir
-                  | Some _ -> Redirect public_theories
+                  | Some _ -> Redirect (Lazy.force public_theories)
                 in
                 (stanza, entry))
           in
           Some entries)
       |> Path.Source.Map.map ~f:(fun stanzas ->
-             Coq_lib.DB.create_from_coqlib_stanzas
-               ~parent:(Some public_theories) ~find_db stanzas)
+             lazy
+               (let public_theories = Lazy.force public_theories in
+                Coq_lib.DB.create_from_coqlib_stanzas
+                  ~parent:(Some public_theories) ~find_db stanzas))
     in
     Path.Source.Map.merge db_by_project_dir coq_db_by_project_dir
       ~f:(fun _dir project_and_db coq_db ->