[coq] Add dependency to META file for Coq plugins

Traditionally, `coqdep` requires the source files of all involved
theories to be present in the filesystem, as to resolve logical paths
to files.

For `.v` files this process is easy, however for plugins, `coqdep`
relies on the presence of a `plugin.mlpack` file as a hint that a
`plugin.cmxs` file will be produced, so it can correctly map `Declare
Ml` to the right `.cmxs`.

Starting with 8.16, `coqdep` can alternatively use `META` files to do
this mapping, but that requires `META` files to be present in the
build tree, at the right path pointed by `OCAMLPATH`.

We thus add the `META` files as a dependency for coqdep, which is
backwards compatible and will allow us to fix Dune to work with the
new findlib-based plugin loading method in Coq 8.16.

Unfortunately, the code in Coq upstream seems pretty broken (it seems
to produce paths that are wrong w.r.t. our `META` files), so this will
need fixing in Coq to fully work, but this is the Dune part, so the
rest of work belongs to Coq upstream IIANM.

CHANGES.md

@@ -61,6 +61,11 @@
 - update vendored copy of cmdliner to 1.1.1. This improves the built-in
   documentation for command groups such as `dune ocaml`. (#6038, @emillon)
 
+- `(coq.theory ...)` will now depend on the `META` files for declared
+  `(plugin ...)`, so `coqdep` can see them. This enables to use the
+  new `findlib`-based loading method implemented in 8.16 (as of 8.16.0
+  tho Coq itself has some bugs preventing this to work)
+
 3.4.1 (26-07-2022)
 ------------------
 

src/dune_rules/coq_rules.ml

@@ -56,8 +56,29 @@ let resolve_program sctx ~loc ~dir prog =
     ~hint:"opam install coq"
 
 module Coq_plugin = struct
+  let meta_info ~context (lib : Lib.t) =
+    let debug = false in
+    let name = Lib.name lib |> Lib_name.to_string in
+    if debug then Format.eprintf "Meta info for %s@\n" name;
+    match Lib_info.status (Lib.info lib) with
+    | Public (_, pkg) ->
+      let package = Package.name pkg in
+      let meta_i =
+        Path.Build.relative
+          (Local_install_path.lib_dir ~context ~package)
+          "META"
+      in
+      if debug then
+        Format.eprintf "Meta for %s: %s@\n" name (Path.Build.to_string meta_i);
+      Some (Path.build meta_i)
+    | Installed -> None
+    | Installed_private | Private _ ->
+      (* XXX: Do a warning here? Or maybe guard on the Dune lang version ? *)
+      User_error.raise
+        [ Pp.textf "can't depend on private libraries as Coq plugins %s" name ]
+
   (* compute include flags and mlpack rules *)
-  let setup_ml_deps libs theories =
+  let setup_ml_deps ~context libs theories =
     (* Pair of include flags and paths to mlpack *)
     let libs =
       let open Resolve.Memo.O in
@@ -76,18 +97,22 @@ module Coq_plugin = struct
     ( flags
     , let* libs = Resolve.Memo.read libs in
       (* If the mlpack files don't exist, don't fail *)
-      Action_builder.paths_existing (List.concat_map ~f:Util.ml_pack_files libs)
-    )
-
-  let of_buildable ~lib_db ~theories_deps (buildable : Coq_stanza.Buildable.t) =
+      Action_builder.all_unit
+        [ Action_builder.paths (List.filter_map ~f:(meta_info ~context) libs)
+        ; Action_builder.paths_existing
+            (List.concat_map ~f:Util.ml_pack_files libs)
+        ] )
+
+  let of_buildable ~context ~lib_db ~theories_deps
+      (buildable : Coq_stanza.Buildable.t) =
     let res =
       let open Resolve.Memo.O in
       let+ libs =
         Resolve.Memo.List.map buildable.plugins ~f:(fun (loc, name) ->
             let+ lib = Lib.DB.resolve lib_db (loc, name) in
             (loc, lib))
       in
-      setup_ml_deps libs theories_deps
+      setup_ml_deps ~context libs theories_deps
     in
     let ml_flags = Resolve.Memo.map res ~f:fst in
     let mlpack_rule =
@@ -290,12 +315,13 @@ module Context = struct
     let loc = buildable.loc in
     let use_stdlib = buildable.use_stdlib in
     let rr = resolve_program sctx ~dir ~loc in
+    let context = Super_context.context sctx |> Context.name in
     let* expander = Super_context.expander sctx ~dir in
     let* scope = Scope.DB.find_by_dir dir in
     let lib_db = Scope.libs scope in
     (* ML-level flags for depending libraries *)
     let ml_flags, mlpack_rule =
-      Coq_plugin.of_buildable ~theories_deps ~lib_db buildable
+      Coq_plugin.of_buildable ~context ~theories_deps ~lib_db buildable
     in
     let mode = select_native_mode ~sctx ~buildable in
     let* native_includes =

test/blackbox-tests/test-cases/coq/deprecate-libraries.t/run.t

@@ -1,40 +1,42 @@
 The libraries field is deprecated
   $ cat > dune << EOF
   > (library
+  >  (public_name bar.foo)
   >  (name foo))
   > 
-  > (coq.theory 
+  > (coq.theory
   >  (name bar)
-  >  (libraries foo))
+  >  (libraries bar.foo))
   > EOF
 
   $ dune build
-  File "dune", line 6, characters 1-16:
-  6 |  (libraries foo))
-       ^^^^^^^^^^^^^^^
+  File "dune", line 7, characters 1-20:
+  7 |  (libraries bar.foo))
+       ^^^^^^^^^^^^^^^^^^^
   Warning: 'libraries' was deprecated in version 0.5 of the Coq language. It
   has been renamed to 'plugins'.
 
 Having both a libraries and plugins field is an error
   $ cat > dune << EOF
   > (library
+  >  (public_name bar.foo)
   >  (name foo))
   > 
-  > (coq.theory 
+  > (coq.theory
   >  (name bar)
-  >  (libraries foo)
-  >  (plugins foo))
+  >  (libraries bar.foo)
+  >  (plugins bar.foo))
   > EOF
 
   $ dune build
-  File "dune", line 6, characters 1-16:
-  6 |  (libraries foo)
-       ^^^^^^^^^^^^^^^
+  File "dune", line 7, characters 1-20:
+  7 |  (libraries bar.foo)
+       ^^^^^^^^^^^^^^^^^^^
   Warning: 'libraries' was deprecated in version 0.5 of the Coq language. It
   has been renamed to 'plugins'.
-  File "dune", line 6, characters 12-15:
-  6 |  (libraries foo)
-                  ^^^
+  File "dune", line 7, characters 12-19:
+  7 |  (libraries bar.foo)
+                  ^^^^^^^
   Error: Cannot both use 'plugins' and 'libraries', please remove 'libraries'
   as it has been deprecated since version 0.5 of the Coq language. It will be
   removed before version 1.0.