[wip] Modularize Coq scope

This PR is a RFC, as it is not clear what we'd like to do here.

There are two choices to support libraries :

- extend native Dune scope [current approach, introduced by ocaml#2053]
- make Super_context aware of the existence of different scope DB

Both approaches have strengths and weaknesses; the first one for
example forces to extend some `Lib` internals and indeed a few checks
there don't really make sense for Coq; the second approach introduces
some code duplication.

It seems to me that the approach this PR proposes could make more
sense; code duplication could be solved by using some programming
abstractions.

src/dune/coq_rules.ml

@@ -240,8 +240,9 @@ let setup_rules ~sctx ~build_dir ~dir ~dir_contents (s : Dune_file.Coq.t) =
   let cc = create_ccoq sctx ~dir in
   let name = snd s.name in
   let scope = SC.find_scope_by_dir sctx dir in
+  let coq_scope = SC.find_coq_scope_by_dir sctx dir in
   let lib_db = Scope.libs scope in
-  let coq_lib_db = Scope.coq_libs scope in
+  let coq_lib_db = Coq_scope.libs coq_scope in
   let expander = SC.expander sctx ~dir in
 
   let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in

src/dune/coq_scope.ml

@@ -0,0 +1,23 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2019                    *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+type t =
+  { db : Coq_lib.DB.t
+  }
+
+let libs { db; _ } = db
+
+module DB = struct
+
+  type scope = t
+  type t = scope
+
+  let create =
+    let db = Coq_lib.DB.create_from_coqlib_stanzas [] in
+    { db }
+
+  let find_by_project _t = Obj.magic 0
+  let find_by_dir _t = Obj.magic 0
+end

src/dune/coq_scope.mli

@@ -0,0 +1,20 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2019                    *)
+(* (c) INRIA 2020                              *)
+(* Written by: Emilio Jesús Gallego Arias *)
+
+open! Stdune
+type t
+
+(** Return the library database associated to this scope *)
+val libs : t -> Coq_lib.DB.t
+
+module DB : sig
+  type scope = t
+  type t
+  val create : t
+
+  val find_by_dir : t -> Path.Build.t -> scope
+  val find_by_project : t -> Dune_project.t -> scope
+
+end with type scope := t

src/dune/lib.ml

@@ -1683,7 +1683,6 @@ module DB = struct
       | Library of Path.Build.t * Dune_file.Library.t
       | External_variant of Dune_file.External_variant.t
       | Deprecated_library_name of Dune_file.Deprecated_library_name.t
-      | Coq_theory of Path.Build.t * Dune_file.Coq.t
   end
 
   module Found_or_redirect = struct
@@ -1697,9 +1696,7 @@ module DB = struct
     List.iter stanzas ~f:(fun (stanza : Library_related_stanza.t) ->
         match stanza with
         | Library _
-        | Deprecated_library_name _
-        | Coq_theory _ ->
-          ()
+        | Deprecated_library_name _ -> ()
         | External_variant ev -> (
           let loc, virtual_lib = ev.virtual_lib in
           match
@@ -1816,10 +1813,7 @@ module DB = struct
               else
                 [ (name, Found info)
                 ; (Lib_name.of_local conf.name, Redirect p.name)
-                ] )
-          | Coq_theory _ ->
-            (* As of today Coq theories do live in a separate namespace *)
-            [])
+                ] ))
       |> Lib_name.Map.of_list_reducei
            ~f:(fun name (v1 : Found_or_redirect.t) v2 ->
              let res =

src/dune/lib.mli

@@ -185,7 +185,6 @@ module DB : sig
       | Library of Path.Build.t * Dune_file.Library.t
       | External_variant of Dune_file.External_variant.t
       | Deprecated_library_name of Dune_file.Deprecated_library_name.t
-      | Coq_theory of Path.Build.t * Dune_file.Coq.t
   end
 
   (** Create a database from a list of library/variants stanzas *)

src/dune/scope.ml

@@ -4,7 +4,6 @@ open Import
 type t =
   { project : Dune_project.t
   ; db : Lib.DB.t
-  ; coq_db : Coq_lib.DB.t
   ; root : Path.Build.t
   }
 
@@ -16,8 +15,6 @@ let project t = t.project
 
 let libs t = t.db
 
-let coq_libs t = t.coq_db
-
 module DB = struct
   type scope = t
 
@@ -71,11 +68,7 @@ module DB = struct
               ; _
               } ->
             Some
-              (Dune_file.Public_lib.name old_public_name, Name new_public_name)
-          | Coq_theory _ ->
-            (* All libraries in Coq are private to a scope for now, we will lift
-               this restriction soon *)
-            None)
+              (Dune_file.Public_lib.name old_public_name, Name new_public_name))
       |> Lib_name.Map.of_list
       |> function
       | Ok x -> x
@@ -119,7 +112,6 @@ module DB = struct
             | Library (_, lib) -> lib.project
             | External_variant ev -> ev.project
             | Deprecated_library_name x -> x.project
-            | Coq_theory (_, thr) -> thr.project
           in
           (Dune_project.root project, stanza))
       |> Path.Source.Map.of_list_multi
@@ -131,16 +123,10 @@ module DB = struct
         let db =
           Lib.DB.create_from_stanzas stanzas ~parent:public_libs ~lib_config
         in
-        let coq_stanzas =
-          List.filter_map stanzas ~f:(function
-            | Coq_theory (p, l) -> Some (p, l)
-            | _ -> None)
-        in
-        let coq_db = Coq_lib.DB.create_from_coqlib_stanzas coq_stanzas in
         let root =
           Path.Build.append_source build_context_dir (Dune_project.root project)
         in
-        Some { project; db; coq_db; root })
+        Some { project; db; root })
 
   let create ~projects ~context ~installed_libs ~lib_config stanzas =
     let t = Fdecl.create Dyn.Encoder.opaque in

src/dune/scope.mli

@@ -15,8 +15,6 @@ val project : t -> Dune_project.t
 (** Return the library database associated to this scope *)
 val libs : t -> Lib.DB.t
 
-val coq_libs : t -> Coq_lib.DB.t
-
 (** Scope databases *)
 module DB : sig
   type scope = t

src/dune/super_context.ml

@@ -175,6 +175,7 @@ end
 type t =
   { context : Context.t
   ; scopes : Scope.DB.t
+  ; coq_scopes : Coq_scope.DB.t
   ; public_libs : Lib.DB.t
   ; installed_libs : Lib.DB.t
   ; stanzas : Dune_file.Stanzas.t Dir_with_dune.t list
@@ -242,6 +243,8 @@ let installed_libs t = t.installed_libs
 
 let find_scope_by_dir t dir = Scope.DB.find_by_dir t.scopes dir
 
+let find_coq_scope_by_dir t dir = Coq_scope.DB.find_by_dir t.coq_scopes dir
+
 let find_scope_by_project t = Scope.DB.find_by_project t.scopes
 
 let find_project_by_key t = Dune_project.File_key.Map.find_exn t.projects_by_key
@@ -441,16 +444,12 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas
           | Dune_file.External_variant ev -> External_variant ev :: acc
           | Dune_file.Deprecated_library_name d ->
             Deprecated_library_name d :: acc
-          | Dune_file.Coq.T coq_lib ->
-            let ctx_dir =
-              Path.Build.append_source context.build_dir dune_file.dir
-            in
-            Coq_theory (ctx_dir, coq_lib) :: acc
           | _ -> acc)
     in
     Scope.DB.create ~projects ~context:context.name ~installed_libs ~lib_config
       stanzas
   in
+  let coq_scopes = Coq_scope.DB.create in
   let stanzas =
     List.map stanzas ~f:(fun { Dune_load.Dune_file.dir; project; stanzas } ->
         let ctx_dir = Path.Build.append_source context.build_dir dir in
@@ -524,6 +523,7 @@ let create ~(context : Context.t) ?host ~projects ~packages ~stanzas
   ; root_expander
   ; host
   ; scopes
+  ; coq_scopes
   ; public_libs
   ; installed_libs
   ; stanzas

src/dune/super_context.mli

@@ -87,6 +87,8 @@ val dump_env : t -> dir:Path.Build.t -> Dune_lang.t list Build.t
 
 val find_scope_by_dir : t -> Path.Build.t -> Scope.t
 
+val find_coq_scope_by_dir : t -> Path.Build.t -> Coq_scope.t
+
 val find_scope_by_project : t -> Dune_project.t -> Scope.t
 
 val find_project_by_key : t -> Dune_project.File_key.t -> Dune_project.t