[rocq] Support for installation of package metadata.

We now install a `rocq-package` file for each Rocq theory. This way,
when Rocq developments build with Dune are globally installed, we can
find out additional metadata, such as the list of their dependencies.

Fixes #11012 fixes #11483

TODO:

- update changelog
- update documentation
- rebase on top of (lang rocq 0.1)

Co-authored-by: Li-yao Xia <[email protected]>

Author: ejgallego

src/dune_rules/coq/coq_lib.ml

@@ -73,17 +73,19 @@ and Dune : sig
     ; 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
+    ; src_root : (Path.Build.t, Path.t list) Either.t
+      (* Right: list of source files *)
+    ; obj_root : (Path.Build.t, Path.t) Either.t
+      (* Left: local library. Right: installed library. *)
     ; theories : (Loc.t * R.t) list Resolve.t
     ; libraries : (Loc.t * Lib.t) list Resolve.t
     ; theories_closure : R.t list Resolve.t Lazy.t
-    ; package : Package.t option
+    ; package : [ `Private | `Local of Package.t | `Dependency ]
     }
 
   val to_dyn : t -> Dyn.t
-  val src_root : t -> Path.Build.t
-  val obj_root : t -> Path.Build.t
+  val src_root : t -> (Path.Build.t, Path.t list) Either.t
+  val obj_root : t -> (Path.Build.t, Path.t) Either.t
   val implicit : t -> bool
 
   (** ML libraries *)
@@ -96,12 +98,14 @@ end = struct
     ; 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
+    ; src_root : (Path.Build.t, Path.t list) Either.t
+      (* Right: list of source files *)
+    ; obj_root : (Path.Build.t, Path.t) Either.t
+      (* Left: local library. Right: installed library. *)
     ; theories : (Loc.t * R.t) list Resolve.t
     ; libraries : (Loc.t * Lib.t) list Resolve.t
     ; theories_closure : R.t list Resolve.t Lazy.t
-    ; package : Package.t option
+    ; package : [ `Private | `Local of Package.t | `Dependency ]
     }
 
   let to_dyn
@@ -125,14 +129,14 @@ end = struct
         ; "id", Id.to_dyn id
         ; "implicit", Bool.to_dyn implicit
         ; "use_stdlib", Bool.to_dyn use_stdlib
-        ; "src_root", Path.Build.to_dyn src_root
-        ; "obj_root", Path.Build.to_dyn obj_root
+        ; "src_root", Either.to_dyn Path.Build.to_dyn (list Path.to_dyn) src_root
+        ; "obj_root", Either.to_dyn Path.Build.to_dyn Path.to_dyn obj_root
         ; "theories", Resolve.to_dyn (Dyn.list (Dyn.pair Loc.to_dyn R.to_dyn)) theories
         ; ( "libraries"
           , Resolve.to_dyn (Dyn.list (Dyn.pair Loc.to_dyn Lib.to_dyn)) libraries )
         ; ( "theories_closure"
           , Resolve.to_dyn (Dyn.list R.to_dyn) (Lazy.force theories_closure) )
-        ; "package", Dyn.option Package.to_dyn package
+        ; "package", match package with `Private -> Dyn.variant "Private" [] | `Local pkg -> Dyn.variant "Local" [Package.to_dyn pkg] | `Dependency -> Dyn.variant "Dependency" []
         ])
   ;;
 
@@ -202,7 +206,7 @@ let name = function
 ;;
 
 let obj_root = function
-  | Dune t -> Dune.obj_root t |> Path.build
+  | Dune t -> Dune.obj_root t |> Either.map ~l:Path.build ~r:Fun.id
   | Legacy t -> Legacy.installed_root t
 ;;
 
@@ -361,11 +365,13 @@ module DB = struct
   module rec R : sig
     val resolve_boot
       :  t
+      -> db:Lib.DB.t
       -> coq_lang_version:Dune_sexp.Syntax.Version.t
       -> (Loc.t * lib) option Resolve.Memo.t
 
     val resolve
       :  t
+      -> db:Lib.DB.t
       -> coq_lang_version:Dune_sexp.Syntax.Version.t
       -> Loc.t * Coq_lib_name.t
       -> lib Resolve.Memo.t
@@ -423,91 +429,103 @@ module DB = struct
       else theories
     ;;
 
-    let resolve_boot ~coq_lang_version ~coq_db (boot_id : Id.t option) =
+    let resolve_boot ~db ~coq_lang_version ~coq_db (boot_id : Id.t option) =
       match boot_id with
       | Some boot_id ->
         let open Resolve.Memo.O in
-        let+ lib = resolve ~coq_lang_version coq_db (boot_id.loc, boot_id.name) in
+        let+ lib = resolve ~db ~coq_lang_version coq_db (boot_id.loc, boot_id.name) in
         Some (boot_id.loc, lib)
       | None -> Resolve.Memo.return None
     ;;
 
     let resolve_theory
+          ~db
           ~coq_lang_version
           ~allow_private_deps
           ~coq_db
           ~boot_id
           (loc, theory_name)
       =
       let open Resolve.Memo.O in
-      let* theory = resolve ~coq_lang_version coq_db (loc, theory_name) in
+      let* theory = resolve ~db ~coq_lang_version coq_db (loc, theory_name) in
       let* () = Resolve.Memo.lift @@ check_boot ~boot_id theory in
       let+ () =
         if allow_private_deps
         then Resolve.Memo.return ()
         else (
           match theory with
-          | Dune { package = None; _ } -> Error.private_deps_not_allowed ~loc theory_name
+          | Dune { package = `Private; _ } -> Error.private_deps_not_allowed ~loc theory_name
           | Legacy _ | Dune _ -> Resolve.Memo.return ())
       in
       loc, theory
     ;;
 
-    let resolve_theories ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id theories =
-      let f = resolve_theory ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id in
+    let resolve_theories ~db ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id theories =
+      let f = resolve_theory ~db ~coq_lang_version ~allow_private_deps ~coq_db ~boot_id in
       Resolve.Memo.List.map theories ~f
     ;;
 
-    let create_from_stanza_impl (coq_db, db, dir, (s : Coq_stanza.Theory.t)) =
+    let create_from_coq_package_impl (coq_db, db, (s : (Path.Build.t * Coq_stanza.Theory.t, Coq_package.t) Either.t)) =
+      let of_package = function
+        | None -> `Private
+        | Some pkg -> `Local pkg
+      in
+      let path, package, s = match s with
+        | Left ((dir, s)) -> Left dir, of_package s.package, Coq_package.of_stanza s
+        | Right p -> Right (Coq_package.path p), `Dependency, Coq_package.meta p in
       let name = s.name in
-      let id = Id.create ~path:(Path.build dir) ~name in
-      let coq_lang_version = s.buildable.coq_lang_version in
+      let id = Id.create ~path:(Either.map ~l:Path.build ~r:Fun.id path) ~name in
+      let coq_lang_version = s.coq_lang_version in
       let open Memo.O in
       let boot_id = if s.boot then None else boot_library_id coq_db in
-      let allow_private_deps = Option.is_none s.package in
-      let use_stdlib = s.buildable.use_stdlib in
+      let allow_private_deps = match package with `Private -> true | _ -> false in
+      let use_stdlib = s.use_stdlib in
       let+ libraries =
-        resolve_plugins ~db ~allow_private_deps ~name:(snd name) s.buildable.plugins
+        resolve_plugins ~db ~allow_private_deps ~name:(snd name) s.plugins
       and+ theories =
         resolve_theories
+          ~db
           ~coq_db
           ~coq_lang_version
           ~allow_private_deps
           ~boot_id
-          s.buildable.theories
-      and+ boot = resolve_boot ~coq_lang_version ~coq_db boot_id in
+          s.theories
+      and+ boot = resolve_boot ~db ~coq_lang_version ~coq_db boot_id in
       let theories = maybe_add_boot ~boot ~use_stdlib ~is_boot:s.boot 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
-      { Dune.loc = s.buildable.loc
+      let src_root = Either.map ~l:(fun dir -> Left dir) ~r:(fun _path -> Right []) path in
+      { Dune.loc = s.loc
       ; boot_id
       ; id
       ; use_stdlib
       ; implicit = s.boot
-      ; obj_root = dir
-      ; src_root = dir
+      ; obj_root = path
+      ; src_root
       ; theories
       ; libraries
       ; theories_closure =
           lazy
             (Resolve.bind theories ~f:(fun theories ->
                List.map theories ~f:snd |> top_closure))
-      ; package = s.package
+      ; package
       }
     ;;
 
     module Input = struct
-      type nonrec t = t * Lib.DB.t * Path.Build.t * Coq_stanza.Theory.t
+      type nonrec t = t * Lib.DB.t * (Path.Build.t * Coq_stanza.Theory.t, Coq_package.t) Either.t
 
-      let equal (coq_db, ml_db, path, stanza) (coq_db', ml_db', path', stanza') =
+      let equal (coq_db, ml_db, s) (coq_db', ml_db', s') =
         phys_equal coq_db coq_db'
         && phys_equal ml_db ml_db'
-        && Path.Build.equal path path'
-        && phys_equal stanza stanza'
+        && match (s, s') with
+        | Left ((path, s)), Left ((path', s')) -> Path.Build.equal path path' && phys_equal s s'
+        | Right s, Right s' -> phys_equal s s'
+        | _, _ -> false
       ;;
 
       let hash = Poly.hash
@@ -517,27 +535,41 @@ module DB = struct
     let memo =
       Memo.create
         "create-from-stanza"
-        ~human_readable_description:(fun (_, _, path, theory) ->
-          Id.pp (Id.create ~path:(Path.build path) ~name:theory.name))
+        ~human_readable_description:(fun (_, _, theory) ->
+          let (path, name) = match theory with
+            | Left (dir, stanza) -> Path.build dir, stanza.name
+            | Right p -> (Coq_package.path p), (Coq_package.meta p).name in
+          Id.pp (Id.create ~path ~name))
         ~input:(module Input)
-        create_from_stanza_impl
+        create_from_coq_package_impl
     ;;
 
-    let create_from_stanza coq_db db dir stanza = Memo.exec memo (coq_db, db, dir, stanza)
+    let create_from_coq_package coq_db ~db pkg =
+      Memo.exec memo (coq_db, db, Right pkg)
+
+    let create_from_stanza coq_db db dir stanza = Memo.exec memo (coq_db, db, Left ((dir, stanza)))
 
     (* XXX: Memoize? This is pretty cheap so not sure worth the cost,
        still called too much I have observed, suspicious! *)
-    let create_from_coqpath ~boot_id cp =
+    let create_from_coqpath_legacy ~boot_id cp =
       let name = Coq_path.name cp in
       let installed_root = Coq_path.path cp in
       let implicit = Coq_path.stdlib cp in
-      let cmxs_directories = Coq_path.cmxs_directories cp in
+      let cmxs_directories = Coq_path.cmxs_directories_legacy cp in
       let vo = Coq_path.vo cp in
       let id = Id.create ~path:installed_root ~name:(Loc.none, name) in
       Resolve.Memo.return
-        { Legacy.boot_id; id; implicit; installed_root; vo; cmxs_directories }
+        (Legacy { Legacy.boot_id; id; implicit; installed_root; vo; cmxs_directories })
     ;;
 
+    let create_from_coqpath coq_db ~db = function
+    | Coq_path.Coq_package pkg ->
+      Memo.map (create_from_coq_package coq_db ~db pkg) ~f:(fun dune ->
+      Resolve.return (Dune dune))
+    | Coq_path.Legacy _ as cp ->
+        let boot_id = coq_db.boot_id in
+        create_from_coqpath_legacy ~boot_id cp
+
     module Resolve_result_no_redirect = struct
       (** In our second iteration, we remove all the redirects *)
       type t =
@@ -582,7 +614,7 @@ module DB = struct
 
     (** Our final final resolve is used externally, and should return the
         library data found from the previous iterations. *)
-    let resolve coq_db ~coq_lang_version (loc, name) =
+    let resolve coq_db ~db ~coq_lang_version (loc, name) =
       match find coq_db ~coq_lang_version name with
       | Not_found -> Error.theory_not_found ~loc name
       | Hidden reason -> Error.hidden_without_composition ~loc ~reason name
@@ -594,15 +626,12 @@ module DB = struct
         let+ (_ : (Loc.t * lib) list) = theory.theories in
         Dune theory
       | Found_path cp ->
-        let open Resolve.Memo.O in
-        let boot_id = coq_db.boot_id in
-        let+ theory = create_from_coqpath ~boot_id cp in
-        Legacy theory
+        create_from_coqpath coq_db ~db cp
     ;;
 
-    let resolve_boot coq_db ~coq_lang_version =
+    let resolve_boot coq_db ~db ~coq_lang_version =
       let boot_id = boot_library_id coq_db in
-      resolve_boot ~coq_lang_version ~coq_db boot_id
+      resolve_boot ~db ~coq_lang_version ~coq_db boot_id
     ;;
   end
 
@@ -692,8 +721,8 @@ module DB = struct
   ;;
 
   (* Resolve helpers *)
-  let find_many t theories ~coq_lang_version =
-    Resolve.Memo.List.map theories ~f:(resolve ~coq_lang_version t)
+  let find_many t theories ~db ~coq_lang_version =
+    Resolve.Memo.List.map theories ~f:(resolve ~db ~coq_lang_version t)
   ;;
 end
 

src/dune_rules/coq/coq_lib.mli

@@ -8,7 +8,7 @@ module Dune : sig
   type t
 
   (** Source directory *)
-  val src_root : t -> Path.Build.t
+  val src_root : t -> (Path.Build.t, Path.t list) Either.t
 
   (** ML libraries *)
   val libraries : t -> (Loc.t * Lib.t) list Resolve.t
@@ -80,16 +80,19 @@ module DB : sig
   val find_many
     :  t
     -> (Loc.t * Coq_lib_name.t) list
+    -> db:Lib.DB.t
     -> coq_lang_version:Dune_sexp.Syntax.Version.t
     -> lib list Resolve.Memo.t
 
   val resolve_boot
     :  t
+    -> db:Lib.DB.t
     -> coq_lang_version:Dune_sexp.Syntax.Version.t
     -> (Loc.t * lib) option Resolve.Memo.t
 
   val resolve
     :  t
+    -> db:Lib.DB.t
     -> coq_lang_version:Dune_sexp.Syntax.Version.t
     -> Loc.t * Coq_lib_name.t
     -> lib Resolve.Memo.t