[scope] [coq] Make the full Coq scope creation lazy

Note the hack in coq_rules as to have better errors in case
of conflicting theories.

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

src/dune_rules/coq/coq_rules.ml

@@ -669,6 +669,11 @@ let install_rules ~sctx ~dir s =
     let loc = s.buildable.loc in
     let* mode = select_native_mode ~sctx ~dir buildable in
     let* scope = Scope.DB.find_by_dir dir in
+    (* We force the coq scope for this DB as to fail early in case of
+       some library conflicts that would also generate conflicting
+       install rules. This is needed as now install rules less lazy
+       than the theory rules. *)
+    let _ = Scope.coq_libs scope in
     let* dir_contents = Dir_contents.get sctx ~dir in
     let name = snd s.name in
     (* This must match the wrapper prefix for now to remain compatible *)

src/dune_rules/scope.ml

@@ -239,10 +239,11 @@ module DB = struct
       |> Path.Source.Map.of_list_multi
     in
     let coq_stanzas_by_project_dir =
-      List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
-          let project = stanza.project in
-          (Dune_project.root project, (dir, stanza)))
-      |> Path.Source.Map.of_list_multi
+      lazy
+        (List.map coq_stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
+             let project = stanza.project in
+             (Dune_project.root project, (dir, stanza)))
+        |> Path.Source.Map.of_list_multi)
     in
     let+ db_by_project_dir =
       Path.Source.Map.merge projects_by_dir stanzas_by_project_dir
@@ -257,36 +258,43 @@ module DB = struct
              in
              (project, db))
     in
+
     let coq_db_by_project_dir =
-      let find_db dir = snd (find_by_dir_in_map db_by_project_dir dir) in
-      Path.Source.Map.merge projects_by_dir coq_stanzas_by_project_dir
-        ~f:(fun _dir project coq_stanzas ->
-          assert (Option.is_some project);
-          let stanzas = Option.value coq_stanzas ~default:[] in
-          let entries =
-            List.map stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
-                let entry =
-                  match stanza.package with
-                  | None -> Coq_lib.DB.Theory dir
-                  | Some _ -> Redirect (Lazy.force public_theories)
-                in
-                (stanza, entry))
-          in
-          Some entries)
-      |> Path.Source.Map.map ~f:(fun stanzas ->
-             lazy
-               (let public_theories = Lazy.force public_theories in
+      lazy
+        (let public_theories = Lazy.force public_theories in
+         let find_db dir = snd (find_by_dir_in_map db_by_project_dir dir) in
+         Path.Source.Map.merge projects_by_dir
+           (Lazy.force coq_stanzas_by_project_dir)
+           ~f:(fun _dir project coq_stanzas ->
+             assert (Option.is_some project);
+             let stanzas = Option.value coq_stanzas ~default:[] in
+             let entries =
+               List.map stanzas ~f:(fun (dir, (stanza : Coq_stanza.Theory.t)) ->
+                   let entry =
+                     match stanza.package with
+                     | None -> Coq_lib.DB.Theory dir
+                     | Some _ -> Redirect 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))
     in
-    Path.Source.Map.merge db_by_project_dir coq_db_by_project_dir
-      ~f:(fun _dir project_and_db coq_db ->
-        let project, db = Option.value_exn project_and_db in
-        let coq_db = Option.value_exn coq_db in
+
+    let coq_db_find dir =
+      lazy
+        (let map = Lazy.force coq_db_by_project_dir in
+         Path.Source.Map.find_exn map dir)
+    in
+
+    Path.Source.Map.mapi db_by_project_dir ~f:(fun dir (project, db) ->
         let root =
           Path.Build.append_source build_dir (Dune_project.root project)
         in
-        Some { project; db; coq_db; root })
+        let coq_db = coq_db_find dir in
+        { project; db; coq_db; root })
 
   let create ~(context : Context.t) ~projects stanzas coq_stanzas =
     let open Memo.O in

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

@@ -4,4 +4,5 @@ Testing composition with two boot libraries
   Error: Cannot have more than one boot theory in scope:
   - B at B/dune:1
   - A at A/dune:1
+  -> required by alias default
   [1]

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

@@ -50,4 +50,7 @@ However if this boot library is public Dune will complain
   Error: Cannot have more than one boot theory in scope:
   - Coq at Coq/dune:1
   - Coq at B/Coq/dune:2
+  -> required by _build/default/B/Foo.dune-package
+  -> required by alias B/all
+  -> required by alias B/default
   [1]