feature(coq): support for inter-project composition of theories

Signed-off-by: Ali Caglayan <[email protected]>

src/dune_rules/coq_lib.ml

@@ -76,9 +76,10 @@ end
 module DB = struct
   type lib = t
 
-  type nonrec t =
-    { boot : (Loc.t * t) option
-    ; libs : t Coq_lib_name.Map.t
+  type t =
+    { boot : (Loc.t * lib) option
+    ; libs : lib Coq_lib_name.Map.t
+    ; parent : t option
     }
 
   let boot_library { boot; _ } = boot
@@ -97,7 +98,7 @@ module DB = struct
       } )
 
   (* Should we register errors and printers, or raise is OK? *)
-  let create_from_coqlib_stanzas sl =
+  let create_from_coqlib_stanzas ~(parent : t option) sl =
     let libs =
       match Coq_lib_name.Map.of_list_map ~f:create_from_stanza sl with
       | Ok m -> m
@@ -111,15 +112,19 @@ module DB = struct
       | _ :: (_, s2) :: _ ->
         Result.ok_exn (Error.duplicate_boot_lib ~loc:s2.buildable.loc s2)
     in
-    { boot; libs }
+    { boot; libs; parent }
 
-  let resolve ?(allow_private_deps = true) db (loc, name) =
+  (* TODO: what is the point of this flag? *)
+  let rec resolve ?(allow_private_deps = true) db (loc, name) =
     match Coq_lib_name.Map.find db.libs name with
     | Some s ->
       if (not allow_private_deps) && Option.is_none s.package then
         Error.private_deps_not_allowed ~loc s
       else Ok s
-    | None -> Error.theory_not_found ~loc name
+    | None -> (
+      match db.parent with
+      | Some parent -> resolve ~allow_private_deps parent (loc, name)
+      | None -> Error.theory_not_found ~loc name)
 
   let find_many t ~loc = Result.List.map ~f:(fun name -> resolve t (loc, name))
 

src/dune_rules/coq_lib.mli

@@ -27,7 +27,7 @@ module DB : sig
 
   type t
 
-  val create_from_coqlib_stanzas :
+  val create_from_coqlib_stanzas : parent:t option ->
     (Path.Build.t * Coq_stanza.Theory.t) list -> t
 
   val find_many : t -> loc:Loc.t -> Coq_lib_name.t list -> lib list Or_exn.t

src/dune_rules/scope.ml

@@ -132,6 +132,11 @@ module DB = struct
       Lib.DB.Resolve_result.redirect (Some scope.db) (Loc.none, name)
     | Some (Name name) -> Lib.DB.Resolve_result.redirect None name
 
+  let public_theories coq_stanzas =
+    List.filter coq_stanzas ~f:(fun (_, (stanza : Coq_stanza.Theory.t)) ->
+        Option.is_some stanza.package)
+    |> Coq_lib.DB.create_from_coqlib_stanzas ~parent:None
+
   (* Create a database from the public libraries defined in the stanzas *)
   let public_libs t ~installed_libs ~modules_of_lib ~lib_config
       ~projects_by_package stanzas =
@@ -178,7 +183,7 @@ module DB = struct
   module Path_source_map_traversals = Memo.Make_map_traversals (Path.Source.Map)
 
   let scopes_by_dir context ~projects_by_package ~modules_of_lib ~projects
-      ~public_libs stanzas coq_stanzas =
+      ~public_libs ~public_theories stanzas coq_stanzas =
     let open Memo.O in
     let projects_by_dir =
       List.map projects ~f:(fun (project : Dune_project.t) ->
@@ -196,12 +201,21 @@ module DB = struct
           (Dune_project.root project, stanza))
       |> Path.Source.Map.of_list_multi
     in
-    let coq_db_by_project_dir =
-      List.map coq_stanzas ~f:(fun (dir, t) ->
-          let project = t.Coq_stanza.Theory.project in
-          (Dune_project.root project, (dir, t)))
+    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
-      |> Path.Source.Map.map ~f:Coq_lib.DB.create_from_coqlib_stanzas
+    in
+    let coq_db_by_project_dir =
+      Path.Source.Map.merge projects_by_dir coq_stanzas_by_project_dir
+        ~f:(fun _dir project coq_stanzas ->
+          let project = Option.value_exn project in
+          let stanzas = Option.value coq_stanzas ~default:[] in
+          Some (project, stanzas))
+      |> Path.Source.Map.map ~f:(fun (project, stanzas) ->
+        let db = Coq_lib.DB.create_from_coqlib_stanzas ~parent:(Some public_theories) stanzas in
+        (project, db))
     in
     let lib_config = Context.lib_config context in
     let+ db_by_project_dir =
@@ -221,11 +235,8 @@ module DB = struct
     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 =
-          match coq_db with
-          | Some db -> db
-          | None -> Coq_lib.DB.create_from_coqlib_stanzas []
-        in
+        let project', coq_db = Option.value_exn coq_db in
+        assert (Dune_project.equal project project');
         let root =
           Path.Build.append_source context.build_dir (Dune_project.root project)
         in
@@ -240,9 +251,10 @@ module DB = struct
       public_libs t ~installed_libs ~lib_config ~projects_by_package
         ~modules_of_lib stanzas
     in
+    let public_theories = public_theories coq_stanzas in
     let+ by_dir =
       scopes_by_dir context ~projects ~projects_by_package ~public_libs
-        ~modules_of_lib stanzas coq_stanzas
+        ~public_theories ~modules_of_lib stanzas coq_stanzas
     in
     let value = { by_dir } in
     Fdecl.set t value;

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/a.v

@@ -0,0 +1,2 @@
+
+Inductive Hello := World | Bye.

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name A)
+ (package A))
+

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/A/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/b.v

@@ -0,0 +1,4 @@
+From A Require Import a.
+
+Check Hello.
+

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune

@@ -0,0 +1,4 @@
+(coq.theory
+ (name B)
+ (libraries other-lib)
+ (theories A))

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/B/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.2)
+(using coq 0.3)

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune

@@ -0,0 +1,3 @@
+(library
+ (name otherlib)
+ (public_name other-lib))

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/dune-project

@@ -0,0 +1 @@
+(lang dune 3.2)

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/OtherLib/foo.ml

@@ -0,0 +1 @@
+let hello = "world"

test/blackbox-tests/test-cases/coq/compose-coq-projects.t/dune-workspace

@@ -0,0 +1 @@
+(lang dune 3.2)

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

@@ -0,0 +1,9 @@
+Testing composition of theories accross a dune workspace
+
+  $ dune build --root B
+  Entering directory 'B'
+  File "dune", line 4, characters 11-12:
+  4 |  (theories A))
+                 ^
+  Error: Theory A not found
+  [1]

test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t

@@ -1,12 +1,80 @@
-  $ dune build --debug-dependency-path
-  File "b/dune", line 4, characters 11-12:
-  4 |  (theories a))
-                 ^
-  Error: Theory a not found
-  -> required by _build/default/b/b.v.d
-  -> required by _build/default/b/b.vo
-  -> required by _build/install/default/lib/coq/user-contrib/b/b.vo
-  -> required by _build/default/cvendor.install
-  -> required by %{read:cvendor.install} at dune:3
-  -> required by alias default in dune:1
-  [1]
+  $ tree
+  .
+  |-- b
+  |   |-- b.v -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/b.v
+  |   `-- dune -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/dune
+  |-- cvendor.opam -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/cvendor.opam
+  |-- dune -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune
+  |-- dune-project -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project
+  `-- vendor
+      |-- a
+      |   |-- a.v -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/a.v
+      |   `-- dune -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/dune
+      |-- cvendor2.opam -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/cvendor2.opam
+      `-- dune-project -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project
+
+  3 directories, 9 files
+
+
+  $ dune build --debug-dependency-path --debug-backtrace
+  ** resolving parent
+  lib: [
+    "_build/install/default/lib/cvendor/META"
+    "_build/install/default/lib/cvendor/dune-package"
+    "_build/install/default/lib/cvendor/opam"
+  ]
+  lib_root: [
+    "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"}
+    "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"}
+  ]
+
+  $ tree
+  .
+  |-- _build
+  |   |-- default
+  |   |   |-- META.cvendor
+  |   |   |-- b
+  |   |   |   |-- b.glob
+  |   |   |   |-- b.v
+  |   |   |   |-- b.v.d
+  |   |   |   |-- b.vo
+  |   |   |   |-- b.vok
+  |   |   |   `-- b.vos
+  |   |   |-- cvendor.dune-package
+  |   |   |-- cvendor.install
+  |   |   |-- cvendor.opam
+  |   |   `-- vendor
+  |   |       `-- a
+  |   |           |-- a.glob
+  |   |           |-- a.v
+  |   |           |-- a.v.d
+  |   |           |-- a.vo
+  |   |           |-- a.vok
+  |   |           `-- a.vos
+  |   |-- install
+  |   |   `-- default
+  |   |       `-- lib
+  |   |           |-- coq
+  |   |           |   `-- user-contrib
+  |   |           |       `-- b
+  |   |           |           |-- b.v -> ../../../../../../default/b/b.v
+  |   |           |           `-- b.vo -> ../../../../../../default/b/b.vo
+  |   |           `-- cvendor
+  |   |               |-- META -> ../../../../default/META.cvendor
+  |   |               |-- dune-package -> ../../../../default/cvendor.dune-package
+  |   |               `-- opam -> ../../../../default/cvendor.opam
+  |   `-- log
+  |-- b
+  |   |-- b.v -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/b.v
+  |   `-- dune -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/b/dune
+  |-- cvendor.opam -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/cvendor.opam
+  |-- dune -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune
+  |-- dune-project -> ../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/dune-project
+  `-- vendor
+      |-- a
+      |   |-- a.v -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/a.v
+      |   `-- dune -> ../../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/a/dune
+      |-- cvendor2.opam -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/cvendor2.opam
+      `-- dune-project -> ../../../../../../../../../default/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/vendor/dune-project
+
+  15 directories, 31 files