[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.

The issue upstream is coq/coq#16571

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

CHANGES.md

@@ -71,14 +71,20 @@
 
 - The test suite for Coq now requires Coq >= 8.16 due to changes in the
   plugin loading mechanism upstream (which now uses findlib).
-  
+
 - Starting with Coq build language 0.6, theories can be built without importing
   Coq's standard library by including `(stdlib no)`.
   (#6165 #6164, fixes #6163, @ejgallego @Alizter @LasseBlaauwbroek)
 
 - on macOS, sign executables produced by artifact substitution (#6137, fixes
   #5650, @emillon)
 
+- The `(coq.theory ...)` stanza will now ensure that for each declared
+ `(plugin ...)`, the `META` file for it is built before calling
+ `coqdep`. This enables to use the new `findlib`-based loading method
+ in Coq 8.16, however as of Coq 8.16.0, Coq itself has some bugs
+ preventing this to work yet. (#6167 , workarounds #5767, @ejgallego)
+
 3.4.1 (26-07-2022)
 ------------------
 

src/dune_rules/coq_rules.ml

@@ -56,8 +56,31 @@ let resolve_program sctx ~loc ~dir prog =
     ~hint:"opam install coq"
 
 module Coq_plugin = struct
+  let meta_info ~coq_lang_version ~plugin_loc ~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 _ ->
+      let is_error = coq_lang_version >= (0, 6) in
+      let text = if is_error then "not supported" else "deprecated" in
+      User_warning.emit ?loc:plugin_loc ~is_error
+        [ Pp.textf "Using private library %s as a Coq plugin is %s" name text ];
+      None
+
   (* compute include flags and mlpack rules *)
-  let setup_ml_deps libs theories =
+  let setup_ml_deps ~coq_lang_version ~context ~plugin_loc libs theories =
     (* Pair of include flags and paths to mlpack *)
     let libs =
       let open Resolve.Memo.O in
@@ -76,18 +99,27 @@ 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 ~plugin_loc ~coq_lang_version ~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
+      let coq_lang_version = buildable.coq_lang_version in
+      let plugin_loc = List.hd_opt buildable.plugins |> Option.map ~f:fst in
+      setup_ml_deps ~plugin_loc ~coq_lang_version ~context libs theories_deps
     in
     let ml_flags = Resolve.Memo.map res ~f:fst in
     let mlpack_rule =
@@ -290,12 +322,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.

test/blackbox-tests/test-cases/coq/plugin-meta.t/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.5)
+(using coq 0.6)

test/blackbox-tests/test-cases/coq/plugin-meta.t/foo.ml

@@ -0,0 +1 @@
+let foo = "bar"

test/blackbox-tests/test-cases/coq/plugin-meta.t/run.t

@@ -0,0 +1,16 @@
+The META file for plugins is built before calling coqdep
+  $ cat > dune << EOF
+  > (library
+  >  (public_name bar.foo)
+  >  (name foo))
+  > 
+  > (coq.theory
+  >  (name bar)
+  >  (plugins bar.foo))
+  > EOF
+
+  $ dune build bar.v.d
+  $ ls _build/install/default/lib/bar
+  _build/install/default/lib/bar:
+  META
+

test/blackbox-tests/test-cases/coq/plugin-private.t/dune-project

@@ -0,0 +1,2 @@
+(lang dune 3.5)
+(using coq 0.6)

test/blackbox-tests/test-cases/coq/plugin-private.t/foo.ml

@@ -0,0 +1 @@
+let foo = "bar"

test/blackbox-tests/test-cases/coq/plugin-private.t/run.t

@@ -0,0 +1,16 @@
+In Coq >= 0.6 depending on a private library as a plugin is an error.
+  $ cat > dune << EOF
+  > (library
+  >  (name foo))
+  > 
+  > (coq.theory
+  >  (name bar)
+  >  (plugins foo))
+  > EOF
+
+  $ dune build
+  File "dune", line 6, characters 10-13:
+  6 |  (plugins foo))
+                ^^^
+  Error: Using private library foo as a Coq plugin is not supported
+  [1]