Add preliminary support for Rocq's packaging support

doc/rocq.rst

@@ -44,7 +44,7 @@ example, adding
 
 .. code:: dune
 
-    (using rocq 0.14)
+    (using rocq 0.15)
 
 to a :doc:`/reference/dune-project/index` file enables using the
 ``rocq.theory`` stanza and other ``rocq.*`` stanzas. See the :ref:`Dune Rocq
@@ -62,12 +62,14 @@ The Rocq theory stanza is very similar in form to the OCaml
 
     (rocq.theory
      (name <module_prefix>)
+     (public_name <findlib_package>)
      (package <package>)
      (synopsis <text>)
      (modules <ordered_set_lang>)
      (plugins <ocaml_plugins>)
      (flags <rocq_flags>)
      (modules_flags <flags_map>)
+     (legacy_install)
      (generate_project_file)
      (rocqdep_flags <rocqdep_flags>)
      (rocqdoc_flags <rocqdoc_flags>)
@@ -110,13 +112,28 @@ The semantics of the fields are:
   the theory, similar to its OCaml counterpart. Modules are specified in Rocq
   notation. That is to say, ``A/b.v`` is written ``A.b`` in this field.
 
+- If the ``public_name`` field is present, Dune exposes the theory as the
+  Findlib package ``<findlib_package>``. The ``name`` field still gives the Rocq
+  logical path, while ``public_name`` is the package name used by downstream
+  ``(theories ...)`` dependencies and Rocq's ``-package`` option.
+
+  .. versionadded:: 3.25
+
 - If the ``package`` field is present, Dune generates install rules for the
   ``.vo`` files of the theory. ``pkg_name`` must be a valid package name.
+  Starting with :ref:`Rocq lang 0.15<rocq-lang>`, ``public_name`` subsumes
+  ``package`` in the same spirit as OCaml libraries: it determines the package
+  the public theory belongs to, but ``package`` may still be kept for migration.
 
-  Note that :ref:`Rocq lang 1.0<rocq-lang-1.0>` uses the Rocq install
-  setup, where all packages share a common root namespace and install
-  directory, ``lib/rocq/user-contrib/<module_prefix>``, as is
-  customary in the Make-based Rocq package ecosystem.
+  With ``public_name``, Dune installs theory files in the new Rocq Findlib
+  layout, under the public package directory's ``rocq.d`` subdirectory, and
+  emits META metadata including the theory's ``rocqpath``. Without
+  ``public_name``, Dune keeps the legacy ``coq/user-contrib/<module_prefix>``
+  layout.
+
+- ``legacy_install`` additionally installs a ``public_name`` theory using the
+  legacy ``coq/user-contrib/<module_prefix>`` layout. This is intended for
+  migration and is available since Rocq lang 0.15.
 
   For compatibility, Dune also installs, under the ``user-contrib`` prefix, the
   ``.cmxs`` files that appear in ``<ocaml_plugins>``. This will be dropped in
@@ -184,8 +201,15 @@ The semantics of the fields are:
 
 - Your Rocq theory can depend on other theories --- globally installed or defined
   in the current workspace --- by adding the theories names to the
-  ``<rocq_theories>`` field. Then, Dune will ensure that the depended theories
-  are present and correctly registered with Rocq.
+  ``<rocq_theories>`` field. In Rocq lang 0.15 and later these names are
+  Findlib package names. If such a package is provided by a theory in the
+  workspace, Dune uses its internal dependency graph and passes explicit ``-Q``
+  and ``-I`` flags as before. Otherwise, Dune passes ``-package <pkg>`` to Rocq,
+  letting Rocq Findlib metadata provide the transitive load path.
+
+  In earlier Rocq language versions, ``<rocq_theories>`` remains a list of Rocq
+  logical paths for backwards compatibility. Then, Dune will ensure that the
+  depended theories are present and correctly registered with Rocq.
 
   See :ref:`Locating Theories<rocq-locating-theories>` for more information on how
   Rocq theories are located by Dune.
@@ -345,8 +369,10 @@ A private theory may depend on both private and public theories; however, a
 public theory may only depend on other public theories.
 
 By default, all :ref:`rocq-theory` stanzas are considered private by Dune. In
-order to make a private theory into a public theory, the ``(package )`` field
-must be specified.
+order to make a private theory into a public theory, either the ``(package )``
+field or the ``(public_name )`` field must be specified. For new Rocq projects,
+``public_name`` is preferred because it gives the Findlib package name used by
+Rocq's ``-package`` option.
 
 .. code:: dune
 
@@ -385,7 +411,7 @@ The Rocq lang can be modified by adding the following to a
 
 .. code:: dune
 
-    (using rocq 0.14)
+    (using rocq 0.15)
 
 The supported Rocq language versions (not the version of Rocq) are:
 
@@ -399,15 +425,19 @@ The supported Rocq language versions (not the version of Rocq) are:
 - ``0.12``: Support for output tests.
 - ``0.13``: ``rocq.extraction`` now uses ``extracted_files`` instead of
   ``extracted_modules``, supporting extraction to languages other than OCaml.
-- ``0.14``: ``(stdlib ...)`` was replaced by ``(no_corelib)``. 
+- ``0.14``: ``(stdlib ...)`` was replaced by ``(no_corelib)``.
+- ``0.15``: ``rocq.theory`` supports ``public_name`` and the Rocq Findlib
+  installation layout. The ``theories`` field is interpreted as Findlib package
+  names, and ``legacy_install`` can be used to additionally install under
+  ``coq/user-contrib``.
 
 .. _rocq-lang-1.0:
 
 Rocq Language Version 1.0
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Guarantees with respect to stability are not yet provided, but we
-intend that the ``(0.14)`` version of the language becomes ``1.0``.
+intend that the ``(0.15)`` version of the language becomes ``1.0``.
 The ``1.0`` version of Rocq lang will commit to a stable set of
 functionality. All the features below are expected to reach ``1.0``
 unchanged or minimally modified.

src/dune_rules/gen_meta.ml

@@ -44,6 +44,7 @@ let ppx_runtime_deps ?(preds = []) pkgs =
 
 let description s = rule "description" [] Set s
 let directory s = rule "directory" [] Set s
+let rocqpath s = rule "rocqpath" [] Set s
 let archive preds s = rule "archive" preds Set s
 let plugin preds s = rule "plugin" preds Set s
 
@@ -173,7 +174,19 @@ let gen_lib pub_name lib ~version =
     ]
 ;;
 
-let gen ~(package : Package.t) ~add_directory_entry entries =
+type rocq_theory =
+  { public_name : Lib_name.t
+  ; rocqpath : string
+  ; deps : Lib_name.Set.t
+  ; synopsis : string option
+  }
+
+let gen_rocq_theory ~version { public_name = _; rocqpath = path; deps; synopsis } =
+  let desc = Option.value synopsis ~default:"" in
+  version @ [ description desc; rocqpath path; requires deps ]
+;;
+
+let gen ?(rocq_theories = []) ~(package : Package.t) ~add_directory_entry entries =
   let open Action_builder.O in
   let version =
     match Package.version package with
@@ -220,6 +233,11 @@ let gen ~(package : Package.t) ~add_directory_entry entries =
           ( Pub_name.of_lib_name (Public_lib.name old_public_name)
           , version @ [ requires deps; exports deps ] ))
   in
+  let pkgs =
+    pkgs
+    @ List.map rocq_theories ~f:(fun theory ->
+      Pub_name.of_lib_name theory.public_name, gen_rocq_theory ~version theory)
+  in
   let pkgs =
     List.map pkgs ~f:(fun (pn, meta) ->
       match Pub_name.to_list pn with

src/dune_rules/gen_meta.mli

@@ -4,9 +4,17 @@ open Import
 
 val requires : ?preds:Meta.predicate list -> Lib_name.Set.t -> Meta.entry
 
+type rocq_theory =
+  { public_name : Lib_name.t
+  ; rocqpath : string
+  ; deps : Lib_name.Set.t
+  ; synopsis : string option
+  }
+
 (** Generate the meta for a package containing some libraries *)
 val gen
-  :  package:Package.t
+  :  ?rocq_theories:rocq_theory list
+  -> package:Package.t
   -> add_directory_entry:bool
   -> Scope.DB.Lib_entry.t list
   -> Meta.t Action_builder.t

src/dune_rules/gen_rules.ml

@@ -798,6 +798,8 @@ let gen_rules ctx ~dir components =
       Bin_layout.gen_rules (Context_name.of_string ctx) ~dir rest |> Memo.return
     | ctx :: ".packages" :: rest ->
       Install_layout.gen_rules (Context_name.of_string ctx) ~dir rest
+    | ctx :: ".packages-rocq" :: rest ->
+      Install_layout.For_rocq_only.gen_rules (Context_name.of_string ctx) ~dir rest
     | ctx :: _ ->
       let ctx = Context_name.of_string ctx in
       with_context ctx ~f:(fun sctx ->

src/dune_rules/install_layout.ml

@@ -44,12 +44,22 @@ let dir ~context ~key =
   Path.Build.L.relative (Install.Context.dir ~context) [ ".packages"; key ]
 ;;
 
+let rocq_dir ~context ~key =
+  Path.Build.L.relative (Install.Context.dir ~context) [ ".packages-rocq"; key ]
+;;
+
 (* Resolve the package set's install entries against the layout root: filter
    out [Source_tree] entries, expand the rest, and key each entry by its
    materialised path under the layout. Collisions (two packages installing
    to the same destination, which can only happen in _root sections) are
    reported as user errors naming the conflicting packages and entry. *)
-let compute_entries context_name root packages =
+let hidden_from_rocq_plugin_layout (entry : Install.Entry.Unexpanded.t) =
+  let dst = Install.Entry.Dst.to_string entry.dst in
+  let components = String.split dst ~on:'/' in
+  Section.equal entry.section Lib_root || List.mem components "rocq.d" ~equal:String.equal
+;;
+
+let compute_entries ?(filter_entry = Fun.const true) context_name root packages =
   let open Memo.O in
   let get_entries = Fdecl.get entry_resolver_fdecl in
   Package.Name.Set.to_list packages
@@ -64,17 +74,20 @@ let compute_entries context_name root packages =
       match entry.kind with
       | Install.Entry.Unexpanded.Source_tree -> None
       | File | Directory ->
-        let relative =
-          Install.Entry.relative_installed_path entry ~paths:install_paths
-          |> Path.as_in_source_tree_exn
-        in
-        let dst = Path.Build.append_source root relative in
-        let expanded =
-          Install.Entry.Expanded.set_src
-            (Install.Entry.Unexpanded.expand entry)
-            (Path.build entry.src)
-        in
-        Some (dst, (pkg, expanded))))
+        if not (filter_entry entry)
+        then None
+        else (
+          let relative =
+            Install.Entry.relative_installed_path entry ~paths:install_paths
+            |> Path.as_in_source_tree_exn
+          in
+          let dst = Path.Build.append_source root relative in
+          let expanded =
+            Install.Entry.Expanded.set_src
+              (Install.Entry.Unexpanded.expand entry)
+              (Path.build entry.src)
+          in
+          Some (dst, (pkg, expanded)))))
   >>| List.concat
   >>| Path.Build.Map.of_list
   >>| function
@@ -122,6 +135,28 @@ let files context_name packages =
   Path.Build.Map.keys entries |> List.map ~f:Path.build
 ;;
 
+let rocq_entries =
+  let set_hash s = List.hash Package.Name.hash (Package.Name.Set.to_list s) in
+  let memo =
+    Memo.create
+      "install-layout-rocq-entries"
+      ~input:
+        (module struct
+          type t = Context_name.t * Package.Name.Set.t
+
+          let equal = Tuple.T2.equal Context_name.equal Package.Name.Set.equal
+          let hash = Tuple.T2.hash Context_name.hash set_hash
+          let to_dyn = Tuple.T2.to_dyn Context_name.to_dyn Package.Name.Set.to_dyn
+        end)
+      (fun (context, packages) ->
+         let key = Key.encode packages in
+         let root = rocq_dir ~context ~key in
+         let filter_entry entry = not (hidden_from_rocq_plugin_layout entry) in
+         compute_entries ~filter_entry context root packages)
+  in
+  fun context packages -> Memo.exec memo (context, packages)
+;;
+
 let deps context_name packages =
   let open Action_builder.O in
   let* files = Action_builder.of_memo (files context_name packages) in
@@ -147,7 +182,7 @@ let make_dispatch ~dir ~directory_targets subdirs f =
     rules
 ;;
 
-let gen_rules context_name ~dir rest =
+let gen_rules_for_entries context_name ~dir rest ~entries:entries_of =
   let open Memo.O in
   match rest with
   | [] ->
@@ -161,12 +196,14 @@ let gen_rules context_name ~dir rest =
     (match Key.decode key with
      | None -> Memo.return Build_config.Gen_rules.no_rules
      | Some packages ->
-       let+ entries = entries context_name packages in
+       let+ entries = entries_of context_name packages in
        let directory_targets =
-         Path.Build.Map.filter_map entries ~f:(fun entry ->
+         let f (entry : Path.t Install.Entry.Expanded.t) =
            match (entry.kind : Install.Entry.Expanded.kind) with
            | File -> None
-           | Directory -> Some Loc.none)
+           | Directory -> Some Loc.none
+         in
+         Path.Build.Map.filter_map entries ~f
        in
        make_dispatch ~dir ~directory_targets Subdir_set.empty (fun () ->
          Path.Build.Map.to_seq entries
@@ -182,29 +219,33 @@ let gen_rules context_name ~dir rest =
     @@ Build_config.Gen_rules.redirect_to_parent Build_config.Gen_rules.Rules.empty
 ;;
 
+let gen_rules context_name ~dir rest =
+  gen_rules_for_entries context_name ~dir rest ~entries
+;;
+
 module For_rocq_only = struct
-  (* Rocq puts the layout's [lib] dir on [OCAMLPATH], where findlib walks
-     eagerly. For a race-free, deterministic walk, every entry findlib could
-     see must be a declared dep. Bulk {!env} doesn't work: it also pulls in
-     {!Section.Lib_root} entries, which include Rocq theory [.vo] files under
-     [lib/coq/user-contrib/...]; in the same-package theory-plus-plugin case,
-     that creates a build cycle (the theory rule depending on its own output
-     via the layout symlink). Filtering to {!Section.Lib} excludes Lib_root
-     content (theory output) while keeping METAs, .cmxs, .cmi etc. — all
-     upstream of theory compilation. *)
+  (* Rocq puts this layout's [lib] dir on [OCAMLPATH], where findlib may walk
+     package directories eagerly. The normal package layout can also contain
+     Rocq theory outputs under [lib/<package>/rocq.d] or
+     [lib/coq/user-contrib/...]. If those theory outputs are visible while
+     compiling the same theory, rocqdep can report a dependency cycle through
+     the theory's own installed [.glob] symlink. Use a Rocq-specific filtered
+     layout: METAs and OCaml plugin files are visible, but [lib_root] entries
+     and [rocq.d] theory outputs are not. *)
   let lib_root context_name packages =
     let open Action_builder.O in
     let* lib_paths =
-      Action_builder.of_memo (entries context_name packages)
-      >>| Path.Build.Map.foldi
-            ~init:[]
-            ~f:(fun dst (entry : Path.t Install.Entry.Expanded.t) acc ->
-              match (entry.section : Section.t) with
-              | Lib -> Path.build dst :: acc
-              | _ -> acc)
+      Action_builder.of_memo (rocq_entries context_name packages)
+      >>| Path.Build.Map.keys
+      >>| List.map ~f:Path.build
     in
     let+ () = Action_builder.paths lib_paths in
-    let layout_root = root context_name packages in
+    let key = Key.encode packages in
+    let layout_root = rocq_dir ~context:context_name ~key in
     (Install.Roots.opam_from_prefix layout_root ~relative:Path.Build.relative).lib_root
   ;;
+
+  let gen_rules context_name ~dir rest =
+    gen_rules_for_entries context_name ~dir rest ~entries:rocq_entries
+  ;;
 end

src/dune_rules/install_layout.mli

@@ -29,7 +29,16 @@ module For_rocq_only : sig
   (** DO NOT USE!!
 
       Returns the layout's [lib] root (suitable for prepending to
-      [OCAMLPATH]) and registers the action's dependency on every
-      {!Section.Lib} entry the layout produces for the set. *)
+      [OCAMLPATH]) and registers the action's dependency on every entry the
+      filtered layout produces for the set. The filtered layout exposes OCaml
+      plugin files and META files, but not [lib_root] entries or Rocq theory
+      outputs. *)
   val lib_root : Context_name.t -> Package.Name.Set.t -> Path.Build.t Action_builder.t
+
+  (** Engine dispatch for [_build/install/<context>/.packages-rocq/<rest>]. *)
+  val gen_rules
+    :  Context_name.t
+    -> dir:Path.Build.t
+    -> string list
+    -> Build_config.Gen_rules.result Memo.t
 end