From e36ee08e4d4a348d626cde53f7a63bac1309eead Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Wed, 1 Jul 2026 15:56:40 +0200 Subject: [PATCH] Add preliminary support for Rocq's packaging support. Signed-off-by: Rodolphe Lepigre --- doc/rocq.rst | 54 ++- src/dune_rules/gen_meta.ml | 20 +- src/dune_rules/gen_meta.mli | 10 +- src/dune_rules/gen_rules.ml | 2 + src/dune_rules/install_layout.ml | 107 ++++-- src/dune_rules/install_layout.mli | 13 +- src/dune_rules/install_rules.ml | 57 ++- src/dune_rules/rocq/rocq_lib.ml | 338 +++++++++++++++--- src/dune_rules/rocq/rocq_lib.mli | 13 +- src/dune_rules/rocq/rocq_lib_name.ml | 1 + src/dune_rules/rocq/rocq_lib_name.mli | 1 + src/dune_rules/rocq/rocq_rules.ml | 175 ++++++--- src/dune_rules/rocq/rocq_stanza.ml | 47 ++- src/dune_rules/rocq/rocq_stanza.mli | 12 +- .../rocq/deprecate-public_name.t/run.t | 40 ++- .../test-cases/rocq/findlib-deps.t/run.t | 51 +++ .../test-cases/rocq/findlib-layout.t/run.t | 62 ++++ .../test-cases/rocq/findlib-plugin.t/run.t | 55 +++ .../test-cases/rocq/plugin-meta.t/run.t | 4 +- 19 files changed, 888 insertions(+), 174 deletions(-) create mode 100644 test/blackbox-tests/test-cases/rocq/findlib-deps.t/run.t create mode 100644 test/blackbox-tests/test-cases/rocq/findlib-layout.t/run.t create mode 100644 test/blackbox-tests/test-cases/rocq/findlib-plugin.t/run.t diff --git a/doc/rocq.rst b/doc/rocq.rst index 768eaec95c1..27712ef8722 100644 --- a/doc/rocq.rst +++ b/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 ) + (public_name ) (package ) (synopsis ) (modules ) (plugins ) (flags ) (modules_flags ) + (legacy_install) (generate_project_file) (rocqdep_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 ````. 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`, ``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` uses the Rocq install - setup, where all packages share a common root namespace and install - directory, ``lib/rocq/user-contrib/``, 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/`` + layout. + +- ``legacy_install`` additionally installs a ``public_name`` theory using the + legacy ``coq/user-contrib/`` 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 ````. 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 - ```` field. Then, Dune will ensure that the depended theories - are present and correctly registered with Rocq. + ```` 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 `` to Rocq, + letting Rocq Findlib metadata provide the transitive load path. + + In earlier Rocq language versions, ```` 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` 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,7 +425,11 @@ 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: @@ -407,7 +437,7 @@ 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. diff --git a/src/dune_rules/gen_meta.ml b/src/dune_rules/gen_meta.ml index dc55a1e93eb..46607c6c1d1 100644 --- a/src/dune_rules/gen_meta.ml +++ b/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 diff --git a/src/dune_rules/gen_meta.mli b/src/dune_rules/gen_meta.mli index f5cd1099fab..db3f3a66ea7 100644 --- a/src/dune_rules/gen_meta.mli +++ b/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 diff --git a/src/dune_rules/gen_rules.ml b/src/dune_rules/gen_rules.ml index 340d5bad350..7e7606d4eb0 100644 --- a/src/dune_rules/gen_rules.ml +++ b/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 -> diff --git a/src/dune_rules/install_layout.ml b/src/dune_rules/install_layout.ml index 109ed8ab684..1d069184508 100644 --- a/src/dune_rules/install_layout.ml +++ b/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//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 diff --git a/src/dune_rules/install_layout.mli b/src/dune_rules/install_layout.mli index c23c006976b..9aa31b06aa5 100644 --- a/src/dune_rules/install_layout.mli +++ b/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//.packages-rocq/]. *) + val gen_rules + : Context_name.t + -> dir:Path.Build.t + -> string list + -> Build_config.Gen_rules.result Memo.t end diff --git a/src/dune_rules/install_rules.ml b/src/dune_rules/install_rules.ml index e087841352c..7fcec034441 100644 --- a/src/dune_rules/install_rules.ml +++ b/src/dune_rules/install_rules.ml @@ -998,8 +998,63 @@ end = struct Super_context.add_rule sctx ~dir:ctx.build_dir action ;; + let rocq_meta_theories sctx (pkg : Package.t) = + let ctx = Super_context.context sctx |> Context.build_context in + let pkg_name = Package.name pkg in + let* stanzas = Dune_load.dune_files ctx.name in + let public_theories = + Dune_file.fold_static_stanzas stanzas ~init:[] ~f:(fun _dune_file stanza acc -> + match Stanza.repr stanza with + | Rocq_stanza.Theory.T { public_name = Some public_name; name; _ } -> + (snd name, Public_lib.name public_name) :: acc + | _ -> acc) + in + let public_names = List.map public_theories ~f:snd |> Lib_name.Set.of_list in + let logical_to_public = Rocq_lib_name.Map.of_list_multi public_theories in + let theory_dep package = + if Lib_name.Set.mem public_names package + then package + else ( + let logical = Rocq_lib_name.of_string (Lib_name.to_string package) in + match Rocq_lib_name.Map.find logical_to_public logical with + | Some [ public_name ] -> public_name + | None | Some ([] | _ :: _ :: _) -> package) + in + Dune_file.fold_static_stanzas stanzas ~init:[] ~f:(fun _dune_file stanza acc -> + match Stanza.repr stanza with + | Rocq_stanza.Theory.T + ({ public_name = Some public_name; package = Some package; buildable; _ } as + theory) + when Package.Name.equal (Package.name package) pkg_name -> + let public_name = Public_lib.name public_name in + let plugin_deps = List.map buildable.plugins ~f:snd in + let theory_deps = + List.filter_map buildable.theories ~f:(function + | Rocq_stanza.Buildable.Theory_dep.Package (_, package) -> + Some (theory_dep package) + | Rocq_stanza.Buildable.Theory_dep.Logical _ -> None) + in + let deps = + plugin_deps @ theory_deps + |> Lib_name.Set.of_list + |> fun deps -> + if buildable.use_corelib && not theory.boot + then Lib_name.Set.add deps (Lib_name.of_string "rocq-core") + else deps + in + { Gen_meta.public_name + ; rocqpath = Rocq_lib_name.to_string (snd theory.name) + ; deps + ; synopsis = theory.synopsis + } + :: acc + | _ -> acc) + |> Memo.return + ;; + let gen_meta_file sctx (pkg : Package.t) entries = let ctx = Super_context.context sctx |> Context.build_context in + let* rocq_theories = rocq_meta_theories sctx pkg in let* () = let template = let meta_template = Path.build (Package_paths.meta_template ctx pkg) in @@ -1053,7 +1108,7 @@ end = struct (let+ template = template and+ (meta : Meta.t) = Action_builder.of_memo meta_entries - >>= Gen_meta.gen ~package:pkg ~add_directory_entry:true + >>= Gen_meta.gen ~rocq_theories ~package:pkg ~add_directory_entry:true in let pp = Pp.concat_map template ~sep:Pp.newline ~f:(fun s -> diff --git a/src/dune_rules/rocq/rocq_lib.ml b/src/dune_rules/rocq/rocq_lib.ml index c0f96602dd3..44bf6b3f14d 100644 --- a/src/dune_rules/rocq/rocq_lib.ml +++ b/src/dune_rules/rocq/rocq_lib.ml @@ -49,27 +49,25 @@ module Id = struct ;; let create ~path ~name:(loc, name) = { path; name; loc } - - module C = Comparable.Make (T) - module Top_closure = Top_closure.Make (C.Set) (Resolve) - - let top_closure ~key ~deps xs = Top_closure.top_closure ~key ~deps xs end module rec R : sig type t = | Dune of Dune.t | Legacy of Legacy.t + | Package of Findlib.t val to_dyn : t -> Dyn.t end = struct type t = | Dune of Dune.t | Legacy of Legacy.t + | Package of Findlib.t let to_dyn = function | Dune t -> Dyn.Variant ("Dune", [ Dune.to_dyn t ]) | Legacy t -> Dyn.Variant ("Legacy", [ Legacy.to_dyn t ]) + | Package t -> Dyn.Variant ("Package", [ Findlib.to_dyn t ]) ;; end @@ -85,6 +83,7 @@ and Dune : sig ; 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 + ; public_name : Lib_name.t option ; package : Package.t option } @@ -107,6 +106,7 @@ end = struct ; 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 + ; public_name : Lib_name.t option ; package : Package.t option } @@ -121,6 +121,7 @@ end = struct ; theories ; libraries ; theories_closure + ; public_name ; package } = @@ -138,6 +139,7 @@ end = struct , 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) ) + ; "public_name", Dyn.option Lib_name.to_dyn public_name ; "package", Dyn.option Package.to_dyn package ]) ;; @@ -185,31 +187,68 @@ end = struct let vo t = t.vo end +and Findlib : sig + type t = + { public_name : Lib_name.t + ; name : Rocq_lib_name.t + } + + val create : public_name:Lib_name.t -> name:Rocq_lib_name.t -> t + val corelib : t + val public_name : t -> Lib_name.t + val to_dyn : t -> Dyn.t +end = struct + type t = + { public_name : Lib_name.t + ; name : Rocq_lib_name.t + } + + let create ~public_name ~name = { public_name; name } + + let corelib = + { public_name = Lib_name.of_string "rocq-core"; name = Rocq_lib_name.corelib } + ;; + + let public_name t = t.public_name + + let to_dyn { public_name; name } = + Dyn.record + [ "public_name", Lib_name.to_dyn public_name; "name", Rocq_lib_name.to_dyn name ] + ;; +end + include R let boot_id_of_lib = function | Dune t -> t.boot_id | Legacy t -> t.boot_id -;; - -let id_of_lib = function - | Dune t -> t.id - | Legacy t -> t.id + | Package _ -> None ;; let name = function | Dune t -> t.id.name | Legacy t -> t.id.name + | Package t -> t.name ;; let obj_root = function | Dune t -> Dune.obj_root t |> Path.build | Legacy t -> Legacy.installed_root t + | Package t -> + Code_error.raise + "findlib package theories do not have a Dune-managed object root" + [ "package", Lib_name.to_dyn t.public_name ] ;; let implicit = function | Dune t -> Dune.implicit t | Legacy t -> Legacy.implicit t + | Package _ -> false +;; + +let package_name = function + | Package t -> Some t.public_name + | Dune _ | Legacy _ -> None ;; module Error = struct @@ -241,6 +280,15 @@ module Error = struct [ Pp.textf "Theory %S has not been found." name ] ;; + let ambiguous_theory_name ~loc name ids = + let name = Rocq_lib_name.to_string name in + Resolve.Memo.fail + @@ User_message.make + ~needs_stack_trace:true + ~loc + [ Pp.textf "Theory %S is ambiguous:" name; Pp.enumerate ~f:Id.pp ids ] + ;; + let private_deps_not_allowed ~loc name = let name = Rocq_lib_name.to_string name in Resolve.Memo.fail @@ -280,16 +328,45 @@ module Error = struct ;; end +module Closure_key = struct + module T = struct + type t = + | Id of Id.t + | Package of Lib_name.t + + let compare x y = + match x, y with + | Id x, Id y -> Id.compare x y + | Package x, Package y -> Lib_name.compare x y + | Id _, Package _ -> Lt + | Package _, Id _ -> Gt + ;; + + let to_dyn = function + | Id id -> Dyn.variant "Id" [ Id.to_dyn id ] + | Package package -> Dyn.variant "Package" [ Lib_name.to_dyn package ] + ;; + end + + include Comparable.Make (T) +end + +module Top_closure = Top_closure.Make (Closure_key.Set) (Resolve) + let top_closure = - let key t = id_of_lib t in + let key = function + | Dune t -> Closure_key.T.Id t.id + | Legacy t -> Closure_key.T.Id t.id + | Package t -> Closure_key.T.Package t.public_name + in let deps t = match t with | Dune t -> t.theories |> Resolve.map ~f:(List.map ~f:snd) - | Legacy _ -> Resolve.return [] + | Legacy _ | Package _ -> Resolve.return [] in fun theories -> let open Resolve.O in - Id.top_closure theories ~key ~deps + Top_closure.top_closure theories ~key ~deps >>= function | Ok s -> Resolve.return s | Error _ -> assert false @@ -305,18 +382,31 @@ module DB = struct | Redirect of 'a | Theory of Lib.DB.t * Path.Build.t * Rocq_stanza.Theory.t | Legacy_theory of Rocq_path.t + | Ambiguous of Id.t list | Not_found end type t = { parent : t option - ; resolve : Rocq_lib_name.t -> t Resolve_result.t + ; resolve_logical : Rocq_lib_name.t -> t Resolve_result.t + ; resolve_package : Lib_name.t -> t Resolve_result.t + ; package_fallback_to_logical : bool ; boot_id : Id.t option } - let rec to_dyn { parent; resolve = _; boot_id } = + let rec to_dyn + { parent + ; resolve_logical = _ + ; resolve_package = _ + ; package_fallback_to_logical + ; boot_id + } + = Dyn.record - [ "parent", Dyn.option to_dyn parent; "boot_id", Dyn.option Id.to_dyn boot_id ] + [ "parent", Dyn.option to_dyn parent + ; "package_fallback_to_logical", Dyn.bool package_fallback_to_logical + ; "boot_id", Dyn.option Id.to_dyn boot_id + ] ;; module Entry = struct @@ -337,6 +427,8 @@ module DB = struct module rec R : sig val resolve_boot : t -> (Loc.t * lib) option Resolve.Memo.t val resolve : t -> Loc.t * Rocq_lib_name.t -> lib Resolve.Memo.t + val resolve_package : t -> Loc.t * Lib_name.t -> lib Resolve.Memo.t + val resolve_dep : t -> Rocq_stanza.Buildable.Theory_dep.t -> lib Resolve.Memo.t end = struct open R @@ -400,17 +492,18 @@ module DB = struct | None -> Resolve.Memo.return None ;; - let resolve_theory ~allow_private_deps ~rocq_db ~boot_id (loc, theory_name) = + let resolve_theory ~allow_private_deps ~rocq_db ~boot_id dep = let open Resolve.Memo.O in - let* theory = resolve rocq_db (loc, theory_name) in + let loc = Rocq_stanza.Buildable.Theory_dep.loc dep in + let* theory = resolve_dep rocq_db dep 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 - | Legacy _ | Dune _ -> Resolve.Memo.return ()) + | Dune { package = None; id; _ } -> Error.private_deps_not_allowed ~loc id.name + | Legacy _ | Dune _ | Package _ -> Resolve.Memo.return ()) in loc, theory ;; @@ -427,11 +520,22 @@ module DB = struct let boot_id = if s.boot then None else boot_library_id rocq_db in let allow_private_deps = Option.is_none s.package in let use_corelib = s.buildable.use_corelib in + let use_findlib_corelib = s.buildable.rocq_lang_version >= (0, 15) in + let use_boot_id_for_corelib = + match boot_id with + | Some { Id.path; _ } -> Path.is_in_build_dir path + | None -> false + in + let public_name = Option.map s.public_name ~f:Public_lib.name in let+ libraries = resolve_plugins ~db ~allow_private_deps ~name:(snd name) s.buildable.plugins and+ theories = resolve_theories ~rocq_db ~allow_private_deps ~boot_id s.buildable.theories - and+ boot = resolve_boot ~rocq_db boot_id in + and+ boot = + if use_findlib_corelib && not use_boot_id_for_corelib + then Resolve.Memo.return (Some (Loc.none, Package Findlib.corelib)) + else resolve_boot ~rocq_db boot_id + in let theories = maybe_add_boot ~boot ~use_corelib ~is_boot:s.boot theories in let map_error x = let human_readable_description () = Id.pp id in @@ -452,6 +556,7 @@ module DB = struct lazy (Resolve.bind theories ~f:(fun theories -> List.map theories ~f:snd |> top_closure)) + ; public_name ; package = s.package } ;; @@ -499,18 +604,47 @@ module DB = struct type t = | Theory of Lib.db * Path.Build.t * Rocq_stanza.Theory.t | Legacy_theory of Rocq_path.t + | Ambiguous of Id.t list | Not_found end - let rec find rocq_db name : Resolve_result_no_redirect.t = - match rocq_db.resolve name with + let rec find_logical rocq_db name : Resolve_result_no_redirect.t = + match rocq_db.resolve_logical name with | Theory (db, dir, stanza) -> Theory (db, dir, stanza) | Legacy_theory cp -> Legacy_theory cp - | Redirect rocq_db -> find rocq_db name + | Ambiguous ids -> Ambiguous ids + | Redirect rocq_db -> find_logical rocq_db name | Not_found -> (match rocq_db.parent with | None -> Not_found - | Some parent -> find parent name) + | Some parent -> find_logical parent name) + ;; + + let rec find_package rocq_db name : Resolve_result_no_redirect.t = + let logical_fallback () : Resolve_result_no_redirect.t = + if rocq_db.package_fallback_to_logical + then ( + let logical = Rocq_lib_name.of_string (Lib_name.to_string name) in + match rocq_db.resolve_logical logical with + | Theory (db, dir, stanza) -> Theory (db, dir, stanza) + | Legacy_theory cp -> Legacy_theory cp + | Ambiguous ids -> Ambiguous ids + | Redirect rocq_db -> find_package rocq_db name + | Not_found -> Not_found) + else Not_found + in + match rocq_db.resolve_package name with + | Theory (db, dir, stanza) -> Theory (db, dir, stanza) + | Legacy_theory cp -> Legacy_theory cp + | Ambiguous ids -> Ambiguous ids + | Redirect rocq_db -> find_package rocq_db name + | Not_found -> + (match logical_fallback () with + | (Theory _ | Legacy_theory _ | Ambiguous _) as found -> found + | Not_found -> + (match rocq_db.parent with + | None -> Not_found + | Some parent -> find_package parent name)) ;; module Resolve_final_result = struct @@ -518,21 +652,54 @@ module DB = struct type t = | Found_stanza of Lib.DB.t * Path.Build.t * Rocq_stanza.Theory.t | Found_path of Rocq_path.t + | Ambiguous of Id.t list | Not_found end - let find rocq_db name : Resolve_final_result.t = - match find rocq_db name with + let find_logical rocq_db name : Resolve_final_result.t = + match find_logical rocq_db name with | Not_found -> Not_found + | Ambiguous ids -> Ambiguous ids | Theory (mldb, dir, stanza) -> Found_stanza (mldb, dir, stanza) | Legacy_theory cp -> Found_path cp ;; + let find_package rocq_db name : Resolve_final_result.t = + match find_package rocq_db name with + | Not_found -> Not_found + | Ambiguous ids -> Ambiguous ids + | Theory (mldb, dir, stanza) -> Found_stanza (mldb, dir, stanza) + | Legacy_theory cp -> Found_path cp + ;; + + let resolve_found ~rocq_db ~loc ~name_for_external = function + | Resolve_final_result.Not_found -> + let name = Rocq_lib_name.of_string (Lib_name.to_string name_for_external) in + Resolve.Memo.return + (Package (Findlib.create ~public_name:name_for_external ~name)) + | Ambiguous ids -> + let name = Rocq_lib_name.of_string (Lib_name.to_string name_for_external) in + Error.ambiguous_theory_name ~loc name ids + | Found_stanza (db, dir, stanza) -> + let open Memo.O in + let+ theory = create_from_stanza rocq_db db dir stanza in + let open Resolve.O in + let* (_ : (Loc.t * Lib.t) list) = theory.libraries in + let+ (_ : (Loc.t * lib) list) = theory.theories in + Dune theory + | Found_path cp -> + let open Resolve.Memo.O in + let boot_id = rocq_db.boot_id in + let+ theory = create_from_rocqpath ~boot_id cp in + Legacy theory + ;; + (** Our final final resolve is used externally, and should return the library data found from the previous iterations. *) let resolve rocq_db (loc, name) = - match find rocq_db name with + match find_logical rocq_db name with | Not_found -> Error.theory_not_found ~loc name + | Ambiguous ids -> Error.ambiguous_theory_name ~loc name ids | Found_stanza (db, dir, stanza) -> let open Memo.O in let+ theory = create_from_stanza rocq_db db dir stanza in @@ -547,6 +714,16 @@ module DB = struct Legacy theory ;; + let resolve_package rocq_db (loc, package) = + find_package rocq_db package + |> resolve_found ~rocq_db ~loc ~name_for_external:package + ;; + + let resolve_dep rocq_db = function + | Rocq_stanza.Buildable.Theory_dep.Logical dep -> resolve rocq_db dep + | Rocq_stanza.Buildable.Theory_dep.Package dep -> resolve_package rocq_db dep + ;; + let resolve_boot rocq_db = let boot_id = boot_library_id rocq_db in resolve_boot ~rocq_db boot_id @@ -576,34 +753,75 @@ module DB = struct (entries : (Rocq_stanza.Theory.t * Entry.t) list) = let boot_id = select_boot_id entries in - let map = - match - Rocq_lib_name.Map.of_list_map - entries - ~f:(fun ((theory : Rocq_stanza.Theory.t), entry) -> - snd theory.name, (theory, entry)) - with - | Ok m -> m - | Error (_name, (theory1, entry1), (theory2, entry2)) -> - let path entry = - match (entry : Entry.t) with - | Theory dir -> Path.build dir - | Redirect db -> - Code_error.raise "created stanza redirected to a library" [ "db", to_dyn db ] - in - let id1 = Id.create ~path:(path entry1) ~name:theory1.name in - let id2 = Id.create ~path:(path entry2) ~name:theory2.name in - Error.duplicate_theory_name id1 id2 + let id_of_entry (theory : Rocq_stanza.Theory.t) (entry : Entry.t) = + match entry with + | Theory dir -> Id.create ~path:(Path.build dir) ~name:theory.name + | Redirect db -> + Code_error.raise "created stanza redirected to a library" [ "db", to_dyn db ] in - let resolve name : t Resolve_result.t = - match Rocq_lib_name.Map.find map name with + let logical_map = + List.map entries ~f:(fun ((theory : Rocq_stanza.Theory.t), entry) -> + snd theory.name, (theory, entry)) + |> Rocq_lib_name.Map.of_list_multi + in + let (_ : (Rocq_stanza.Theory.t * Entry.t) Rocq_lib_name.Map.t) = + List.fold_left + entries + ~init:Rocq_lib_name.Map.empty + ~f:(fun seen ((theory : Rocq_stanza.Theory.t), entry) -> + let name = snd theory.name in + match Rocq_lib_name.Map.find seen name with + | None -> Rocq_lib_name.Map.set seen name (theory, entry) + | Some (prev_theory, prev_entry) -> + if Option.is_some theory.public_name && Option.is_some prev_theory.public_name + then seen + else ( + let id1 = id_of_entry theory entry in + let id2 = id_of_entry prev_theory prev_entry in + Error.duplicate_theory_name id1 id2)) + in + let package_map = + List.filter_map entries ~f:(fun ((theory : Rocq_stanza.Theory.t), entry) -> + Option.map theory.public_name ~f:(fun public_name -> + Public_lib.name public_name, (theory, entry))) + in + let package_map = + match Lib_name.Map.of_list package_map with + | Ok map -> map + | Error (public_name, (theory1, entry1), (theory2, entry2)) -> + let id1 = id_of_entry theory1 entry1 in + let id2 = id_of_entry theory2 entry2 in + User_error.raise + ~needs_stack_trace:true + [ Pp.textf + "Rocq theory public name %s is defined twice:" + (Lib_name.to_string public_name) + ; Pp.enumerate ~f:Id.pp [ id1; id2 ] + ] + in + let resolve_entry (theory, (entry : Entry.t)) : t Resolve_result.t = + match entry with + | Entry.Theory dir -> Resolve_result.Theory (find_db dir, dir, theory) + | Entry.Redirect db -> Resolve_result.Redirect db + in + let resolve_logical name : t Resolve_result.t = + match Rocq_lib_name.Map.find logical_map name with + | None -> Not_found + | Some [ entry ] -> resolve_entry entry + | Some entries -> + Ambiguous (List.map entries ~f:(fun (theory, entry) -> id_of_entry theory entry)) + in + let resolve_package name : t Resolve_result.t = + match Lib_name.Map.find package_map name with | None -> Not_found - | Some (theory, entry) -> - (match entry with - | Theory dir -> Theory (find_db dir, dir, theory) - | Redirect db -> Redirect db) + | Some entry -> resolve_entry entry in - { boot_id; resolve; parent } + { boot_id + ; resolve_logical + ; resolve_package + ; package_fallback_to_logical = true + ; parent + } ;; (* XXX: This is basically duplicated from create_from_rocqlib_stanzas @@ -630,19 +848,25 @@ module DB = struct precedence. This is in line with Rocq semantics. *) |> Rocq_lib_name.Map.of_list_reducei ~f:(fun _name _cp1 cp2 -> cp2) in - let resolve name : t Resolve_result.t = + let resolve_logical name : t Resolve_result.t = match Rocq_lib_name.Map.find map name with | None -> Not_found | Some cp -> Legacy_theory cp in - { parent; resolve; boot_id } + let resolve_package _ : t Resolve_result.t = Resolve_result.Not_found in + { parent + ; resolve_logical + ; resolve_package + ; package_fallback_to_logical = false + ; boot_id + } ;; (* Resolve helpers *) - let find_many t theories = Resolve.Memo.List.map theories ~f:(resolve t) + let find_many t theories = Resolve.Memo.List.map theories ~f:(resolve_dep t) end let theories_closure = function | Dune t -> Lazy.force t.theories_closure - | Legacy _ -> Resolve.return [] + | Legacy _ | Package _ -> Resolve.return [] ;; diff --git a/src/dune_rules/rocq/rocq_lib.mli b/src/dune_rules/rocq/rocq_lib.mli index 366439ffca9..401686df556 100644 --- a/src/dune_rules/rocq/rocq_lib.mli +++ b/src/dune_rules/rocq/rocq_lib.mli @@ -49,14 +49,23 @@ module Legacy : sig val vo : t -> Path.t list end +module Findlib : sig + type t + + val corelib : t + val public_name : t -> Lib_name.t +end + type t = | Dune of Dune.t | Legacy of Legacy.t + | Package of Findlib.t val to_dyn : t -> Dyn.t val name : t -> Rocq_lib_name.t val obj_root : t -> Path.t val implicit : t -> bool +val package_name : t -> Lib_name.t option (** Return the list of dependencies needed for compiling this library *) val theories_closure : t -> t list Resolve.t @@ -86,7 +95,9 @@ module DB : sig libraries are installed, we would infer the right amount of information. *) val create_from_rocqpaths : Rocq_path.t list -> t - val find_many : t -> (Loc.t * Rocq_lib_name.t) list -> lib list Resolve.Memo.t + val find_many : t -> Rocq_stanza.Buildable.Theory_dep.t list -> lib list Resolve.Memo.t val resolve_boot : t -> (Loc.t * lib) option Resolve.Memo.t val resolve : t -> Loc.t * Rocq_lib_name.t -> lib Resolve.Memo.t + val resolve_package : t -> Loc.t * Lib_name.t -> lib Resolve.Memo.t + val resolve_dep : t -> Rocq_stanza.Buildable.Theory_dep.t -> lib Resolve.Memo.t end diff --git a/src/dune_rules/rocq/rocq_lib_name.ml b/src/dune_rules/rocq/rocq_lib_name.ml index 86cc5e082ce..ff686e41463 100644 --- a/src/dune_rules/rocq/rocq_lib_name.ml +++ b/src/dune_rules/rocq/rocq_lib_name.ml @@ -19,6 +19,7 @@ type t = string list let compare = List.compare ~compare:String.compare let equal x y = Ordering.is_eq (compare x y) let to_string x = String.concat ~sep:"." x +let of_string s = String.split ~on:'.' s let empty = [] let corelib = [ "Corelib" ] let to_list x = x diff --git a/src/dune_rules/rocq/rocq_lib_name.mli b/src/dune_rules/rocq/rocq_lib_name.mli index c31e1bbfaea..1440809e122 100644 --- a/src/dune_rules/rocq/rocq_lib_name.mli +++ b/src/dune_rules/rocq/rocq_lib_name.mli @@ -31,6 +31,7 @@ val decode : (Loc.t * t) Dune_lang.Decoder.t (* to be removed in favor of encode / decode *) val to_string : t -> string +val of_string : string -> t (** The Rocq standard library name *) val corelib : t diff --git a/src/dune_rules/rocq/rocq_rules.ml b/src/dune_rules/rocq/rocq_rules.ml index 09f2dab9db5..3840ada36f2 100644 --- a/src/dune_rules/rocq/rocq_rules.ml +++ b/src/dune_rules/rocq/rocq_rules.ml @@ -192,10 +192,13 @@ let rocqdoc_footer ~dir ~stanza_rocqdoc_footer ~expander = ;; let theory_rocqc_flag lib = - let name = Rocq_lib_name.wrapper (Rocq_lib.name lib) in - let dir = Rocq_lib.obj_root lib in - let binding_flag = if Rocq_lib.implicit lib then "-R" else "-Q" in - Command.Args.S [ A binding_flag; Path dir; A name ] + match Rocq_lib.package_name lib with + | Some package -> Command.Args.S [ A "-package"; A (Lib_name.to_string package) ] + | None -> + let name = Rocq_lib_name.wrapper (Rocq_lib.name lib) in + let dir = Rocq_lib.obj_root lib in + let binding_flag = if Rocq_lib.implicit lib then "-R" else "-Q" in + Command.Args.S [ A binding_flag; Path dir; A name ] ;; let theories_flags ~theories_deps = @@ -215,6 +218,7 @@ module Bootstrap : sig val make : scope:Scope.t -> use_corelib:bool + -> rocq_lang_version:Dune_sexp.Syntax.Version.t -> wrapper_name:string -> Rocq_module.t -> t Resolve.Memo.t @@ -240,7 +244,7 @@ end = struct (* [Bootstrap.t] determines, for a concrete Rocq module, how Corelib is being handled. See the main modes above. *) - let make ~scope ~use_corelib ~wrapper_name rocq_module = + let make ~scope ~use_corelib ~rocq_lang_version ~wrapper_name rocq_module = let open Resolve.Memo.O in let* boot_lib = Scope.rocq_libs scope |> Resolve.Memo.lift_memo >>= Rocq_lib.DB.resolve_boot @@ -249,13 +253,25 @@ end = struct then ( match boot_lib with | None -> - Resolve.Memo.fail - (User_message.make - [ Pp.text - "Couldn't find Rocq Corelib, and the theory does not disable automatic \ - Corelib inclusion with (no_corelib)." - ]) + if rocq_lang_version >= (0, 15) + then Resolve.Memo.return (Corelib (Rocq_lib.Package Rocq_lib.Findlib.corelib)) + else + Resolve.Memo.fail + (User_message.make + [ Pp.text + "Couldn't find Rocq Corelib, and the theory does not disable \ + automatic Corelib inclusion with (no_corelib)." + ]) | Some (_loc, boot_lib) -> + let boot_lib = + if rocq_lang_version >= (0, 15) + then ( + match boot_lib with + | Rocq_lib.Dune _ -> boot_lib + | Rocq_lib.Legacy _ | Rocq_lib.Package _ -> + Rocq_lib.Package Rocq_lib.Findlib.corelib) + else boot_lib + in Resolve.Memo.return @@ (* TODO: replace with per_file flags *) @@ -302,7 +318,7 @@ let directories_of_lib ~sctx lib = let* dir_contents = Dir_contents.get sctx ~dir in let+ rocq_sources = Dir_contents.rocq dir_contents in Rocq_sources.directories rocq_sources ~name - | Rocq_lib.Legacy _ -> + | Rocq_lib.Legacy _ | Rocq_lib.Package _ -> (* TODO: we could return this if we don't restrict ourselves to Path.Build.t here. @@ -391,9 +407,11 @@ let libs_of_theory ~lib_db ~theories_deps plugins : (Lib.t list * _) Resolve.Mem let f (t : Rocq_lib.t) = match t with | Dune t -> Left t - | Legacy t -> Right t + | Legacy t -> Right (Some t) + | Package _ -> Right None in let dune_theories, legacy_theories = List.partition_map ~f theories in + let legacy_theories = List.filter_opt legacy_theories in let* dlibs = Resolve.List.concat_map ~f:Rocq_lib.Dune.libraries dune_theories |> Resolve.Memo.lift in @@ -487,6 +505,7 @@ let setup_rocqproject_for_theory_rule ~theories_deps ~wrapper_name ~use_corelib + ~rocq_lang_version ~ml_flags ~stanza_flags ~theory_dirs @@ -496,7 +515,7 @@ let setup_rocqproject_for_theory_rule let boot_type = match rocq_modules with | [] -> Resolve.Memo.return Bootstrap.empty - | m :: _ -> Bootstrap.make ~scope ~use_corelib ~wrapper_name m + | m :: _ -> Bootstrap.make ~scope ~use_corelib ~rocq_lang_version ~wrapper_name m in let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in let* args = @@ -737,6 +756,7 @@ let deps_of ~dir ~boot_type ~wrapper_name ~mode rocq_module = let prelude = "Init/Prelude.vo" in match boot_type with | Bootstrap.No_corelib -> deps + | Bootstrap.Corelib (Rocq_lib.Package _) -> deps | Bootstrap.Corelib lib -> Path.relative (Rocq_lib.obj_root lib) prelude :: deps in Action_builder.paths deps @@ -851,7 +871,9 @@ let setup_rocqc_rule rocq_module = (* Process rocqdep and generate rules *) - let boot_type = Bootstrap.make ~scope ~use_corelib ~wrapper_name rocq_module in + let boot_type = + Bootstrap.make ~scope ~use_corelib ~rocq_lang_version ~wrapper_name rocq_module + in let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in (* TODO: merge with boot_type *) let per_file_flags = Per_file.match_ modules_flags rocq_module in @@ -919,6 +941,7 @@ let rocq_modules_of_theory ~sctx lib = let name = Rocq_lib.name lib in match lib with | Rocq_lib.Legacy lib -> Memo.return @@ Rocq_lib.Legacy.vo lib + | Rocq_lib.Package _ -> Memo.return [] | Rocq_lib.Dune lib -> let dir = Rocq_lib.Dune.src_root lib in let* dir_contents = Dir_contents.get sctx ~dir in @@ -1054,10 +1077,16 @@ let setup_rocqdoc_rules ~sctx ~dir ~theories_deps (s : Rocq_stanza.Theory.t) roc ;; (* Common context for a theory, deps and rules *) -let theory_context ~context ~scope ~name buildable = +let theory_context ~context ~scope (s : Rocq_stanza.Theory.t) = + let buildable = s.buildable in let theory = let* rocq_lib_db = Scope.rocq_libs scope in - Rocq_lib.DB.resolve rocq_lib_db name + match s.public_name with + | Some public_name -> + Rocq_lib.DB.resolve_package + rocq_lib_db + (Public_lib.loc public_name, Public_lib.name public_name) + | None -> Rocq_lib.DB.resolve rocq_lib_db s.name in let theories_deps = Resolve.Memo.bind theory ~f:(fun theory -> @@ -1076,14 +1105,22 @@ let extraction_context ~context ~scope (buildable : Rocq_stanza.Buildable.t) = let rocq_lib_db = Scope.rocq_libs scope in let theories_deps = let* rocq_lib_db = rocq_lib_db in - Resolve.Memo.List.map buildable.theories ~f:(Rocq_lib.DB.resolve rocq_lib_db) + Resolve.Memo.List.map buildable.theories ~f:(Rocq_lib.DB.resolve_dep rocq_lib_db) in (* Extraction requires a boot library so we do this unconditionally for now. We must do this because it can happen that s.buildable.theories is empty *) let boot = - let* rocq_lib_db = rocq_lib_db in - Rocq_lib.DB.resolve_boot rocq_lib_db + let open Resolve.Memo.O in + let* rocq_lib_db = Resolve.Memo.lift_memo rocq_lib_db in + let* boot = Rocq_lib.DB.resolve_boot rocq_lib_db in + if buildable.rocq_lang_version >= (0, 15) + then ( + match boot with + | Some (_, Rocq_lib.Dune _) -> Resolve.Memo.return boot + | None | Some (_, (Rocq_lib.Legacy _ | Rocq_lib.Package _)) -> + Resolve.Memo.return (Some (Loc.none, Rocq_lib.Package Rocq_lib.Findlib.corelib))) + else Resolve.Memo.return boot in let theories_deps = let open Resolve.Memo.O in @@ -1102,11 +1139,10 @@ let extraction_context ~context ~scope (buildable : Rocq_stanza.Buildable.t) = let setup_theory_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) = let* scope = Scope.DB.find_by_dir dir in - let name = s.name in let rocq_lang_version = s.buildable.rocq_lang_version in let theory, theories_deps, ml_flags, plugin_ocamlpath = let context = Super_context.context sctx |> Context.name in - theory_context ~context ~scope ~name s.buildable + theory_context ~context ~scope s in let wrapper_name = Rocq_lib_name.wrapper (snd s.name) in let use_corelib = s.buildable.use_corelib in @@ -1139,7 +1175,7 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) = about -noinit as rocqdep ignores it *) match rocq_modules with | [] -> Resolve.Memo.return Bootstrap.empty - | m :: _ -> Bootstrap.make ~scope ~use_corelib ~wrapper_name m + | m :: _ -> Bootstrap.make ~scope ~use_corelib ~rocq_lang_version ~wrapper_name m in let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in (if not (snd s.generate_project_file) @@ -1153,6 +1189,7 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) = ~theories_deps ~wrapper_name ~use_corelib + ~rocq_lang_version ~ml_flags ~stanza_flags ~theory_dirs @@ -1202,16 +1239,22 @@ let setup_theory_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) = let rocqtop_args_theory ~sctx ~dir ~dir_contents (s : Rocq_stanza.Theory.t) rocq_module = let* scope = Scope.DB.find_by_dir dir in - let name = s.name in let _theory, theories_deps, ml_flags, _plugin_ocamlpath = let context = Super_context.context sctx |> Context.name in - theory_context ~context ~scope ~name s.buildable + theory_context ~context ~scope s in let wrapper_name = Rocq_lib_name.wrapper (snd s.name) in let* mode = select_native_mode ~sctx ~dir s.buildable in let name = snd s.name in let use_corelib = s.buildable.use_corelib in - let boot_type = Bootstrap.make ~scope ~use_corelib ~wrapper_name rocq_module in + let boot_type = + Bootstrap.make + ~scope + ~use_corelib + ~rocq_lang_version:s.buildable.rocq_lang_version + ~wrapper_name + rocq_module + in let* rocq_dir_contents = Dir_contents.rocq dir_contents in let theory_dirs = Rocq_sources.directories rocq_dir_contents ~name |> Path.Build.Set.of_list @@ -1253,8 +1296,7 @@ let install_rules ~sctx ~dir s = let name = snd s.name in (* This must match the wrapper prefix for now to remain compatible *) let dst_suffix = Rocq_lib_name.dir name in - (* These are the rules for now, rocq lang 2.0 will make this uniform *) - let dst_dir = + let legacy_dst_dir = if s.boot then (* We drop the "Corelib" prefix (!) *) Path.Local.of_string "coq/theories" @@ -1262,36 +1304,55 @@ let install_rules ~sctx ~dir s = let rocq_root = Path.Local.of_string "coq/user-contrib" in Path.Local.relative rocq_root dst_suffix) in + let findlib_dst_dir public_name = + let base = + match Public_lib.sub_dir public_name with + | None -> Path.Local.root + | Some sub_dir -> Path.Local.of_string sub_dir + in + Path.Local.relative base "rocq.d" + in + let layouts = + match s.public_name with + | None -> [ Section.Lib_root, legacy_dst_dir ] + | Some public_name -> + let layouts = [ Section.Lib, findlib_dst_dir public_name ] in + if s.legacy_install + then (Section.Lib_root, legacy_dst_dir) :: layouts + else layouts + in let wrapper_name = Rocq_lib_name.wrapper name in let to_path f = Path.reach ~from:(Path.build dir) (Path.build f) in - let to_dst f = Path.Local.to_string @@ Path.Local.relative dst_dir f in - let make_entry (orig_file : Path.Build.t) (dst_file : string) = + let make_entry ~section ~dst_dir (orig_file : Path.Build.t) (dst_file : string) = + let dst = Path.Local.to_string @@ Path.Local.relative dst_dir dst_file in let entry = Install.Entry.Unexpanded.make - Section.Lib_root - ~dst:(to_dst dst_file) + section + ~dst orig_file ~kind:Install.Entry.Unexpanded.File in Install.Entry.Sourced.Unexpanded.create ~loc entry in let+ rocq_sources = Dir_contents.rocq dir_contents in - rocq_sources - |> Rocq_sources.library ~name - |> List.concat_map ~f:(fun (vfile : Rocq_module.t) -> - let obj_files = - Rocq_module.obj_files - ~wrapper_name - ~mode - ~obj_dir:dir - ~obj_files_mode:Rocq_module.Install - vfile - |> List.map ~f:(fun ((vo_file : Path.Build.t), (install_vo_file : string)) -> - make_entry vo_file install_vo_file) - in - let vfile = Rocq_module.source vfile |> Path.as_in_build_dir_exn in - let vfile_dst = to_path vfile in - make_entry vfile vfile_dst :: obj_files) + let modules = Rocq_sources.library rocq_sources ~name in + List.concat_map layouts ~f:(fun (section, dst_dir) -> + modules + |> List.concat_map ~f:(fun (vfile : Rocq_module.t) -> + let make_entry = make_entry ~section ~dst_dir in + let obj_files = + Rocq_module.obj_files + ~wrapper_name + ~mode + ~obj_dir:dir + ~obj_files_mode:Rocq_module.Install + vfile + |> List.map ~f:(fun ((vo_file : Path.Build.t), (install_vo_file : string)) -> + make_entry vo_file install_vo_file) + in + let vfile = Rocq_module.source vfile |> Path.as_in_build_dir_exn in + let vfile_dst = to_path vfile in + make_entry vfile vfile_dst :: obj_files)) ;; let setup_rocqpp_rules ~sctx ~dir ({ loc; modules } : Rocq_stanza.Rocqpp.t) = @@ -1339,7 +1400,7 @@ let setup_extraction_rules ~sctx ~dir ~dir_contents (s : Rocq_stanza.Extraction. about -noinit as rocqdep ignores it *) match [ rocq_module ] with | [] -> Resolve.Memo.return Bootstrap.empty - | m :: _ -> Bootstrap.make ~scope ~use_corelib ~wrapper_name m + | m :: _ -> Bootstrap.make ~scope ~use_corelib ~rocq_lang_version ~wrapper_name m in let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in let modules_flags = None in @@ -1385,7 +1446,14 @@ let rocqtop_args_extraction ~sctx ~dir (s : Rocq_stanza.Extraction.t) rocq_modul extraction_context ~context ~scope s.buildable in let wrapper_name = extraction_wrapper_name s in - let boot_type = Bootstrap.make ~scope ~use_corelib ~wrapper_name rocq_module in + let boot_type = + Bootstrap.make + ~scope + ~use_corelib + ~rocq_lang_version:s.buildable.rocq_lang_version + ~wrapper_name + rocq_module + in let boot_flags = Resolve.Memo.read boot_type |> Action_builder.map ~f:Bootstrap.flags in let per_file_flags = None in let* mode = select_native_mode ~sctx ~dir s.buildable in @@ -1409,7 +1477,12 @@ let deps_of ~dir ~use_corelib ~wrapper_name ~mode rocq_module = let boot_type = let open Memo.O in let* scope = Scope.DB.find_by_dir dir in - Bootstrap.make ~scope ~use_corelib ~wrapper_name rocq_module + Bootstrap.make + ~scope + ~use_corelib + ~rocq_lang_version:(0, 14) + ~wrapper_name + rocq_module in deps_of ~dir ~boot_type ~wrapper_name ~mode rocq_module ;; diff --git a/src/dune_rules/rocq/rocq_stanza.ml b/src/dune_rules/rocq/rocq_stanza.ml index 07ec1a79528..3ad3244a33e 100644 --- a/src/dune_rules/rocq/rocq_stanza.ml +++ b/src/dune_rules/rocq/rocq_stanza.ml @@ -22,6 +22,7 @@ let rocq_syntax = ; (0, 12), `Since (3, 22) ; (0, 13), `Since (3, 23) ; (0, 14), `Since (3, 24) + ; (0, 15), `Since (3, 25) ] ;; @@ -50,13 +51,30 @@ module Rocqpp = struct end module Buildable = struct + module Theory_dep = struct + type t = + | Logical of (Loc.t * Rocq_lib_name.t) + | Package of (Loc.t * Lib_name.t) + + let loc = function + | Logical (loc, _) | Package (loc, _) -> loc + ;; + + let decode = + let* rocq_lang_version = get_rocq_syntax () in + if rocq_lang_version < (0, 15) + then Rocq_lib_name.decode >>| fun dep -> Logical dep + else located Lib_name.decode >>| fun dep -> Package dep + ;; + end + type t = { flags : Ordered_set_lang.Unexpanded.t ; rocq_lang_version : Dune_sexp.Syntax.Version.t ; mode : Rocq_mode.t option ; use_corelib : bool ; plugins : (Loc.t * Lib_name.t) list (** ocaml libraries *) - ; theories : (Loc.t * Rocq_lib_name.t) list (** rocq libraries *) + ; theories : Theory_dep.t list (** rocq libraries *) ; loc : Loc.t } @@ -78,7 +96,7 @@ module Buildable = struct and+ no_corelib_opt = field_o "no_corelib" (Dune_lang.Syntax.since rocq_syntax (0, 14) >>> return true) and+ plugins = field "plugins" (repeat (located Lib_name.decode)) ~default:[] - and+ theories = field "theories" (repeat Rocq_lib_name.decode) ~default:[] in + and+ theories = field "theories" (repeat Theory_dep.decode) ~default:[] in let use_corelib = if rocq_lang_version < (0, 14) then Option.value stdlib_opt ~default:true @@ -146,12 +164,14 @@ end module Theory = struct type t = { name : Loc.t * Rocq_lib_name.t + ; public_name : Public_lib.t option ; package : Package.t option ; project : Dune_project.t ; synopsis : string option ; modules : Ordered_set_lang.t ; modules_flags : (Rocq_module.Name.t * Ordered_set_lang.Unexpanded.t) list option ; boot : bool + ; legacy_install : bool ; generate_project_file : Loc.t * bool ; enabled_if : Blang.t ; buildable : Buildable.t @@ -170,7 +190,7 @@ module Theory = struct then ( match theories with | [] -> () - | (loc, _) :: _ -> boot_has_deps loc) + | dep :: _ -> boot_has_deps (Buildable.Theory_dep.loc dep)) ;; let check_generate_project_file (loc, generate_project_file) modules_flags = @@ -198,10 +218,18 @@ module Theory = struct let decode = fields (let+ name = field "name" Rocq_lib_name.decode + and+ public_name = + field_o + "public_name" + (Dune_lang.Syntax.since rocq_syntax (0, 15) + >>> Public_lib.decode ~allow_deprecated_names:false) and+ package = Stanza_pkg.field_opt () >>| Option.map ~f:snd and+ project = Dune_project.get_exn () and+ synopsis = field_o "synopsis" string and+ boot = field_b "boot" ~check:(Dune_lang.Syntax.since rocq_syntax (0, 2)) + and+ legacy_install = + located + @@ field_b "legacy_install" ~check:(Dune_lang.Syntax.since rocq_syntax (0, 15)) and+ generate_project_file = located @@ field_b "generate_project_file" and+ modules = Ordered_set_lang.field "modules" and+ modules_flags = field_o "modules_flags" Per_file.decode @@ -211,17 +239,30 @@ module Theory = struct and+ rocqdoc_flags = Ordered_set_lang.Unexpanded.field "rocqdoc_flags" and+ rocqdoc_header = field_o "rocqdoc_header" String_with_vars.decode and+ rocqdoc_footer = field_o "rocqdoc_footer" String_with_vars.decode in + let package = + match public_name with + | None -> package + | Some public_name -> Some (Public_lib.package public_name) + in + let legacy_install_loc, legacy_install = legacy_install in + if legacy_install && Option.is_none public_name + then + User_error.raise + ~loc:legacy_install_loc + [ Pp.text "legacy_install requires public_name" ]; (* boot libraries cannot depend on other theories *) check_boot_has_no_deps boot buildable; (* project files can only be generated when no per-module flags are configured. *) check_generate_project_file generate_project_file modules_flags; { name + ; public_name ; package ; project ; synopsis ; modules ; modules_flags ; boot + ; legacy_install ; generate_project_file ; buildable ; enabled_if diff --git a/src/dune_rules/rocq/rocq_stanza.mli b/src/dune_rules/rocq/rocq_stanza.mli index 197421095e4..98d67658748 100644 --- a/src/dune_rules/rocq/rocq_stanza.mli +++ b/src/dune_rules/rocq/rocq_stanza.mli @@ -14,13 +14,21 @@ open Import module Buildable : sig + module Theory_dep : sig + type t = + | Logical of (Loc.t * Rocq_lib_name.t) + | Package of (Loc.t * Lib_name.t) + + val loc : t -> Loc.t + end + type t = { flags : Ordered_set_lang.Unexpanded.t ; rocq_lang_version : Dune_sexp.Syntax.Version.t ; mode : Rocq_mode.t option ; use_corelib : bool ; plugins : (Loc.t * Lib_name.t) list (** ocaml plugins *) - ; theories : (Loc.t * Rocq_lib_name.t) list (** rocq libraries *) + ; theories : Theory_dep.t list (** rocq libraries *) ; loc : Loc.t } end @@ -40,12 +48,14 @@ end module Theory : sig type t = { name : Loc.t * Rocq_lib_name.t + ; public_name : Public_lib.t option ; package : Package.t option ; project : Dune_project.t ; synopsis : string option ; modules : Ordered_set_lang.t ; modules_flags : (Rocq_module.Name.t * Ordered_set_lang.Unexpanded.t) list option ; boot : bool + ; legacy_install : bool ; generate_project_file : Loc.t * bool ; enabled_if : Blang.t ; buildable : Buildable.t diff --git a/test/blackbox-tests/test-cases/rocq/deprecate-public_name.t/run.t b/test/blackbox-tests/test-cases/rocq/deprecate-public_name.t/run.t index 5e816c3b26e..4e6d098e990 100644 --- a/test/blackbox-tests/test-cases/rocq/deprecate-public_name.t/run.t +++ b/test/blackbox-tests/test-cases/rocq/deprecate-public_name.t/run.t @@ -1,4 +1,9 @@ -public_name field is deprecated +public_name is gated on Rocq language 0.15 + $ chmod u+w dune-project + $ cat > dune-project << EOF + > (lang dune 3.24) + > (using rocq 0.14) + > EOF $ cat > dune << EOF > (rocq.theory > (name foo) @@ -6,13 +11,21 @@ public_name field is deprecated > EOF $ dune build - File "dune", line 3, characters 2-13: + File "dune", line 3, characters 1-18: 3 | (public_name Foo)) - ^^^^^^^^^^^ - Error: Unknown field "public_name" + ^^^^^^^^^^^^^^^^^ + Error: 'public_name' is only available since version 0.15 of Rocq Prover + build language. Please update your dune-project file to have (using rocq + 0.15). [1] -both package and public_name field is an error +package and public_name are accepted together for migration; public_name chooses +the findlib package. + $ cat > dune-project << EOF + > (lang dune 3.25) + > (using rocq 0.15) + > (package (name Foo)) + > EOF $ cat > dune << EOF > (rocq.theory > (name foo) @@ -20,9 +33,18 @@ both package and public_name field is an error > (package Foo)) > EOF + $ dune build @install + +legacy_install is only meaningful for public_name theories. + $ cat > dune << EOF + > (rocq.theory + > (name foo) + > (legacy_install)) + > EOF + $ dune build - File "dune", line 3, characters 2-13: - 3 | (public_name Foo) - ^^^^^^^^^^^ - Error: Unknown field "public_name" + File "dune", line 3, characters 1-17: + 3 | (legacy_install)) + ^^^^^^^^^^^^^^^^ + Error: legacy_install requires public_name [1] diff --git a/test/blackbox-tests/test-cases/rocq/findlib-deps.t/run.t b/test/blackbox-tests/test-cases/rocq/findlib-deps.t/run.t new file mode 100644 index 00000000000..4ffb7464994 --- /dev/null +++ b/test/blackbox-tests/test-cases/rocq/findlib-deps.t/run.t @@ -0,0 +1,51 @@ +Rocq theory dependencies are package names in Rocq language 0.15. + + $ make_rocq_project 3.25 0.15 + $ cat >> dune-project << EOF + > (package (name pkg)) + > EOF + $ touch pkg.opam + +Workspace packages are resolved by Dune and passed as ordinary -Q flags. +Installed packages stay package-shaped and are passed to Rocq with -package. + + $ mkdir A B + $ cat > A/dune << EOF + > (rocq.theory + > (name A) + > (public_name pkg.a)) + > EOF + $ cat > A/a.v << EOF + > Definition x := 0. + > EOF + $ cat > B/dune << EOF + > (rocq.theory + > (name B) + > (public_name pkg.b) + > (theories pkg.a rocq-stdlib)) + > EOF + $ cat > B/b.v << EOF + > From A Require Import a. + > From Stdlib Require Import List. + > Definition y := x. + > Definition ys := map (fun x : nat => x) nil. + > EOF + +Two public theories may share a Rocq logical name when their public names do not +collide. + + $ mkdir A2 + $ cat > A2/dune << EOF + > (rocq.theory + > (name A) + > (public_name pkg.a2)) + > EOF + $ cat > A2/a2.v << EOF + > Definition z := 2. + > EOF + $ dune build A2/a2.vo + + $ trace_rocq_flags B/b.vo | grep -o '"-package","rocq-stdlib"' + "-package","rocq-stdlib" + "-package","rocq-stdlib" + $ trace_rocq_flags B/b.vo | grep '"-package","pkg.a"' || true diff --git a/test/blackbox-tests/test-cases/rocq/findlib-layout.t/run.t b/test/blackbox-tests/test-cases/rocq/findlib-layout.t/run.t new file mode 100644 index 00000000000..1b3fca4edda --- /dev/null +++ b/test/blackbox-tests/test-cases/rocq/findlib-layout.t/run.t @@ -0,0 +1,62 @@ +Rocq public theories use findlib-style packages and install under rocq.d. + + $ make_rocq_project 3.25 0.15 + $ cat >> dune-project << EOF + > (package (name pkg)) + > EOF + $ touch pkg.opam + +A public theory with a public_name is installed in its findlib package +(directory) under rocq.d, not under coq/user-contrib. + + $ mkdir A + $ cat > A/dune << EOF + > (rocq.theory + > (name A) + > (public_name pkg) + > (synopsis "A theory")) + > EOF + $ cat > A/a.v << EOF + > Definition x := 0. + > EOF + +The legacy layout can still be requested explicitly. + + $ mkdir B + $ cat > B/dune << EOF + > (rocq.theory + > (name B) + > (public_name pkg.b) + > (theories A) + > (legacy_install)) + > EOF + $ cat > B/b.v << EOF + > From A Require Import a. + > Definition y := x. + > EOF + + $ dune build @install + $ find _build/install/default/lib -type l | sort + _build/install/default/lib/coq/user-contrib/B/b.glob + _build/install/default/lib/coq/user-contrib/B/b.v + _build/install/default/lib/coq/user-contrib/B/b.vo + _build/install/default/lib/pkg/META + _build/install/default/lib/pkg/b/rocq.d/b.glob + _build/install/default/lib/pkg/b/rocq.d/b.v + _build/install/default/lib/pkg/b/rocq.d/b.vo + _build/install/default/lib/pkg/dune-package + _build/install/default/lib/pkg/opam + _build/install/default/lib/pkg/rocq.d/a.glob + _build/install/default/lib/pkg/rocq.d/a.v + _build/install/default/lib/pkg/rocq.d/a.vo + + $ cat _build/install/default/lib/pkg/META + description = "A theory" + rocqpath = "A" + requires = "rocq-core" + package "b" ( + directory = "b" + description = "" + rocqpath = "B" + requires = "pkg rocq-core" + ) diff --git a/test/blackbox-tests/test-cases/rocq/findlib-plugin.t/run.t b/test/blackbox-tests/test-cases/rocq/findlib-plugin.t/run.t new file mode 100644 index 00000000000..b6401f44eb3 --- /dev/null +++ b/test/blackbox-tests/test-cases/rocq/findlib-plugin.t/run.t @@ -0,0 +1,55 @@ +A public Rocq theory in the new findlib layout can depend on a plugin from the +same package. The theory's rocq.d install entries must not be pulled into the +OCAMLPATH layout used for resolving the plugin, otherwise rocqdep sees a cycle +through the theory's own installed .glob file. + + $ make_rocq_project 3.25 0.15 + $ cat >> dune-project << EOF + > (name test) + > (generate_opam_files true) + > (package (name test)) + > EOF + + $ mkdir plugin theories + $ cat > plugin/dune << EOF + > (library + > (name plugin) + > (public_name test.plugin) + > (libraries rocq-runtime.vernac)) + > + > (rocq.pp (modules g_test)) + > EOF + $ touch plugin/plugin.mlpack + $ cat > plugin/g_test.mlg << EOF + > DECLARE PLUGIN "rocq-term-deps.plugin" + > + > { + > + > [@@@ocaml.warning "-27"] + > + > open Stdarg + > + > } + > + > VERNAC COMMAND EXTEND TermDeps CLASSIFIED AS QUERY + > | [ "Hello" ] -> { () } + > END + > EOF + + $ cat > theories/dune << EOF + > (rocq.theory + > (public_name test) + > (name test) + > (plugins test.plugin)) + > EOF + $ cat > theories/plugin.v << EOF + > Declare ML Module "test.plugin". + > EOF + + $ dune build theories/plugin.vo + +The package layout used for Rocq's plugin OCAMLPATH contains plugin files, but +not Rocq theory install files. Exposing the theory's rocq.d symlinks here would +let rocqdep depend on the theory's own installed .glob file. + + $ find _build/install/default/.packages-rocq -path '*rocq.d*' -print diff --git a/test/blackbox-tests/test-cases/rocq/plugin-meta.t/run.t b/test/blackbox-tests/test-cases/rocq/plugin-meta.t/run.t index a19684e84aa..5f28dea95b1 100644 --- a/test/blackbox-tests/test-cases/rocq/plugin-meta.t/run.t +++ b/test/blackbox-tests/test-cases/rocq/plugin-meta.t/run.t @@ -10,6 +10,6 @@ The META file for plugins is built before calling coqdep > EOF $ dune build .bar.theory.d - $ find _build/install/default/.packages -name META | censor - _build/install/default/.packages/$DIGEST/lib/bar/META + $ find _build/install/default/.packages-rocq -name META | censor + _build/install/default/.packages-rocq/$DIGEST/lib/bar/META